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 ⊢∃xw∈x∧∀y∈x𝒫y⊆x∧∃z∈x𝒫y⊆z∧∀y∈𝒫xy≈x∨y∈x
2 eltskg ⊢x∈V→x∈Tarski↔∀y∈x𝒫y⊆x∧∃z∈x𝒫y⊆z∧∀y∈𝒫xy≈x∨y∈x
3 2 elv ⊢x∈Tarski↔∀y∈x𝒫y⊆x∧∃z∈x𝒫y⊆z∧∀y∈𝒫xy≈x∨y∈x
4 3 anbi2i ⊢w∈x∧x∈Tarski↔w∈x∧∀y∈x𝒫y⊆x∧∃z∈x𝒫y⊆z∧∀y∈𝒫xy≈x∨y∈x
5 3anass ⊢w∈x∧∀y∈x𝒫y⊆x∧∃z∈x𝒫y⊆z∧∀y∈𝒫xy≈x∨y∈x↔w∈x∧∀y∈x𝒫y⊆x∧∃z∈x𝒫y⊆z∧∀y∈𝒫xy≈x∨y∈x
6 4 5 bitr4i ⊢w∈x∧x∈Tarski↔w∈x∧∀y∈x𝒫y⊆x∧∃z∈x𝒫y⊆z∧∀y∈𝒫xy≈x∨y∈x
7 6 exbii ⊢∃xw∈x∧x∈Tarski↔∃xw∈x∧∀y∈x𝒫y⊆x∧∃z∈x𝒫y⊆z∧∀y∈𝒫xy≈x∨y∈x
8 1 7 mpbir ⊢∃xw∈x∧x∈Tarski
9 eluni ⊢w∈⋃Tarski↔∃xw∈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