Suppose we are writing very detailed proofs, absolutely without any gaps (for example, for checking proofs by computer).
In such formal proofs every step (even a trivial one) must be justified.
For example, when we have proved that A = B and A is a prime number, we can infer that B is also a prime number.
We can justify this step by Leibniz Law (which may be represented by an axiom of Predicate Calculus with Equality).
When a group A is isomorphic to a group B and the group A is simple, then we can infer that the group B is also simple.
We can say , that "the isomorphism inference rule" was used in that case.
To justify such inferences, Bourbaki developed a general theory of isomorphism (see their book "Theory of Sets").
Because the Bourbaki theory is rather complicated, my questions are:
It seems that the Bourbaki theory can be greatly simplified if we allow only one principal base set. The example of an untransportable relation (i.e. formula) in the book involves 2 principal base sets. Are there examples of untrasportable formulas when we allow only one principal base set?
Are there other approaches for justification of "the isomorphism inference rule"?
Or maybe there are more simple expositions of Bourbaki approach?