Metamath Proof Explorer

Theorem grothpw

Description: Derive the Axiom of Power Sets ax-pow from the Tarski-Grothendieck axiom ax-groth . That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html . Note that ax-pow is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009) (New usage is discouraged.)

Ref Expression
Assertion grothpw ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y

Proof

Step Hyp Ref Expression
1 simpl ⊢ 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w → 𝒫 z ⊆ y
2 1 ralimi ⊢ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w → ∀ z ∈ y 𝒫 z ⊆ y
3 pweq ⊢ z = x → 𝒫 z = 𝒫 x
4 3 sseq1d ⊢ z = x → 𝒫 z ⊆ y ↔ 𝒫 x ⊆ y
5 4 rspccv ⊢ ∀ z ∈ y 𝒫 z ⊆ y → x ∈ y → 𝒫 x ⊆ y
6 2 5 syl ⊢ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w → x ∈ y → 𝒫 x ⊆ y
7 6 anim2i ⊢ x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w → x ∈ y ∧ x ∈ y → 𝒫 x ⊆ y
8 7 3adant3 ⊢ x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y → x ∈ y ∧ x ∈ y → 𝒫 x ⊆ y
9 pm3.35 ⊢ x ∈ y ∧ x ∈ y → 𝒫 x ⊆ y → 𝒫 x ⊆ y
10 vex ⊢ y ∈ V
11 10 ssex ⊢ 𝒫 x ⊆ y → 𝒫 x ∈ V
12 8 9 11 3syl ⊢ x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y → 𝒫 x ∈ V
13 axgroth5 ⊢ ∃ y x ∈ y ∧ ∀ z ∈ y 𝒫 z ⊆ y ∧ ∃ w ∈ y 𝒫 z ⊆ w ∧ ∀ z ∈ 𝒫 y z ≈ y ∨ z ∈ y
14 12 13 exlimiiv ⊢ 𝒫 x ∈ V
15 axpweq ⊢ 𝒫 x ∈ V ↔ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y
16 14 15 mpbi ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y