Metamath Proof Explorer

Theorem onvf1odlem4

Description: Lemma for onvf1od . If the range of F does not exist, then it must equal the universe. (Contributed by BTernaryTau, 4-Dec-2025)

Ref Expression
Hypotheses onvf1odlem4.1 
|- ( ph -> A. z ( z =/= (/) -> ( G ` z ) e. z ) )
onvf1odlem4.2 
|- M = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. ran w }
onvf1odlem4.3 
|- N = ( G ` ( ( R1 ` M ) \ ran w ) )
onvf1odlem4.4 
|- F = recs ( ( w e. _V |-> N ) )
onvf1odlem4.5 
|- B = |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) }
onvf1odlem4.6 
|- C = ( G ` ( ( R1 ` B ) \ ( F " t ) ) )
Assertion onvf1odlem4 
|- ( ph -> ( -. ran F e. _V -> ran F = _V ) )

Proof

Step Hyp Ref Expression
1 onvf1odlem4.1 
 |-  ( ph -> A. z ( z =/= (/) -> ( G ` z ) e. z ) )
2 onvf1odlem4.2 
 |-  M = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. ran w }
3 onvf1odlem4.3 
 |-  N = ( G ` ( ( R1 ` M ) \ ran w ) )
4 onvf1odlem4.4 
 |-  F = recs ( ( w e. _V |-> N ) )
5 onvf1odlem4.5 
 |-  B = |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) }
6 onvf1odlem4.6 
 |-  C = ( G ` ( ( R1 ` B ) \ ( F " t ) ) )
7 eqv 
 |-  ( ran F = _V <-> A. v v e. ran F )
8 exnal 
 |-  ( E. v -. v e. ran F <-> -. A. v v e. ran F )
9 4 tfr1 
 |-  F Fn On
10 fvelrnb 
 |-  ( F Fn On -> ( s e. ran F <-> E. t e. On ( F ` t ) = s ) )
11 9 10 ax-mp 
 |-  ( s e. ran F <-> E. t e. On ( F ` t ) = s )
12 2 3 4 5 6 onvf1odlem3 
 |-  ( t e. On -> ( F ` t ) = C )
13 12 adantl 
 |-  ( ( ph /\ t e. On ) -> ( F ` t ) = C )
14 fnfun 
 |-  ( F Fn On -> Fun F )
15 9 14 ax-mp 
 |-  Fun F
16 vex 
 |-  t e. _V
17 16 funimaex 
 |-  ( Fun F -> ( F " t ) e. _V )
18 15 17 ax-mp 
 |-  ( F " t ) e. _V
19 1 5 6 onvf1odlem2 
 |-  ( ph -> ( ( F " t ) e. _V -> C e. ( ( R1 ` B ) \ ( F " t ) ) ) )
20 18 19 mpi 
 |-  ( ph -> C e. ( ( R1 ` B ) \ ( F " t ) ) )
21 20 eldifad 
 |-  ( ph -> C e. ( R1 ` B ) )
22 21 adantr 
 |-  ( ( ph /\ t e. On ) -> C e. ( R1 ` B ) )
23 13 22 eqeltrd 
 |-  ( ( ph /\ t e. On ) -> ( F ` t ) e. ( R1 ` B ) )
24 rankr1ai 
 |-  ( ( F ` t ) e. ( R1 ` B ) -> ( rank ` ( F ` t ) ) e. B )
25 onvf1odlem1 
 |-  ( ( F " t ) e. _V -> E. u e. On E. v e. ( R1 ` u ) -. v e. ( F " t ) )
26 18 25 ax-mp 
 |-  E. u e. On E. v e. ( R1 ` u ) -. v e. ( F " t )
27 onintrab2 
 |-  ( E. u e. On E. v e. ( R1 ` u ) -. v e. ( F " t ) <-> |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } e. On )
28 5 eleq1i 
 |-  ( B e. On <-> |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } e. On )
29 27 28 bitr4i 
 |-  ( E. u e. On E. v e. ( R1 ` u ) -. v e. ( F " t ) <-> B e. On )
30 26 29 mpbi 
 |-  B e. On
31 30 oneli 
 |-  ( ( rank ` ( F ` t ) ) e. B -> ( rank ` ( F ` t ) ) e. On )
32 fveq2 
 |-  ( u = ( rank ` ( F ` t ) ) -> ( R1 ` u ) = ( R1 ` ( rank ` ( F ` t ) ) ) )
33 32 rexeqdv 
 |-  ( u = ( rank ` ( F ` t ) ) -> ( E. v e. ( R1 ` u ) -. v e. ( F " t ) <-> E. v e. ( R1 ` ( rank ` ( F ` t ) ) ) -. v e. ( F " t ) ) )
34 33 onnminsb 
 |-  ( ( rank ` ( F ` t ) ) e. On -> ( ( rank ` ( F ` t ) ) e. |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } -> -. E. v e. ( R1 ` ( rank ` ( F ` t ) ) ) -. v e. ( F " t ) ) )
35 5 eleq2i 
 |-  ( ( rank ` ( F ` t ) ) e. B <-> ( rank ` ( F ` t ) ) e. |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } )
36 dfral2 
 |-  ( A. v e. ( R1 ` ( rank ` ( F ` t ) ) ) v e. ( F " t ) <-> -. E. v e. ( R1 ` ( rank ` ( F ` t ) ) ) -. v e. ( F " t ) )
37 34 35 36 3imtr4g 
 |-  ( ( rank ` ( F ` t ) ) e. On -> ( ( rank ` ( F ` t ) ) e. B -> A. v e. ( R1 ` ( rank ` ( F ` t ) ) ) v e. ( F " t ) ) )
38 31 37 mpcom 
 |-  ( ( rank ` ( F ` t ) ) e. B -> A. v e. ( R1 ` ( rank ` ( F ` t ) ) ) v e. ( F " t ) )
39 imassrn 
 |-  ( F " t ) C_ ran F
40 39 sseli 
 |-  ( v e. ( F " t ) -> v e. ran F )
41 40 ralimi 
 |-  ( A. v e. ( R1 ` ( rank ` ( F ` t ) ) ) v e. ( F " t ) -> A. v e. ( R1 ` ( rank ` ( F ` t ) ) ) v e. ran F )
42 38 41 syl 
 |-  ( ( rank ` ( F ` t ) ) e. B -> A. v e. ( R1 ` ( rank ` ( F ` t ) ) ) v e. ran F )
43 23 24 42 3syl 
 |-  ( ( ph /\ t e. On ) -> A. v e. ( R1 ` ( rank ` ( F ` t ) ) ) v e. ran F )
44 2fveq3 
 |-  ( ( F ` t ) = s -> ( R1 ` ( rank ` ( F ` t ) ) ) = ( R1 ` ( rank ` s ) ) )
45 44 raleqdv 
 |-  ( ( F ` t ) = s -> ( A. v e. ( R1 ` ( rank ` ( F ` t ) ) ) v e. ran F <-> A. v e. ( R1 ` ( rank ` s ) ) v e. ran F ) )
46 43 45 syl5ibcom 
 |-  ( ( ph /\ t e. On ) -> ( ( F ` t ) = s -> A. v e. ( R1 ` ( rank ` s ) ) v e. ran F ) )
47 46 rexlimdva 
 |-  ( ph -> ( E. t e. On ( F ` t ) = s -> A. v e. ( R1 ` ( rank ` s ) ) v e. ran F ) )
48 11 47 biimtrid 
 |-  ( ph -> ( s e. ran F -> A. v e. ( R1 ` ( rank ` s ) ) v e. ran F ) )
49 48 imp 
 |-  ( ( ph /\ s e. ran F ) -> A. v e. ( R1 ` ( rank ` s ) ) v e. ran F )
50 df-ral 
 |-  ( A. v e. ( R1 ` ( rank ` s ) ) v e. ran F <-> A. v ( v e. ( R1 ` ( rank ` s ) ) -> v e. ran F ) )
51 49 50 sylib 
 |-  ( ( ph /\ s e. ran F ) -> A. v ( v e. ( R1 ` ( rank ` s ) ) -> v e. ran F ) )
52 51 19.21bi 
 |-  ( ( ph /\ s e. ran F ) -> ( v e. ( R1 ` ( rank ` s ) ) -> v e. ran F ) )
53 52 con3d 
 |-  ( ( ph /\ s e. ran F ) -> ( -. v e. ran F -> -. v e. ( R1 ` ( rank ` s ) ) ) )
54 rankon 
 |-  ( rank ` s ) e. On
55 vex 
 |-  v e. _V
56 55 ssrankr1 
 |-  ( ( rank ` s ) e. On -> ( ( rank ` s ) C_ ( rank ` v ) <-> -. v e. ( R1 ` ( rank ` s ) ) ) )
57 54 56 ax-mp 
 |-  ( ( rank ` s ) C_ ( rank ` v ) <-> -. v e. ( R1 ` ( rank ` s ) ) )
58 53 57 imbitrrdi 
 |-  ( ( ph /\ s e. ran F ) -> ( -. v e. ran F -> ( rank ` s ) C_ ( rank ` v ) ) )
59 58 impancom 
 |-  ( ( ph /\ -. v e. ran F ) -> ( s e. ran F -> ( rank ` s ) C_ ( rank ` v ) ) )
60 59 ralrimiv 
 |-  ( ( ph /\ -. v e. ran F ) -> A. s e. ran F ( rank ` s ) C_ ( rank ` v ) )
61 rankon 
 |-  ( rank ` v ) e. On
62 sseq2 
 |-  ( r = ( rank ` v ) -> ( ( rank ` s ) C_ r <-> ( rank ` s ) C_ ( rank ` v ) ) )
63 62 ralbidv 
 |-  ( r = ( rank ` v ) -> ( A. s e. ran F ( rank ` s ) C_ r <-> A. s e. ran F ( rank ` s ) C_ ( rank ` v ) ) )
64 63 rspcev 
 |-  ( ( ( rank ` v ) e. On /\ A. s e. ran F ( rank ` s ) C_ ( rank ` v ) ) -> E. r e. On A. s e. ran F ( rank ` s ) C_ r )
65 61 64 mpan 
 |-  ( A. s e. ran F ( rank ` s ) C_ ( rank ` v ) -> E. r e. On A. s e. ran F ( rank ` s ) C_ r )
66 bndrank 
 |-  ( E. r e. On A. s e. ran F ( rank ` s ) C_ r -> ran F e. _V )
67 60 65 66 3syl 
 |-  ( ( ph /\ -. v e. ran F ) -> ran F e. _V )
68 67 expcom 
 |-  ( -. v e. ran F -> ( ph -> ran F e. _V ) )
69 68 exlimiv 
 |-  ( E. v -. v e. ran F -> ( ph -> ran F e. _V ) )
70 8 69 sylbir 
 |-  ( -. A. v v e. ran F -> ( ph -> ran F e. _V ) )
71 7 70 sylnbi 
 |-  ( -. ran F = _V -> ( ph -> ran F e. _V ) )
72 71 com12 
 |-  ( ph -> ( -. ran F = _V -> ran F e. _V ) )
73 72 con1d 
 |-  ( ph -> ( -. ran F e. _V -> ran F = _V ) )