> So what? We all know in principle that this reasoning can be written down formally in ZFC with enough effort

But how can you know this? You're starting from reasoning in natural language that, by your own admission, sometimes engages in "sloppy" abuses of notation, such as treating isomorphism as if it could be equated with identity. Whenever mathematicians argue that "this can be written down formally in ZFC" they're essentially using a sloppy, informal, ad-hoc version of type theory and higher-level logic in the process; they're merely in denial about this point.