Metamath Proof Explorer

Theorem permaxinf2lem

Description: Lemma for permaxinf2 . (Contributed by Eric Schmidt, 6-Nov-2025)

Ref Expression
Hypotheses permmodel.1 
|- F : _V -1-1-onto-> _V
permmodel.2 
|- R = ( `' F o. _E )
permaxinf2lem.3 
|- Z = ( rec ( ( v e. _V |-> ( `' F ` ( ( F ` v ) u. { v } ) ) ) , ( `' F ` (/) ) ) " _om )
Assertion permaxinf2lem 
|- E. x ( E. y ( y R x /\ A. z -. z R y ) /\ A. y ( y R x -> E. z ( z R x /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 permmodel.1 
 |-  F : _V -1-1-onto-> _V
2 permmodel.2 
 |-  R = ( `' F o. _E )
3 permaxinf2lem.3 
 |-  Z = ( rec ( ( v e. _V |-> ( `' F ` ( ( F ` v ) u. { v } ) ) ) , ( `' F ` (/) ) ) " _om )
4 fvex 
 |-  ( `' F ` Z ) e. _V
5 breq2 
 |-  ( x = ( `' F ` Z ) -> ( y R x <-> y R ( `' F ` Z ) ) )
6 5 anbi1d 
 |-  ( x = ( `' F ` Z ) -> ( ( y R x /\ A. z -. z R y ) <-> ( y R ( `' F ` Z ) /\ A. z -. z R y ) ) )
7 6 exbidv 
 |-  ( x = ( `' F ` Z ) -> ( E. y ( y R x /\ A. z -. z R y ) <-> E. y ( y R ( `' F ` Z ) /\ A. z -. z R y ) ) )
8 breq2 
 |-  ( x = ( `' F ` Z ) -> ( z R x <-> z R ( `' F ` Z ) ) )
9 8 anbi1d 
 |-  ( x = ( `' F ` Z ) -> ( ( z R x /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) <-> ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) )
10 9 exbidv 
 |-  ( x = ( `' F ` Z ) -> ( E. z ( z R x /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) <-> E. z ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) )
11 5 10 imbi12d 
 |-  ( x = ( `' F ` Z ) -> ( ( y R x -> E. z ( z R x /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) <-> ( y R ( `' F ` Z ) -> E. z ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) ) )
12 11 albidv 
 |-  ( x = ( `' F ` Z ) -> ( A. y ( y R x -> E. z ( z R x /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) <-> A. y ( y R ( `' F ` Z ) -> E. z ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) ) )
13 7 12 anbi12d 
 |-  ( x = ( `' F ` Z ) -> ( ( E. y ( y R x /\ A. z -. z R y ) /\ A. y ( y R x -> E. z ( z R x /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) ) <-> ( E. y ( y R ( `' F ` Z ) /\ A. z -. z R y ) /\ A. y ( y R ( `' F ` Z ) -> E. z ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) ) ) )
14 fvex 
 |-  ( `' F ` (/) ) e. _V
15 breq1 
 |-  ( y = ( `' F ` (/) ) -> ( y R ( `' F ` Z ) <-> ( `' F ` (/) ) R ( `' F ` Z ) ) )
16 breq2 
 |-  ( y = ( `' F ` (/) ) -> ( z R y <-> z R ( `' F ` (/) ) ) )
17 16 notbid 
 |-  ( y = ( `' F ` (/) ) -> ( -. z R y <-> -. z R ( `' F ` (/) ) ) )
18 17 albidv 
 |-  ( y = ( `' F ` (/) ) -> ( A. z -. z R y <-> A. z -. z R ( `' F ` (/) ) ) )
19 15 18 anbi12d 
 |-  ( y = ( `' F ` (/) ) -> ( ( y R ( `' F ` Z ) /\ A. z -. z R y ) <-> ( ( `' F ` (/) ) R ( `' F ` Z ) /\ A. z -. z R ( `' F ` (/) ) ) ) )
20 orbitinit 
 |-  ( ( `' F ` (/) ) e. _V -> ( `' F ` (/) ) e. ( rec ( ( v e. _V |-> ( `' F ` ( ( F ` v ) u. { v } ) ) ) , ( `' F ` (/) ) ) " _om ) )
21 20 3 eleqtrrdi 
 |-  ( ( `' F ` (/) ) e. _V -> ( `' F ` (/) ) e. Z )
22 14 21 ax-mp 
 |-  ( `' F ` (/) ) e. Z
23 orbitex 
 |-  ( rec ( ( v e. _V |-> ( `' F ` ( ( F ` v ) u. { v } ) ) ) , ( `' F ` (/) ) ) " _om ) e. _V
24 3 23 eqeltri 
 |-  Z e. _V
25 1 2 14 24 brpermmodelcnv 
 |-  ( ( `' F ` (/) ) R ( `' F ` Z ) <-> ( `' F ` (/) ) e. Z )
26 22 25 mpbir 
 |-  ( `' F ` (/) ) R ( `' F ` Z )
27 noel 
 |-  -. z e. (/)
28 vex 
 |-  z e. _V
29 0ex 
 |-  (/) e. _V
30 1 2 28 29 brpermmodelcnv 
 |-  ( z R ( `' F ` (/) ) <-> z e. (/) )
31 27 30 mtbir 
 |-  -. z R ( `' F ` (/) )
32 31 ax-gen 
 |-  A. z -. z R ( `' F ` (/) )
33 26 32 pm3.2i 
 |-  ( ( `' F ` (/) ) R ( `' F ` Z ) /\ A. z -. z R ( `' F ` (/) ) )
34 14 19 33 ceqsexv2d 
 |-  E. y ( y R ( `' F ` Z ) /\ A. z -. z R y )
35 fvex 
 |-  ( `' F ` ( ( F ` y ) u. { y } ) ) e. _V
36 nfcv 
 |-  F/_ v y
37 nfcv 
 |-  F/_ v ( `' F ` ( ( F ` y ) u. { y } ) )
38 fveq2 
 |-  ( v = y -> ( F ` v ) = ( F ` y ) )
39 sneq 
 |-  ( v = y -> { v } = { y } )
40 38 39 uneq12d 
 |-  ( v = y -> ( ( F ` v ) u. { v } ) = ( ( F ` y ) u. { y } ) )
41 40 fveq2d 
 |-  ( v = y -> ( `' F ` ( ( F ` v ) u. { v } ) ) = ( `' F ` ( ( F ` y ) u. { y } ) ) )
42 36 37 3 41 orbitclmpt 
 |-  ( ( y e. Z /\ ( `' F ` ( ( F ` y ) u. { y } ) ) e. _V ) -> ( `' F ` ( ( F ` y ) u. { y } ) ) e. Z )
43 35 42 mpan2 
 |-  ( y e. Z -> ( `' F ` ( ( F ` y ) u. { y } ) ) e. Z )
44 vex 
 |-  y e. _V
45 1 2 44 24 brpermmodelcnv 
 |-  ( y R ( `' F ` Z ) <-> y e. Z )
46 1 2 35 24 brpermmodelcnv 
 |-  ( ( `' F ` ( ( F ` y ) u. { y } ) ) R ( `' F ` Z ) <-> ( `' F ` ( ( F ` y ) u. { y } ) ) e. Z )
47 43 45 46 3imtr4i 
 |-  ( y R ( `' F ` Z ) -> ( `' F ` ( ( F ` y ) u. { y } ) ) R ( `' F ` Z ) )
48 vex 
 |-  w e. _V
49 fvex 
 |-  ( F ` y ) e. _V
50 vsnex 
 |-  { y } e. _V
51 49 50 unex 
 |-  ( ( F ` y ) u. { y } ) e. _V
52 1 2 48 51 brpermmodelcnv 
 |-  ( w R ( `' F ` ( ( F ` y ) u. { y } ) ) <-> w e. ( ( F ` y ) u. { y } ) )
53 elun 
 |-  ( w e. ( ( F ` y ) u. { y } ) <-> ( w e. ( F ` y ) \/ w e. { y } ) )
54 1 2 48 44 brpermmodel 
 |-  ( w R y <-> w e. ( F ` y ) )
55 54 bicomi 
 |-  ( w e. ( F ` y ) <-> w R y )
56 velsn 
 |-  ( w e. { y } <-> w = y )
57 55 56 orbi12i 
 |-  ( ( w e. ( F ` y ) \/ w e. { y } ) <-> ( w R y \/ w = y ) )
58 52 53 57 3bitri 
 |-  ( w R ( `' F ` ( ( F ` y ) u. { y } ) ) <-> ( w R y \/ w = y ) )
59 58 ax-gen 
 |-  A. w ( w R ( `' F ` ( ( F ` y ) u. { y } ) ) <-> ( w R y \/ w = y ) )
60 breq1 
 |-  ( z = ( `' F ` ( ( F ` y ) u. { y } ) ) -> ( z R ( `' F ` Z ) <-> ( `' F ` ( ( F ` y ) u. { y } ) ) R ( `' F ` Z ) ) )
61 breq2 
 |-  ( z = ( `' F ` ( ( F ` y ) u. { y } ) ) -> ( w R z <-> w R ( `' F ` ( ( F ` y ) u. { y } ) ) ) )
62 61 bibi1d 
 |-  ( z = ( `' F ` ( ( F ` y ) u. { y } ) ) -> ( ( w R z <-> ( w R y \/ w = y ) ) <-> ( w R ( `' F ` ( ( F ` y ) u. { y } ) ) <-> ( w R y \/ w = y ) ) ) )
63 62 albidv 
 |-  ( z = ( `' F ` ( ( F ` y ) u. { y } ) ) -> ( A. w ( w R z <-> ( w R y \/ w = y ) ) <-> A. w ( w R ( `' F ` ( ( F ` y ) u. { y } ) ) <-> ( w R y \/ w = y ) ) ) )
64 60 63 anbi12d 
 |-  ( z = ( `' F ` ( ( F ` y ) u. { y } ) ) -> ( ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) <-> ( ( `' F ` ( ( F ` y ) u. { y } ) ) R ( `' F ` Z ) /\ A. w ( w R ( `' F ` ( ( F ` y ) u. { y } ) ) <-> ( w R y \/ w = y ) ) ) ) )
65 35 64 spcev 
 |-  ( ( ( `' F ` ( ( F ` y ) u. { y } ) ) R ( `' F ` Z ) /\ A. w ( w R ( `' F ` ( ( F ` y ) u. { y } ) ) <-> ( w R y \/ w = y ) ) ) -> E. z ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) )
66 47 59 65 sylancl 
 |-  ( y R ( `' F ` Z ) -> E. z ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) )
67 66 ax-gen 
 |-  A. y ( y R ( `' F ` Z ) -> E. z ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) )
68 34 67 pm3.2i 
 |-  ( E. y ( y R ( `' F ` Z ) /\ A. z -. z R y ) /\ A. y ( y R ( `' F ` Z ) -> E. z ( z R ( `' F ` Z ) /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) )
69 4 13 68 ceqsexv2d 
 |-  E. x ( E. y ( y R x /\ A. z -. z R y ) /\ A. y ( y R x -> E. z ( z R x /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) )