Metamath Proof Explorer

Theorem onvfowev

Description: If F maps the ordinals onto the universe, then R well-orders the universe. This is the ZFC version of (8 -> 3) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the antecedent would be something like A. X ( X =/= (/) -> E. F F : On -onto-> X ) , but since we cannot quantify over classes, we instead consider only the case X = _V which is sufficient for this proof. (Contributed by BTernaryTau, 12-Jun-2026)

Ref Expression
Hypotheses onvfowev.1 
|- R = { <. x , y >. | ( H ` x ) e. ( H ` y ) }
onvfowev.2 
|- H = ( z e. _V |-> |^| ( `' F " { z } ) )
Assertion onvfowev 
|- ( F : On -onto-> _V -> R We _V )

Proof

Step Hyp Ref Expression
1 onvfowev.1 
 |-  R = { <. x , y >. | ( H ` x ) e. ( H ` y ) }
2 onvfowev.2 
 |-  H = ( z e. _V |-> |^| ( `' F " { z } ) )
3 cnvimass 
 |-  ( `' F " { z } ) C_ dom F
4 fofn 
 |-  ( F : On -onto-> _V -> F Fn On )
5 4 fndmd 
 |-  ( F : On -onto-> _V -> dom F = On )
6 3 5 sseqtrid 
 |-  ( F : On -onto-> _V -> ( `' F " { z } ) C_ On )
7 vex 
 |-  z e. _V
8 forn 
 |-  ( F : On -onto-> _V -> ran F = _V )
9 7 8 eleqtrrid 
 |-  ( F : On -onto-> _V -> z e. ran F )
10 inisegn0 
 |-  ( z e. ran F <-> ( `' F " { z } ) =/= (/) )
11 9 10 sylib 
 |-  ( F : On -onto-> _V -> ( `' F " { z } ) =/= (/) )
12 oninton 
 |-  ( ( ( `' F " { z } ) C_ On /\ ( `' F " { z } ) =/= (/) ) -> |^| ( `' F " { z } ) e. On )
13 6 11 12 syl2anc 
 |-  ( F : On -onto-> _V -> |^| ( `' F " { z } ) e. On )
14 13 adantr 
 |-  ( ( F : On -onto-> _V /\ z e. _V ) -> |^| ( `' F " { z } ) e. On )
15 14 2 fmptd 
 |-  ( F : On -onto-> _V -> H : _V --> On )
16 fofun 
 |-  ( F : On -onto-> _V -> Fun F )
17 fvexd 
 |-  ( ( F : On -onto-> _V /\ ( H ` v ) = ( H ` w ) ) -> ( H ` v ) e. _V )
18 vex 
 |-  w e. _V
19 18 a1i 
 |-  ( F : On -onto-> _V -> w e. _V )
20 13 adantr 
 |-  ( ( F : On -onto-> _V /\ z = w ) -> |^| ( `' F " { z } ) e. On )
21 sneq 
 |-  ( z = w -> { z } = { w } )
22 21 imaeq2d 
 |-  ( z = w -> ( `' F " { z } ) = ( `' F " { w } ) )
23 22 inteqd 
 |-  ( z = w -> |^| ( `' F " { z } ) = |^| ( `' F " { w } ) )
24 23 adantl 
 |-  ( ( F : On -onto-> _V /\ z = w ) -> |^| ( `' F " { z } ) = |^| ( `' F " { w } ) )
25 19 20 24 fvmptdv2 
 |-  ( F : On -onto-> _V -> ( H = ( z e. _V |-> |^| ( `' F " { z } ) ) -> ( H ` w ) = |^| ( `' F " { w } ) ) )
26 2 25 mpi 
 |-  ( F : On -onto-> _V -> ( H ` w ) = |^| ( `' F " { w } ) )
27 cnvimass 
 |-  ( `' F " { w } ) C_ dom F
28 27 5 sseqtrid 
 |-  ( F : On -onto-> _V -> ( `' F " { w } ) C_ On )
29 18 8 eleqtrrid 
 |-  ( F : On -onto-> _V -> w e. ran F )
30 inisegn0 
 |-  ( w e. ran F <-> ( `' F " { w } ) =/= (/) )
31 29 30 sylib 
 |-  ( F : On -onto-> _V -> ( `' F " { w } ) =/= (/) )
32 onint 
 |-  ( ( ( `' F " { w } ) C_ On /\ ( `' F " { w } ) =/= (/) ) -> |^| ( `' F " { w } ) e. ( `' F " { w } ) )
33 28 31 32 syl2anc 
 |-  ( F : On -onto-> _V -> |^| ( `' F " { w } ) e. ( `' F " { w } ) )
34 26 33 eqeltrd 
 |-  ( F : On -onto-> _V -> ( H ` w ) e. ( `' F " { w } ) )
35 eleq1 
 |-  ( ( H ` v ) = ( H ` w ) -> ( ( H ` v ) e. ( `' F " { w } ) <-> ( H ` w ) e. ( `' F " { w } ) ) )
36 34 35 syl5ibrcom 
 |-  ( F : On -onto-> _V -> ( ( H ` v ) = ( H ` w ) -> ( H ` v ) e. ( `' F " { w } ) ) )
37 vex 
 |-  v e. _V
38 37 a1i 
 |-  ( F : On -onto-> _V -> v e. _V )
39 13 adantr 
 |-  ( ( F : On -onto-> _V /\ z = v ) -> |^| ( `' F " { z } ) e. On )
40 sneq 
 |-  ( z = v -> { z } = { v } )
41 40 imaeq2d 
 |-  ( z = v -> ( `' F " { z } ) = ( `' F " { v } ) )
42 41 inteqd 
 |-  ( z = v -> |^| ( `' F " { z } ) = |^| ( `' F " { v } ) )
43 42 adantl 
 |-  ( ( F : On -onto-> _V /\ z = v ) -> |^| ( `' F " { z } ) = |^| ( `' F " { v } ) )
44 38 39 43 fvmptdv2 
 |-  ( F : On -onto-> _V -> ( H = ( z e. _V |-> |^| ( `' F " { z } ) ) -> ( H ` v ) = |^| ( `' F " { v } ) ) )
45 2 44 mpi 
 |-  ( F : On -onto-> _V -> ( H ` v ) = |^| ( `' F " { v } ) )
46 cnvimass 
 |-  ( `' F " { v } ) C_ dom F
47 46 5 sseqtrid 
 |-  ( F : On -onto-> _V -> ( `' F " { v } ) C_ On )
48 37 8 eleqtrrid 
 |-  ( F : On -onto-> _V -> v e. ran F )
49 inisegn0 
 |-  ( v e. ran F <-> ( `' F " { v } ) =/= (/) )
50 48 49 sylib 
 |-  ( F : On -onto-> _V -> ( `' F " { v } ) =/= (/) )
51 onint 
 |-  ( ( ( `' F " { v } ) C_ On /\ ( `' F " { v } ) =/= (/) ) -> |^| ( `' F " { v } ) e. ( `' F " { v } ) )
52 47 50 51 syl2anc 
 |-  ( F : On -onto-> _V -> |^| ( `' F " { v } ) e. ( `' F " { v } ) )
53 45 52 eqeltrd 
 |-  ( F : On -onto-> _V -> ( H ` v ) e. ( `' F " { v } ) )
54 36 53 jctild 
 |-  ( F : On -onto-> _V -> ( ( H ` v ) = ( H ` w ) -> ( ( H ` v ) e. ( `' F " { v } ) /\ ( H ` v ) e. ( `' F " { w } ) ) ) )
55 54 imp 
 |-  ( ( F : On -onto-> _V /\ ( H ` v ) = ( H ` w ) ) -> ( ( H ` v ) e. ( `' F " { v } ) /\ ( H ` v ) e. ( `' F " { w } ) ) )
56 eleq1 
 |-  ( u = ( H ` v ) -> ( u e. ( `' F " { v } ) <-> ( H ` v ) e. ( `' F " { v } ) ) )
57 eleq1 
 |-  ( u = ( H ` v ) -> ( u e. ( `' F " { w } ) <-> ( H ` v ) e. ( `' F " { w } ) ) )
58 56 57 anbi12d 
 |-  ( u = ( H ` v ) -> ( ( u e. ( `' F " { v } ) /\ u e. ( `' F " { w } ) ) <-> ( ( H ` v ) e. ( `' F " { v } ) /\ ( H ` v ) e. ( `' F " { w } ) ) ) )
59 17 55 58 spcedv 
 |-  ( ( F : On -onto-> _V /\ ( H ` v ) = ( H ` w ) ) -> E. u ( u e. ( `' F " { v } ) /\ u e. ( `' F " { w } ) ) )
60 59 ex 
 |-  ( F : On -onto-> _V -> ( ( H ` v ) = ( H ` w ) -> E. u ( u e. ( `' F " { v } ) /\ u e. ( `' F " { w } ) ) ) )
61 elinisegg 
 |-  ( ( v e. _V /\ u e. _V ) -> ( u e. ( `' F " { v } ) <-> u F v ) )
62 61 el2v 
 |-  ( u e. ( `' F " { v } ) <-> u F v )
63 elinisegg 
 |-  ( ( w e. _V /\ u e. _V ) -> ( u e. ( `' F " { w } ) <-> u F w ) )
64 63 el2v 
 |-  ( u e. ( `' F " { w } ) <-> u F w )
65 62 64 anbi12i 
 |-  ( ( u e. ( `' F " { v } ) /\ u e. ( `' F " { w } ) ) <-> ( u F v /\ u F w ) )
66 65 exbii 
 |-  ( E. u ( u e. ( `' F " { v } ) /\ u e. ( `' F " { w } ) ) <-> E. u ( u F v /\ u F w ) )
67 60 66 imbitrdi 
 |-  ( F : On -onto-> _V -> ( ( H ` v ) = ( H ` w ) -> E. u ( u F v /\ u F w ) ) )
68 funeu 
 |-  ( ( Fun F /\ u F v ) -> E! v u F v )
69 68 3adant3 
 |-  ( ( Fun F /\ u F v /\ u F w ) -> E! v u F v )
70 3simpc 
 |-  ( ( Fun F /\ u F v /\ u F w ) -> ( u F v /\ u F w ) )
71 breq2 
 |-  ( v = w -> ( u F v <-> u F w ) )
72 71 eu4 
 |-  ( E! v u F v <-> ( E. v u F v /\ A. v A. w ( ( u F v /\ u F w ) -> v = w ) ) )
73 72 simprbi 
 |-  ( E! v u F v -> A. v A. w ( ( u F v /\ u F w ) -> v = w ) )
74 73 19.21bbi 
 |-  ( E! v u F v -> ( ( u F v /\ u F w ) -> v = w ) )
75 69 70 74 sylc 
 |-  ( ( Fun F /\ u F v /\ u F w ) -> v = w )
76 75 3expib 
 |-  ( Fun F -> ( ( u F v /\ u F w ) -> v = w ) )
77 76 exlimdv 
 |-  ( Fun F -> ( E. u ( u F v /\ u F w ) -> v = w ) )
78 16 67 77 sylsyld 
 |-  ( F : On -onto-> _V -> ( ( H ` v ) = ( H ` w ) -> v = w ) )
79 78 ralrimivw 
 |-  ( F : On -onto-> _V -> A. w e. _V ( ( H ` v ) = ( H ` w ) -> v = w ) )
80 79 ralrimivw 
 |-  ( F : On -onto-> _V -> A. v e. _V A. w e. _V ( ( H ` v ) = ( H ` w ) -> v = w ) )
81 dff13 
 |-  ( H : _V -1-1-> On <-> ( H : _V --> On /\ A. v e. _V A. w e. _V ( ( H ` v ) = ( H ` w ) -> v = w ) ) )
82 15 80 81 sylanbrc 
 |-  ( F : On -onto-> _V -> H : _V -1-1-> On )
83 1 vonf1wev 
 |-  ( H : _V -1-1-> On -> R We _V )
84 82 83 syl 
 |-  ( F : On -onto-> _V -> R We _V )