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