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