This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 -> ~P x = ~P y )
2 1 sseq1d 
 |-  ( x = y -> ( ~P x C_ u <-> ~P y C_ u ) )
3 1 eleq1d 
 |-  ( x = y -> ( ~P x e. u <-> ~P y e. u ) )
4 2 3 anbi12d 
 |-  ( x = y -> ( ( ~P x C_ u /\ ~P x e. u ) <-> ( ~P y C_ u /\ ~P y e. u ) ) )
5 4 rspcva 
 |-  ( ( y e. u /\ A. x e. u ( ~P x C_ u /\ ~P x e. u ) ) -> ( ~P y C_ u /\ ~P y e. u ) )
6 5 simpld 
 |-  ( ( y e. u /\ A. x e. u ( ~P x C_ u /\ ~P x e. u ) ) -> ~P y C_ u )
7 rabss 
 |-  ( { x e. ~P u | x ~< u } C_ u <-> A. x e. ~P u ( x ~< u -> x e. u ) )
8 7 biimpri 
 |-  ( A. x e. ~P u ( x ~< u -> x e. u ) -> { x e. ~P u | x ~< u } C_ u )
9 vex 
 |-  y e. _V
10 9 canth2 
 |-  y ~< ~P y
11 sdomdom 
 |-  ( y ~< ~P y -> y ~<_ ~P y )
12 10 11 ax-mp 
 |-  y ~<_ ~P y
13 ssdomg 
 |-  ( u e. _V -> ( ~P y C_ u -> ~P y ~<_ u ) )
14 13 elv 
 |-  ( ~P y C_ u -> ~P y ~<_ u )
15 domtr 
 |-  ( ( y ~<_ ~P y /\ ~P y ~<_ u ) -> y ~<_ u )
16 12 14 15 sylancr 
 |-  ( ~P y C_ u -> y ~<_ u )
17 vex 
 |-  u e. _V
18 tskwe 
 |-  ( ( u e. _V /\ { x e. ~P u | x ~< u } C_ u ) -> u e. dom card )
19 17 18 mpan 
 |-  ( { x e. ~P u | x ~< u } C_ u -> u e. dom card )
20 numdom 
 |-  ( ( u e. dom card /\ y ~<_ u ) -> y e. dom card )
21 20 expcom 
 |-  ( y ~<_ u -> ( u e. dom card -> y e. dom card ) )
22 16 19 21 syl2im 
 |-  ( ~P y C_ u -> ( { x e. ~P u | x ~< u } C_ u -> y e. dom card ) )
23 6 8 22 syl2im 
 |-  ( ( y e. u /\ A. x e. u ( ~P x C_ u /\ ~P x e. u ) ) -> ( A. x e. ~P u ( x ~< u -> x e. u ) -> y e. dom card ) )
24 23 3impia 
 |-  ( ( y e. u /\ A. x e. u ( ~P x C_ u /\ ~P x e. u ) /\ A. x e. ~P u ( x ~< u -> x e. u ) ) -> y e. dom card )
25 axgroth6 
 |-  E. u ( y e. u /\ A. x e. u ( ~P x C_ u /\ ~P x e. u ) /\ A. x e. ~P u ( x ~< u -> x e. u ) )
26 24 25 exlimiiv 
 |-  y e. dom card
27 26 9 2th 
 |-  ( y e. dom card <-> y e. _V )
28 27 eqriv 
 |-  dom card = _V