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∀ww∈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∈𝒫yz≈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∈𝒫yz≈y∨z∈y→𝒫x∈V
13 axgroth5 ⊢∃yx∈y∧∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y
14 12 13 exlimiiv ⊢𝒫x∈V
15 axpweq ⊢𝒫x∈V↔∃y∀z∀ww∈z→w∈x→z∈y
16 14 15 mpbi ⊢∃y∀z∀ww∈z→w∈x→z∈y