Metamath Proof Explorer

Theorem grothtsk

Description: The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013)

Ref Expression
Assertion grothtsk ⊢ ⋃ Tarski = V

Proof

Step Hyp Ref Expression
1 axgroth5 ⊢ ∃ x w ∈ x ∧ ∀ y ∈ x 𝒫 y ⊆ x ∧ ∃ z ∈ x 𝒫 y ⊆ z ∧ ∀ y ∈ 𝒫 x y ≈ x ∨ y ∈ x
2 eltskg ⊢ x ∈ V → x ∈ Tarski ↔ ∀ y ∈ x 𝒫 y ⊆ x ∧ ∃ z ∈ x 𝒫 y ⊆ z ∧ ∀ y ∈ 𝒫 x y ≈ x ∨ y ∈ x
3 2 elv ⊢ x ∈ Tarski ↔ ∀ y ∈ x 𝒫 y ⊆ x ∧ ∃ z ∈ x 𝒫 y ⊆ z ∧ ∀ y ∈ 𝒫 x y ≈ x ∨ y ∈ x
4 3 anbi2i ⊢ w ∈ x ∧ x ∈ Tarski ↔ w ∈ x ∧ ∀ y ∈ x 𝒫 y ⊆ x ∧ ∃ z ∈ x 𝒫 y ⊆ z ∧ ∀ y ∈ 𝒫 x y ≈ x ∨ y ∈ x
5 3anass ⊢ w ∈ x ∧ ∀ y ∈ x 𝒫 y ⊆ x ∧ ∃ z ∈ x 𝒫 y ⊆ z ∧ ∀ y ∈ 𝒫 x y ≈ x ∨ y ∈ x ↔ w ∈ x ∧ ∀ y ∈ x 𝒫 y ⊆ x ∧ ∃ z ∈ x 𝒫 y ⊆ z ∧ ∀ y ∈ 𝒫 x y ≈ x ∨ y ∈ x
6 4 5 bitr4i ⊢ w ∈ x ∧ x ∈ Tarski ↔ w ∈ x ∧ ∀ y ∈ x 𝒫 y ⊆ x ∧ ∃ z ∈ x 𝒫 y ⊆ z ∧ ∀ y ∈ 𝒫 x y ≈ x ∨ y ∈ x
7 6 exbii ⊢ ∃ x w ∈ x ∧ x ∈ Tarski ↔ ∃ x w ∈ x ∧ ∀ y ∈ x 𝒫 y ⊆ x ∧ ∃ z ∈ x 𝒫 y ⊆ z ∧ ∀ y ∈ 𝒫 x y ≈ x ∨ y ∈ x
8 1 7 mpbir ⊢ ∃ x w ∈ x ∧ x ∈ Tarski
9 eluni ⊢ w ∈ ⋃ Tarski ↔ ∃ x w ∈ x ∧ x ∈ Tarski
10 8 9 mpbir ⊢ w ∈ ⋃ Tarski
11 vex ⊢ w ∈ V
12 10 11 2th ⊢ w ∈ ⋃ Tarski ↔ w ∈ V
13 12 eqriv ⊢ ⋃ Tarski = V