Metamath Proof Explorer

Theorem grothpwex

Description: Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth . Note that ax-pow is not used by the proof. Use axpweq to obtain ax-pow . Use pwex or pwexg instead. (Contributed by GΓ©rard Lang, 22-Jun-2009) (New usage is discouraged.)

Ref Expression
Assertion grothpwex βŠ’π’«x∈V

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