Metamath Proof Explorer

Theorem axgroth5

Description: The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009)

Ref Expression
Assertion axgroth5 ⊢∃yx∈y∧∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y

Proof

Step Hyp Ref Expression
1 ax-groth ⊢∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y
2 biid ⊢x∈y↔x∈y
3 pwss ⊢𝒫z⊆y↔∀ww⊆z→w∈y
4 pwss ⊢𝒫z⊆w↔∀vv⊆z→v∈w
5 4 rexbii ⊢∃w∈y𝒫z⊆w↔∃w∈y∀vv⊆z→v∈w
6 3 5 anbi12i ⊢𝒫z⊆y∧∃w∈y𝒫z⊆w↔∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w
7 6 ralbii ⊢∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w↔∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w
8 df-ral ⊢∀z∈𝒫yz≈y∨z∈y↔∀zz∈𝒫y→z≈y∨z∈y
9 velpw ⊢z∈𝒫y↔z⊆y
10 9 imbi1i ⊢z∈𝒫y→z≈y∨z∈y↔z⊆y→z≈y∨z∈y
11 10 albii ⊢∀zz∈𝒫y→z≈y∨z∈y↔∀zz⊆y→z≈y∨z∈y
12 8 11 bitri ⊢∀z∈𝒫yz≈y∨z∈y↔∀zz⊆y→z≈y∨z∈y
13 2 7 12 3anbi123i ⊢x∈y∧∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y↔x∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y
14 13 exbii ⊢∃yx∈y∧∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y↔∃yx∈y∧∀z∈y∀ww⊆z→w∈y∧∃w∈y∀vv⊆z→v∈w∧∀zz⊆y→z≈y∨z∈y
15 1 14 mpbir ⊢∃yx∈y∧∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y