Metamath Proof Explorer

Theorem onf1oracwevd

Description: If F maps the proper class W one-to-one into the ordinals or H maps the ordinals one-to-one into the proper class W , and if every set can either be mapped one-to-one into the ordinals or have the ordinals mapped one-to-one into it, then R well-orders the universe. This is the ZFC version of (9 -> 3) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first two hypotheses would be replaced by something like ( ph -> A. X ( E. F F : X -1-1-> On \/ E. H H : On -1-1-> X ) ) . However, we cannot quantify over classes, so we split this into the case where X is a set and the case where X is the proper class W which together are sufficient for this proof. (Contributed by BTernaryTau, 16-Sep-2026)

Ref Expression
Hypotheses onf1oracwevd.1 
|- ( ph -> ( F : W -1-1-> On \/ H : On -1-1-> W ) )
onf1oracwevd.2 
|- ( ph -> A. v ( E. f f : v -1-1-> On \/ E. h h : On -1-1-> v ) )
onf1oracwevd.3 
|- W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
onf1oracwevd.4 
|- R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y A z ) ) }
onf1oracwevd.5 
|- A = ( I ` |^| { w e. On | ( I ` w ) We ( R1 ` suc ( rank ` y ) ) } )
onf1oracwevd.6 
|- I = if ( F : W -1-1-> On , `' F , H )
Assertion onf1oracwevd 
|- ( ph -> R We _V )

Proof

Step Hyp Ref Expression
1 onf1oracwevd.1 
 |-  ( ph -> ( F : W -1-1-> On \/ H : On -1-1-> W ) )
2 onf1oracwevd.2 
 |-  ( ph -> A. v ( E. f f : v -1-1-> On \/ E. h h : On -1-1-> v ) )
3 onf1oracwevd.3 
 |-  W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
4 onf1oracwevd.4 
 |-  R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y A z ) ) }
5 onf1oracwevd.5 
 |-  A = ( I ` |^| { w e. On | ( I ` w ) We ( R1 ` suc ( rank ` y ) ) } )
6 onf1oracwevd.6 
 |-  I = if ( F : W -1-1-> On , `' F , H )
7 simpr 
 |-  ( ( ph /\ F : W -1-1-> On ) -> F : W -1-1-> On )
8 7 a1d 
 |-  ( ( ph /\ F : W -1-1-> On ) -> ( -. W e. _V -> F : W -1-1-> On ) )
9 onprc 
 |-  -. On e. _V
10 f1dmex 
 |-  ( ( h : On -1-1-> v /\ v e. _V ) -> On e. _V )
11 10 elvd 
 |-  ( h : On -1-1-> v -> On e. _V )
12 9 11 mto 
 |-  -. h : On -1-1-> v
13 12 nex 
 |-  -. E. h h : On -1-1-> v
14 orel2 
 |-  ( -. E. h h : On -1-1-> v -> ( ( E. f f : v -1-1-> On \/ E. h h : On -1-1-> v ) -> E. f f : v -1-1-> On ) )
15 13 14 ax-mp 
 |-  ( ( E. f f : v -1-1-> On \/ E. h h : On -1-1-> v ) -> E. f f : v -1-1-> On )
16 2 15 sylg 
 |-  ( ph -> A. v E. f f : v -1-1-> On )
17 dfac15 
 |-  ( CHOICE <-> A. v E. f f : v -1-1-> On )
18 16 17 sylibr 
 |-  ( ph -> CHOICE )
19 18 adantr 
 |-  ( ( ph /\ F : W -1-1-> On ) -> CHOICE )
20 eqid 
 |-  { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) } = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) }
21 eqid 
 |-  ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) = ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
22 8 19 3 20 21 prconf1acwevd 
 |-  ( ( ph /\ F : W -1-1-> On ) -> { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) } We _V )
23 iftrue 
 |-  ( F : W -1-1-> On -> if ( F : W -1-1-> On , `' F , H ) = `' F )
24 6 23 eqtrid 
 |-  ( F : W -1-1-> On -> I = `' F )
25 24 fveq1d 
 |-  ( F : W -1-1-> On -> ( I ` w ) = ( `' F ` w ) )
26 eqidd 
 |-  ( F : W -1-1-> On -> ( R1 ` suc ( rank ` y ) ) = ( R1 ` suc ( rank ` y ) ) )
27 25 26 weeq12d 
 |-  ( F : W -1-1-> On -> ( ( I ` w ) We ( R1 ` suc ( rank ` y ) ) <-> ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) ) )
28 27 rabbidv 
 |-  ( F : W -1-1-> On -> { w e. On | ( I ` w ) We ( R1 ` suc ( rank ` y ) ) } = { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
29 28 inteqd 
 |-  ( F : W -1-1-> On -> |^| { w e. On | ( I ` w ) We ( R1 ` suc ( rank ` y ) ) } = |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
30 24 29 fveq12d 
 |-  ( F : W -1-1-> On -> ( I ` |^| { w e. On | ( I ` w ) We ( R1 ` suc ( rank ` y ) ) } ) = ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) )
31 5 30 eqtrid 
 |-  ( F : W -1-1-> On -> A = ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) )
32 31 breqd 
 |-  ( F : W -1-1-> On -> ( y A z <-> y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) )
33 32 anbi2d 
 |-  ( F : W -1-1-> On -> ( ( ( rank ` y ) = ( rank ` z ) /\ y A z ) <-> ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) )
34 33 orbi2d 
 |-  ( F : W -1-1-> On -> ( ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y A z ) ) <-> ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) ) )
35 34 opabbidv 
 |-  ( F : W -1-1-> On -> { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y A z ) ) } = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) } )
36 4 35 eqtrid 
 |-  ( F : W -1-1-> On -> R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) } )
37 eqidd 
 |-  ( F : W -1-1-> On -> _V = _V )
38 36 37 weeq12d 
 |-  ( F : W -1-1-> On -> ( R We _V <-> { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) } We _V ) )
39 38 adantl 
 |-  ( ( ph /\ F : W -1-1-> On ) -> ( R We _V <-> { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) z ) ) } We _V ) )
40 22 39 mpbird 
 |-  ( ( ph /\ F : W -1-1-> On ) -> R We _V )
41 1 orcanai 
 |-  ( ( ph /\ -. F : W -1-1-> On ) -> H : On -1-1-> W )
42 iffalse 
 |-  ( -. F : W -1-1-> On -> if ( F : W -1-1-> On , `' F , H ) = H )
43 6 42 eqtrid 
 |-  ( -. F : W -1-1-> On -> I = H )
44 f1eq1 
 |-  ( I = H -> ( I : On -1-1-> W <-> H : On -1-1-> W ) )
45 43 44 syl 
 |-  ( -. F : W -1-1-> On -> ( I : On -1-1-> W <-> H : On -1-1-> W ) )
46 45 adantl 
 |-  ( ( ph /\ -. F : W -1-1-> On ) -> ( I : On -1-1-> W <-> H : On -1-1-> W ) )
47 41 46 mpbird 
 |-  ( ( ph /\ -. F : W -1-1-> On ) -> I : On -1-1-> W )
48 47 a1d 
 |-  ( ( ph /\ -. F : W -1-1-> On ) -> ( -. W e. _V -> I : On -1-1-> W ) )
49 18 adantr 
 |-  ( ( ph /\ -. F : W -1-1-> On ) -> CHOICE )
50 48 49 3 4 5 onprcf1acwevd 
 |-  ( ( ph /\ -. F : W -1-1-> On ) -> R We _V )
51 40 50 pm2.61dan 
 |-  ( ph -> R We _V )