Metamath Proof Explorer

Theorem permaxpow

Description: The Axiom of Power Sets ax-pow holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 6-Nov-2025)

Ref Expression
Hypotheses permmodel.1 
|- F : _V -1-1-onto-> _V
permmodel.2 
|- R = ( `' F o. _E )
Assertion permaxpow 
|- E. y A. z ( A. w ( w R z -> w R x ) -> z R y )

Proof

Step Hyp Ref Expression
1 permmodel.1 
 |-  F : _V -1-1-onto-> _V
2 permmodel.2 
 |-  R = ( `' F o. _E )
3 fvex 
 |-  ( `' F ` ( `' F " ~P ( F ` x ) ) ) e. _V
4 breq2 
 |-  ( y = ( `' F ` ( `' F " ~P ( F ` x ) ) ) -> ( z R y <-> z R ( `' F ` ( `' F " ~P ( F ` x ) ) ) ) )
5 4 imbi2d 
 |-  ( y = ( `' F ` ( `' F " ~P ( F ` x ) ) ) -> ( ( A. w ( w R z -> w R x ) -> z R y ) <-> ( A. w ( w R z -> w R x ) -> z R ( `' F ` ( `' F " ~P ( F ` x ) ) ) ) ) )
6 5 albidv 
 |-  ( y = ( `' F ` ( `' F " ~P ( F ` x ) ) ) -> ( A. z ( A. w ( w R z -> w R x ) -> z R y ) <-> A. z ( A. w ( w R z -> w R x ) -> z R ( `' F ` ( `' F " ~P ( F ` x ) ) ) ) ) )
7 vex 
 |-  z e. _V
8 dff1o3 
 |-  ( F : _V -1-1-onto-> _V <-> ( F : _V -onto-> _V /\ Fun `' F ) )
9 1 8 mpbi 
 |-  ( F : _V -onto-> _V /\ Fun `' F )
10 9 simpri 
 |-  Fun `' F
11 fvex 
 |-  ( F ` x ) e. _V
12 11 pwex 
 |-  ~P ( F ` x ) e. _V
13 12 funimaex 
 |-  ( Fun `' F -> ( `' F " ~P ( F ` x ) ) e. _V )
14 10 13 ax-mp 
 |-  ( `' F " ~P ( F ` x ) ) e. _V
15 1 2 7 14 brpermmodelcnv 
 |-  ( z R ( `' F ` ( `' F " ~P ( F ` x ) ) ) <-> z e. ( `' F " ~P ( F ` x ) ) )
16 f1ofn 
 |-  ( F : _V -1-1-onto-> _V -> F Fn _V )
17 1 16 ax-mp 
 |-  F Fn _V
18 elpreima 
 |-  ( F Fn _V -> ( z e. ( `' F " ~P ( F ` x ) ) <-> ( z e. _V /\ ( F ` z ) e. ~P ( F ` x ) ) ) )
19 17 18 ax-mp 
 |-  ( z e. ( `' F " ~P ( F ` x ) ) <-> ( z e. _V /\ ( F ` z ) e. ~P ( F ` x ) ) )
20 7 19 mpbiran 
 |-  ( z e. ( `' F " ~P ( F ` x ) ) <-> ( F ` z ) e. ~P ( F ` x ) )
21 15 20 bitri 
 |-  ( z R ( `' F ` ( `' F " ~P ( F ` x ) ) ) <-> ( F ` z ) e. ~P ( F ` x ) )
22 df-ss 
 |-  ( ( F ` z ) C_ ( F ` x ) <-> A. w ( w e. ( F ` z ) -> w e. ( F ` x ) ) )
23 fvex 
 |-  ( F ` z ) e. _V
24 23 elpw 
 |-  ( ( F ` z ) e. ~P ( F ` x ) <-> ( F ` z ) C_ ( F ` x ) )
25 vex 
 |-  w e. _V
26 1 2 25 7 brpermmodel 
 |-  ( w R z <-> w e. ( F ` z ) )
27 vex 
 |-  x e. _V
28 1 2 25 27 brpermmodel 
 |-  ( w R x <-> w e. ( F ` x ) )
29 26 28 imbi12i 
 |-  ( ( w R z -> w R x ) <-> ( w e. ( F ` z ) -> w e. ( F ` x ) ) )
30 29 albii 
 |-  ( A. w ( w R z -> w R x ) <-> A. w ( w e. ( F ` z ) -> w e. ( F ` x ) ) )
31 22 24 30 3bitr4i 
 |-  ( ( F ` z ) e. ~P ( F ` x ) <-> A. w ( w R z -> w R x ) )
32 21 31 sylbbr 
 |-  ( A. w ( w R z -> w R x ) -> z R ( `' F ` ( `' F " ~P ( F ` x ) ) ) )
33 32 ax-gen 
 |-  A. z ( A. w ( w R z -> w R x ) -> z R ( `' F ` ( `' F " ~P ( F ` x ) ) ) )
34 3 6 33 ceqsexv2d 
 |-  E. y A. z ( A. w ( w R z -> w R x ) -> z R y )