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∈𝒫ux≺u→x∈u
8 7 biimpri ⊢∀x∈𝒫ux≺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∈𝒫ux≺u→x∈u→y∈dom⁡card
24 23 3impia ⊢y∈u∧∀x∈u𝒫x⊆u∧𝒫x∈u∧∀x∈𝒫ux≺u→x∈u→y∈dom⁡card
25 axgroth6 ⊢∃uy∈u∧∀x∈u𝒫x⊆u∧𝒫x∈u∧∀x∈𝒫ux≺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