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 → 𝒫 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