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 ⊢ ( 𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦 )
2 1 sseq1d ⊢ ( 𝑥 = 𝑦 → ( 𝒫 𝑥 ⊆ 𝑢 ↔ 𝒫 𝑦 ⊆ 𝑢 ) )
3 1 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝒫 𝑥 ∈ 𝑢 ↔ 𝒫 𝑦 ∈ 𝑢 ) )
4 2 3 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ↔ ( 𝒫 𝑦 ⊆ 𝑢 ∧ 𝒫 𝑦 ∈ 𝑢 ) ) )
5 4 rspcva ⊢ ( ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ) → ( 𝒫 𝑦 ⊆ 𝑢 ∧ 𝒫 𝑦 ∈ 𝑢 ) )
6 5 simpld ⊢ ( ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ) → 𝒫 𝑦 ⊆ 𝑢 )
7 rabss ⊢ ( { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 ↔ ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) )
8 7 biimpri ⊢ ( ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) → { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 )
9 vex ⊢ 𝑦 ∈ V
10 9 canth2 ⊢ 𝑦 ≺ 𝒫 𝑦
11 sdomdom ⊢ ( 𝑦 ≺ 𝒫 𝑦 → 𝑦 ≼ 𝒫 𝑦 )
12 10 11 ax-mp ⊢ 𝑦 ≼ 𝒫 𝑦
13 ssdomg ⊢ ( 𝑢 ∈ V → ( 𝒫 𝑦 ⊆ 𝑢 → 𝒫 𝑦 ≼ 𝑢 ) )
14 13 elv ⊢ ( 𝒫 𝑦 ⊆ 𝑢 → 𝒫 𝑦 ≼ 𝑢 )
15 domtr ⊢ ( ( 𝑦 ≼ 𝒫 𝑦 ∧ 𝒫 𝑦 ≼ 𝑢 ) → 𝑦 ≼ 𝑢 )
16 12 14 15 sylancr ⊢ ( 𝒫 𝑦 ⊆ 𝑢 → 𝑦 ≼ 𝑢 )
17 vex ⊢ 𝑢 ∈ V
18 tskwe ⊢ ( ( 𝑢 ∈ V ∧ { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 ) → 𝑢 ∈ dom card )
19 17 18 mpan ⊢ ( { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 → 𝑢 ∈ dom card )
20 numdom ⊢ ( ( 𝑢 ∈ dom card ∧ 𝑦 ≼ 𝑢 ) → 𝑦 ∈ dom card )
21 20 expcom ⊢ ( 𝑦 ≼ 𝑢 → ( 𝑢 ∈ dom card → 𝑦 ∈ dom card ) )
22 16 19 21 syl2im ⊢ ( 𝒫 𝑦 ⊆ 𝑢 → ( { 𝑥 ∈ 𝒫 𝑢 ∣ 𝑥 ≺ 𝑢 } ⊆ 𝑢 → 𝑦 ∈ dom card ) )
23 6 8 22 syl2im ⊢ ( ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ) → ( ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) → 𝑦 ∈ dom card ) )
24 23 3impia ⊢ ( ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) ) → 𝑦 ∈ dom card )
25 axgroth6 ⊢ ∃ 𝑢 ( 𝑦 ∈ 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ⊆ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑢 ( 𝑥 ≺ 𝑢 → 𝑥 ∈ 𝑢 ) )
26 24 25 exlimiiv ⊢ 𝑦 ∈ dom card
27 26 9 2th ⊢ ( 𝑦 ∈ dom card ↔ 𝑦 ∈ V )
28 27 eqriv ⊢ dom card = V