This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝒫 𝑦 ⊆ 𝑥 ∧ ∃ 𝑧 ∈ 𝑥 𝒫 𝑦 ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≈ 𝑥 ∨ 𝑦 ∈ 𝑥 ) )
2 eltskg ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ Tarski ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝒫 𝑦 ⊆ 𝑥 ∧ ∃ 𝑧 ∈ 𝑥 𝒫 𝑦 ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≈ 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) ) )
3 2 elv ⊢ ( 𝑥 ∈ Tarski ↔ ( ∀ 𝑦 ∈ 𝑥 ( 𝒫 𝑦 ⊆ 𝑥 ∧ ∃ 𝑧 ∈ 𝑥 𝒫 𝑦 ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≈ 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) )
4 3 anbi2i ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ Tarski ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( ∀ 𝑦 ∈ 𝑥 ( 𝒫 𝑦 ⊆ 𝑥 ∧ ∃ 𝑧 ∈ 𝑥 𝒫 𝑦 ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≈ 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) ) )
5 3anass ⊢ ( ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝒫 𝑦 ⊆ 𝑥 ∧ ∃ 𝑧 ∈ 𝑥 𝒫 𝑦 ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≈ 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( ∀ 𝑦 ∈ 𝑥 ( 𝒫 𝑦 ⊆ 𝑥 ∧ ∃ 𝑧 ∈ 𝑥 𝒫 𝑦 ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≈ 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) ) )
6 4 5 bitr4i ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ Tarski ) ↔ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝒫 𝑦 ⊆ 𝑥 ∧ ∃ 𝑧 ∈ 𝑥 𝒫 𝑦 ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≈ 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) )
7 6 exbii ⊢ ( ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ Tarski ) ↔ ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝒫 𝑦 ⊆ 𝑥 ∧ ∃ 𝑧 ∈ 𝑥 𝒫 𝑦 ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ≈ 𝑥 ∨ 𝑦 ∈ 𝑥 ) ) )
8 1 7 mpbir ⊢ ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ Tarski )
9 eluni ⊢ ( 𝑤 ∈ ∪ Tarski ↔ ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ Tarski ) )
10 8 9 mpbir ⊢ 𝑤 ∈ ∪ Tarski
11 vex ⊢ 𝑤 ∈ V
12 10 11 2th ⊢ ( 𝑤 ∈ ∪ Tarski ↔ 𝑤 ∈ V )
13 12 eqriv ⊢ ∪ Tarski = V