Metamath Proof Explorer

Theorem axgroth5

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

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

Proof

Step Hyp Ref Expression
1 ax-groth ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → z ≈ y ∨ z ∈ y
2 biid ⊢ x ∈ y ↔ x ∈ y
3 pwss ⊢ 𝒫 z ⊆ y ↔ ∀ w w ⊆ z → w ∈ y
4 pwss ⊢ 𝒫 z ⊆ w ↔ ∀ v v ⊆ z → v ∈ w
5 4 rexbii ⊢ ∃ w ∈ y 𝒫 z ⊆ w ↔ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w
6 3 5 anbi12i ⊢ 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ↔ ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w
7 6 ralbii ⊢ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ↔ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w
8 df-ral ⊢ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y ↔ ∀ z z ∈ 𝒫 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 ⊢ ∀ z z ∈ 𝒫 y → z ≈ y ∨ z ∈ y ↔ ∀ z z ⊆ y → z ≈ y ∨ z ∈ y
12 8 11 bitri ⊢ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y ↔ ∀ z z ⊆ y → z ≈ y ∨ z ∈ y
13 2 7 12 3anbi123i ⊢ x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y ↔ x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → z ≈ y ∨ z ∈ y
14 13 exbii ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y ↔ ∃ y x ∈ y ∧ ∀ z ∈ y ∀ w w ⊆ z → w ∈ y ∧ ∃ w ∈ y ∀ v v ⊆ z → v ∈ w ∧ ∀ z z ⊆ y → z ≈ y ∨ z ∈ y
15 1 14 mpbir ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y