Metamath Proof Explorer

Theorem pwclaxpow

Description: Suppose M is a transitive class that is closed under power sets intersected with M . Then, M models the Axiom of Power Sets ax-pow . One direction of Lemma II.2.8 of Kunen2 p. 113. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion pwclaxpow 
|- ( ( Tr M /\ A. x e. M ( ~P x i^i M ) e. M ) -> A. x e. M E. y e. M A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. y ) )

Proof

Step Hyp Ref Expression
1 velpw 
 |-  ( z e. ~P x <-> z C_ x )
2 ssabso 
 |-  ( ( Tr M /\ z e. M ) -> ( z C_ x <-> A. w e. M ( w e. z -> w e. x ) ) )
3 1 2 bitrid 
 |-  ( ( Tr M /\ z e. M ) -> ( z e. ~P x <-> A. w e. M ( w e. z -> w e. x ) ) )
4 elin 
 |-  ( z e. ( ~P x i^i M ) <-> ( z e. ~P x /\ z e. M ) )
5 4 simplbi2com 
 |-  ( z e. M -> ( z e. ~P x -> z e. ( ~P x i^i M ) ) )
6 5 adantl 
 |-  ( ( Tr M /\ z e. M ) -> ( z e. ~P x -> z e. ( ~P x i^i M ) ) )
7 3 6 sylbird 
 |-  ( ( Tr M /\ z e. M ) -> ( A. w e. M ( w e. z -> w e. x ) -> z e. ( ~P x i^i M ) ) )
8 7 ralrimiva 
 |-  ( Tr M -> A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. ( ~P x i^i M ) ) )
9 eleq2 
 |-  ( y = ( ~P x i^i M ) -> ( z e. y <-> z e. ( ~P x i^i M ) ) )
10 9 imbi2d 
 |-  ( y = ( ~P x i^i M ) -> ( ( A. w e. M ( w e. z -> w e. x ) -> z e. y ) <-> ( A. w e. M ( w e. z -> w e. x ) -> z e. ( ~P x i^i M ) ) ) )
11 10 ralbidv 
 |-  ( y = ( ~P x i^i M ) -> ( A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. y ) <-> A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. ( ~P x i^i M ) ) ) )
12 11 rspcev 
 |-  ( ( ( ~P x i^i M ) e. M /\ A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. ( ~P x i^i M ) ) ) -> E. y e. M A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. y ) )
13 8 12 sylan2 
 |-  ( ( ( ~P x i^i M ) e. M /\ Tr M ) -> E. y e. M A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. y ) )
14 13 expcom 
 |-  ( Tr M -> ( ( ~P x i^i M ) e. M -> E. y e. M A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. y ) ) )
15 14 ralimdv 
 |-  ( Tr M -> ( A. x e. M ( ~P x i^i M ) e. M -> A. x e. M E. y e. M A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. y ) ) )
16 15 imp 
 |-  ( ( Tr M /\ A. x e. M ( ~P x i^i M ) e. M ) -> A. x e. M E. y e. M A. z e. M ( A. w e. M ( w e. z -> w e. x ) -> z e. y ) )