3-On the same page (84) he states axioms A and A', Tarski also considers the 16 following axioms variants for A and A' and asserts witout giving a proof that they are all equivalent. Axiom C: "For every set x, there exists a set y satisfying the four following conditions C1, C2, C3 and C4, where for every i=1,2,3,4 Ci is choosen to be Ai or A'i." QUESTION 3: Does anyone know about an explicit proof of the equivalence of the 16 variants of axioms A and A' ?
4-As an example, let us consider the Tarski-Grothendieck axiom (TG) used by Mizar and Metamath, that is the variant C obtained by choosing C1=A1, C2=A2, C3=A'3 and C4=A4. As A'3 is ane asy consequence of A3 (take w of A'3 to be t of A3), TG is a consequence of axiom A. So, to prove that TG is equivalent with A, it is sufficient to prove that A3 from TG. from A1 and A2, we have that the power-set of x, P(x) is included inside y, and from A'3 that there exists a set w that is a member element of y such that P(x) is included inside w. And also, we have that P(w) is included inside y by A2. In view of A4, suppose that the set P(x) is equipotent with y. We then have an injection i from y into P(x), and as P(x) is included inside w we also have an injection j from y into w, and as P(w) is included inside y, the restriction k of j to the subset P(w) of y is an injection from P(w) to w. But by Cantor's theorem, such an injection k does not exist, so a bijection between P(x) and y is impossible, and by A4, P(x) must be a member element of y, and A3 is proved from TG.
