Metamath Proof Explorer

Theorem wfaxpow

Description: The class of well-founded sets models the Axioms of Power Sets. Part of Corollary II.2.9 of Kunen2 p. 113. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Hypothesis wfax.1 
|- W = U. ( R1 " On )
Assertion wfaxpow 
|- A. x e. W E. y e. W A. z e. W ( A. w e. W ( w e. z -> w e. x ) -> z e. y )

Proof

Step Hyp Ref Expression
1 wfax.1 
 |-  W = U. ( R1 " On )
2 trwf 
 |-  Tr U. ( R1 " On )
3 treq 
 |-  ( W = U. ( R1 " On ) -> ( Tr W <-> Tr U. ( R1 " On ) ) )
4 1 3 ax-mp 
 |-  ( Tr W <-> Tr U. ( R1 " On ) )
5 2 4 mpbir 
 |-  Tr W
6 pwclaxpow 
 |-  ( ( Tr W /\ A. x e. W ( ~P x i^i W ) e. W ) -> A. x e. W E. y e. W A. z e. W ( A. w e. W ( w e. z -> w e. x ) -> z e. y ) )
7 5 6 mpan 
 |-  ( A. x e. W ( ~P x i^i W ) e. W -> A. x e. W E. y e. W A. z e. W ( A. w e. W ( w e. z -> w e. x ) -> z e. y ) )
8 pwwf 
 |-  ( x e. U. ( R1 " On ) <-> ~P x e. U. ( R1 " On ) )
9 8 biimpi 
 |-  ( x e. U. ( R1 " On ) -> ~P x e. U. ( R1 " On ) )
10 r1elssi 
 |-  ( ~P x e. U. ( R1 " On ) -> ~P x C_ U. ( R1 " On ) )
11 dfss2 
 |-  ( ~P x C_ U. ( R1 " On ) <-> ( ~P x i^i U. ( R1 " On ) ) = ~P x )
12 eleq1 
 |-  ( ( ~P x i^i U. ( R1 " On ) ) = ~P x -> ( ( ~P x i^i U. ( R1 " On ) ) e. U. ( R1 " On ) <-> ~P x e. U. ( R1 " On ) ) )
13 11 12 sylbi 
 |-  ( ~P x C_ U. ( R1 " On ) -> ( ( ~P x i^i U. ( R1 " On ) ) e. U. ( R1 " On ) <-> ~P x e. U. ( R1 " On ) ) )
14 9 10 13 3syl 
 |-  ( x e. U. ( R1 " On ) -> ( ( ~P x i^i U. ( R1 " On ) ) e. U. ( R1 " On ) <-> ~P x e. U. ( R1 " On ) ) )
15 9 14 mpbird 
 |-  ( x e. U. ( R1 " On ) -> ( ~P x i^i U. ( R1 " On ) ) e. U. ( R1 " On ) )
16 1 eleq2i 
 |-  ( x e. W <-> x e. U. ( R1 " On ) )
17 1 ineq2i 
 |-  ( ~P x i^i W ) = ( ~P x i^i U. ( R1 " On ) )
18 17 1 eleq12i 
 |-  ( ( ~P x i^i W ) e. W <-> ( ~P x i^i U. ( R1 " On ) ) e. U. ( R1 " On ) )
19 15 16 18 3imtr4i 
 |-  ( x e. W -> ( ~P x i^i W ) e. W )
20 7 19 mprg 
 |-  A. x e. W E. y e. W A. z e. W ( A. w e. W ( w e. z -> w e. x ) -> z e. y )