Metamath Proof Explorer

Theorem permaxun

Description: The Axiom of Union ax-un 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 permaxun 
|- E. y A. z ( E. w ( z R w /\ 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 ` U. ( F " ( F ` x ) ) ) e. _V
4 breq2 
 |-  ( y = ( `' F ` U. ( F " ( F ` x ) ) ) -> ( z R y <-> z R ( `' F ` U. ( F " ( F ` x ) ) ) ) )
5 4 imbi2d 
 |-  ( y = ( `' F ` U. ( F " ( F ` x ) ) ) -> ( ( E. w ( z R w /\ w R x ) -> z R y ) <-> ( E. w ( z R w /\ w R x ) -> z R ( `' F ` U. ( F " ( F ` x ) ) ) ) ) )
6 5 albidv 
 |-  ( y = ( `' F ` U. ( F " ( F ` x ) ) ) -> ( A. z ( E. w ( z R w /\ w R x ) -> z R y ) <-> A. z ( E. w ( z R w /\ w R x ) -> z R ( `' F ` U. ( F " ( F ` x ) ) ) ) ) )
7 vex 
 |-  z e. _V
8 vex 
 |-  w e. _V
9 1 2 7 8 brpermmodel 
 |-  ( z R w <-> z e. ( F ` w ) )
10 vex 
 |-  x e. _V
11 1 2 8 10 brpermmodel 
 |-  ( w R x <-> w e. ( F ` x ) )
12 f1ofn 
 |-  ( F : _V -1-1-onto-> _V -> F Fn _V )
13 1 12 ax-mp 
 |-  F Fn _V
14 ssv 
 |-  ( F ` x ) C_ _V
15 fnfvima 
 |-  ( ( F Fn _V /\ ( F ` x ) C_ _V /\ w e. ( F ` x ) ) -> ( F ` w ) e. ( F " ( F ` x ) ) )
16 13 14 15 mp3an12 
 |-  ( w e. ( F ` x ) -> ( F ` w ) e. ( F " ( F ` x ) ) )
17 elunii 
 |-  ( ( z e. ( F ` w ) /\ ( F ` w ) e. ( F " ( F ` x ) ) ) -> z e. U. ( F " ( F ` x ) ) )
18 16 17 sylan2 
 |-  ( ( z e. ( F ` w ) /\ w e. ( F ` x ) ) -> z e. U. ( F " ( F ` x ) ) )
19 9 11 18 syl2anb 
 |-  ( ( z R w /\ w R x ) -> z e. U. ( F " ( F ` x ) ) )
20 f1ofun 
 |-  ( F : _V -1-1-onto-> _V -> Fun F )
21 1 20 ax-mp 
 |-  Fun F
22 fvex 
 |-  ( F ` x ) e. _V
23 22 funimaex 
 |-  ( Fun F -> ( F " ( F ` x ) ) e. _V )
24 21 23 ax-mp 
 |-  ( F " ( F ` x ) ) e. _V
25 24 uniex 
 |-  U. ( F " ( F ` x ) ) e. _V
26 1 2 7 25 brpermmodelcnv 
 |-  ( z R ( `' F ` U. ( F " ( F ` x ) ) ) <-> z e. U. ( F " ( F ` x ) ) )
27 19 26 sylibr 
 |-  ( ( z R w /\ w R x ) -> z R ( `' F ` U. ( F " ( F ` x ) ) ) )
28 27 exlimiv 
 |-  ( E. w ( z R w /\ w R x ) -> z R ( `' F ` U. ( F " ( F ` x ) ) ) )
29 28 ax-gen 
 |-  A. z ( E. w ( z R w /\ w R x ) -> z R ( `' F ` U. ( F " ( F ` x ) ) ) )
30 3 6 29 ceqsexv2d 
 |-  E. y A. z ( E. w ( z R w /\ w R x ) -> z R y )