Metamath Proof Explorer

Theorem prconf1acwevd

Description: If F maps the proper class W one-to-one into the ordinals and the Axiom of Choice holds, then R well-orders the universe. (Contributed by BTernaryTau, 16-Sep-2026)

Ref Expression
Hypotheses prconf1acwevd.1 
|- ( ph -> ( -. W e. _V -> F : W -1-1-> On ) )
prconf1acwevd.2 
|- ( ph -> CHOICE )
prconf1acwevd.3 
|- W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
prconf1acwevd.4 
|- R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y S z ) ) }
prconf1acwevd.5 
|- S = ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
Assertion prconf1acwevd 
|- ( ph -> R We _V )

Proof

Step Hyp Ref Expression
1 prconf1acwevd.1 
 |-  ( ph -> ( -. W e. _V -> F : W -1-1-> On ) )
2 prconf1acwevd.2 
 |-  ( ph -> CHOICE )
3 prconf1acwevd.3 
 |-  W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
4 prconf1acwevd.4 
 |-  R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y S z ) ) }
5 prconf1acwevd.5 
 |-  S = ( `' F ` |^| { w e. On | ( `' F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
6 3 acwer1prc 
 |-  ( CHOICE -> -. W e. _V )
7 2 6 syl 
 |-  ( ph -> -. W e. _V )
8 7 1 mpd 
 |-  ( ph -> F : W -1-1-> On )
9 f1f 
 |-  ( F : W -1-1-> On -> F : W --> On )
10 frn 
 |-  ( F : W --> On -> ran F C_ On )
11 8 9 10 3syl 
 |-  ( ph -> ran F C_ On )
12 11 adantr 
 |-  ( ( ph /\ v e. On ) -> ran F C_ On )
13 ssid 
 |-  W C_ W
14 3 onprcf1acwevdlem1 
 |-  ( ( W C_ W /\ v e. On /\ A. u e. W -. u We ( R1 ` v ) ) -> W e. _V )
15 13 14 mp3an1 
 |-  ( ( v e. On /\ A. u e. W -. u We ( R1 ` v ) ) -> W e. _V )
16 15 ex 
 |-  ( v e. On -> ( A. u e. W -. u We ( R1 ` v ) -> W e. _V ) )
17 16 7 nsyli 
 |-  ( v e. On -> ( ph -> -. A. u e. W -. u We ( R1 ` v ) ) )
18 17 impcom 
 |-  ( ( ph /\ v e. On ) -> -. A. u e. W -. u We ( R1 ` v ) )
19 dfrex2 
 |-  ( E. u e. W u We ( R1 ` v ) <-> -. A. u e. W -. u We ( R1 ` v ) )
20 18 19 sylibr 
 |-  ( ( ph /\ v e. On ) -> E. u e. W u We ( R1 ` v ) )
21 f1f1orn 
 |-  ( F : W -1-1-> On -> F : W -1-1-onto-> ran F )
22 f1ocnv 
 |-  ( F : W -1-1-onto-> ran F -> `' F : ran F -1-1-onto-> W )
23 8 21 22 3syl 
 |-  ( ph -> `' F : ran F -1-1-onto-> W )
24 f1ofo 
 |-  ( `' F : ran F -1-1-onto-> W -> `' F : ran F -onto-> W )
25 forn 
 |-  ( `' F : ran F -onto-> W -> ran `' F = W )
26 23 24 25 3syl 
 |-  ( ph -> ran `' F = W )
27 26 rexeqdv 
 |-  ( ph -> ( E. u e. ran `' F u We ( R1 ` v ) <-> E. u e. W u We ( R1 ` v ) ) )
28 f1ofn 
 |-  ( `' F : ran F -1-1-onto-> W -> `' F Fn ran F )
29 weeq1 
 |-  ( u = ( `' F ` w ) -> ( u We ( R1 ` v ) <-> ( `' F ` w ) We ( R1 ` v ) ) )
30 29 rexrn 
 |-  ( `' F Fn ran F -> ( E. u e. ran `' F u We ( R1 ` v ) <-> E. w e. ran F ( `' F ` w ) We ( R1 ` v ) ) )
31 23 28 30 3syl 
 |-  ( ph -> ( E. u e. ran `' F u We ( R1 ` v ) <-> E. w e. ran F ( `' F ` w ) We ( R1 ` v ) ) )
32 27 31 bitr3d 
 |-  ( ph -> ( E. u e. W u We ( R1 ` v ) <-> E. w e. ran F ( `' F ` w ) We ( R1 ` v ) ) )
33 32 adantr 
 |-  ( ( ph /\ v e. On ) -> ( E. u e. W u We ( R1 ` v ) <-> E. w e. ran F ( `' F ` w ) We ( R1 ` v ) ) )
34 20 33 mpbid 
 |-  ( ( ph /\ v e. On ) -> E. w e. ran F ( `' F ` w ) We ( R1 ` v ) )
35 ssrexv 
 |-  ( ran F C_ On -> ( E. w e. ran F ( `' F ` w ) We ( R1 ` v ) -> E. w e. On ( `' F ` w ) We ( R1 ` v ) ) )
36 12 34 35 sylc 
 |-  ( ( ph /\ v e. On ) -> E. w e. On ( `' F ` w ) We ( R1 ` v ) )
37 4 5 36 onprcf1acwevdlem2 
 |-  ( ph -> R We _V )