Metamath Proof Explorer


Theorem grothac

Description: The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv ). This can be put in a more conventional form via ween and dfac8 . Note that the mere existence of strongly inaccessible cardinals doesn't imply AC, but rather the particular form of the Tarski-Grothendieck axiom (see http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html ). (Contributed by Mario Carneiro, 19-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion grothac dom card = V

Proof

Step Hyp Ref Expression
1 pweq x = y 𝒫 x = 𝒫 y
2 1 sseq1d x = y 𝒫 x u 𝒫 y u
3 1 eleq1d x = y 𝒫 x u 𝒫 y u
4 2 3 anbi12d x = y 𝒫 x u 𝒫 x u 𝒫 y u 𝒫 y u
5 4 rspcva y u x u 𝒫 x u 𝒫 x u 𝒫 y u 𝒫 y u
6 5 simpld y u x u 𝒫 x u 𝒫 x u 𝒫 y u
7 rabss x 𝒫 u | x u u x 𝒫 u x u x u
8 7 biimpri x 𝒫 u x u x u x 𝒫 u | x u u
9 vex y V
10 9 canth2 y 𝒫 y
11 sdomdom y 𝒫 y y 𝒫 y
12 10 11 ax-mp y 𝒫 y
13 ssdomg u V 𝒫 y u 𝒫 y u
14 13 elv 𝒫 y u 𝒫 y u
15 domtr y 𝒫 y 𝒫 y u y u
16 12 14 15 sylancr 𝒫 y u y u
17 vex u V
18 tskwe u V x 𝒫 u | x u u u dom card
19 17 18 mpan x 𝒫 u | x u u u dom card
20 numdom u dom card y u y dom card
21 20 expcom y u u dom card y dom card
22 16 19 21 syl2im 𝒫 y u x 𝒫 u | x u u y dom card
23 6 8 22 syl2im y u x u 𝒫 x u 𝒫 x u x 𝒫 u x u x u y dom card
24 23 3impia y u x u 𝒫 x u 𝒫 x u x 𝒫 u x u x u y dom card
25 axgroth6 u y u x u 𝒫 x u 𝒫 x u x 𝒫 u x u x u
26 24 25 exlimiiv y dom card
27 26 9 2th y dom card y V
28 27 eqriv dom card = V