Metamath Proof Explorer

Theorem vonf1owev

Description: If F is a bijection from the universe to the ordinals, then R well-orders the universe. This is the ZFC version of (2 -> 3) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 6-Dec-2025)

Ref Expression
Hypothesis vonf1owev.1 
|- R = { <. x , y >. | ( F ` x ) e. ( F ` y ) }
Assertion vonf1owev 
|- ( F : _V -1-1-onto-> On -> R We _V )

Proof

Step Hyp Ref Expression
1 vonf1owev.1 
 |-  R = { <. x , y >. | ( F ` x ) e. ( F ` y ) }
2 f1of 
 |-  ( F : _V -1-1-onto-> On -> F : _V --> On )
3 2 fimassd 
 |-  ( F : _V -1-1-onto-> On -> ( F " t ) C_ On )
4 f1odm 
 |-  ( F : _V -1-1-onto-> On -> dom F = _V )
5 4 ineq1d 
 |-  ( F : _V -1-1-onto-> On -> ( dom F i^i t ) = ( _V i^i t ) )
6 5 neeq1d 
 |-  ( F : _V -1-1-onto-> On -> ( ( dom F i^i t ) =/= (/) <-> ( _V i^i t ) =/= (/) ) )
7 inv1 
 |-  ( t i^i _V ) = t
8 7 ineqcomi 
 |-  ( _V i^i t ) = t
9 8 neeq1i 
 |-  ( ( _V i^i t ) =/= (/) <-> t =/= (/) )
10 6 9 bitr2di 
 |-  ( F : _V -1-1-onto-> On -> ( t =/= (/) <-> ( dom F i^i t ) =/= (/) ) )
11 10 biimpa 
 |-  ( ( F : _V -1-1-onto-> On /\ t =/= (/) ) -> ( dom F i^i t ) =/= (/) )
12 11 imadisjlnd 
 |-  ( ( F : _V -1-1-onto-> On /\ t =/= (/) ) -> ( F " t ) =/= (/) )
13 onssmin 
 |-  ( ( ( F " t ) C_ On /\ ( F " t ) =/= (/) ) -> E. r e. ( F " t ) A. s e. ( F " t ) r C_ s )
14 3 12 13 syl2an2r 
 |-  ( ( F : _V -1-1-onto-> On /\ t =/= (/) ) -> E. r e. ( F " t ) A. s e. ( F " t ) r C_ s )
15 14 ex 
 |-  ( F : _V -1-1-onto-> On -> ( t =/= (/) -> E. r e. ( F " t ) A. s e. ( F " t ) r C_ s ) )
16 vex 
 |-  v e. _V
17 vex 
 |-  u e. _V
18 fveq2 
 |-  ( x = v -> ( F ` x ) = ( F ` v ) )
19 18 eleq1d 
 |-  ( x = v -> ( ( F ` x ) e. ( F ` y ) <-> ( F ` v ) e. ( F ` y ) ) )
20 fveq2 
 |-  ( y = u -> ( F ` y ) = ( F ` u ) )
21 20 eleq2d 
 |-  ( y = u -> ( ( F ` v ) e. ( F ` y ) <-> ( F ` v ) e. ( F ` u ) ) )
22 16 17 19 21 1 brab 
 |-  ( v R u <-> ( F ` v ) e. ( F ` u ) )
23 22 notbii 
 |-  ( -. v R u <-> -. ( F ` v ) e. ( F ` u ) )
24 2 ffvelcdmda 
 |-  ( ( F : _V -1-1-onto-> On /\ u e. _V ) -> ( F ` u ) e. On )
25 24 elvd 
 |-  ( F : _V -1-1-onto-> On -> ( F ` u ) e. On )
26 2 ffvelcdmda 
 |-  ( ( F : _V -1-1-onto-> On /\ v e. _V ) -> ( F ` v ) e. On )
27 26 elvd 
 |-  ( F : _V -1-1-onto-> On -> ( F ` v ) e. On )
28 ontri1 
 |-  ( ( ( F ` u ) e. On /\ ( F ` v ) e. On ) -> ( ( F ` u ) C_ ( F ` v ) <-> -. ( F ` v ) e. ( F ` u ) ) )
29 25 27 28 syl2anc 
 |-  ( F : _V -1-1-onto-> On -> ( ( F ` u ) C_ ( F ` v ) <-> -. ( F ` v ) e. ( F ` u ) ) )
30 23 29 bitr4id 
 |-  ( F : _V -1-1-onto-> On -> ( -. v R u <-> ( F ` u ) C_ ( F ` v ) ) )
31 30 ralbidv 
 |-  ( F : _V -1-1-onto-> On -> ( A. v e. t -. v R u <-> A. v e. t ( F ` u ) C_ ( F ` v ) ) )
32 f1ofn 
 |-  ( F : _V -1-1-onto-> On -> F Fn _V )
33 ssv 
 |-  t C_ _V
34 sseq2 
 |-  ( s = ( F ` v ) -> ( ( F ` u ) C_ s <-> ( F ` u ) C_ ( F ` v ) ) )
35 34 ralima 
 |-  ( ( F Fn _V /\ t C_ _V ) -> ( A. s e. ( F " t ) ( F ` u ) C_ s <-> A. v e. t ( F ` u ) C_ ( F ` v ) ) )
36 32 33 35 sylancl 
 |-  ( F : _V -1-1-onto-> On -> ( A. s e. ( F " t ) ( F ` u ) C_ s <-> A. v e. t ( F ` u ) C_ ( F ` v ) ) )
37 31 36 bitr4d 
 |-  ( F : _V -1-1-onto-> On -> ( A. v e. t -. v R u <-> A. s e. ( F " t ) ( F ` u ) C_ s ) )
38 37 rexbidv 
 |-  ( F : _V -1-1-onto-> On -> ( E. u e. t A. v e. t -. v R u <-> E. u e. t A. s e. ( F " t ) ( F ` u ) C_ s ) )
39 sseq1 
 |-  ( r = ( F ` u ) -> ( r C_ s <-> ( F ` u ) C_ s ) )
40 39 ralbidv 
 |-  ( r = ( F ` u ) -> ( A. s e. ( F " t ) r C_ s <-> A. s e. ( F " t ) ( F ` u ) C_ s ) )
41 40 rexima 
 |-  ( ( F Fn _V /\ t C_ _V ) -> ( E. r e. ( F " t ) A. s e. ( F " t ) r C_ s <-> E. u e. t A. s e. ( F " t ) ( F ` u ) C_ s ) )
42 32 33 41 sylancl 
 |-  ( F : _V -1-1-onto-> On -> ( E. r e. ( F " t ) A. s e. ( F " t ) r C_ s <-> E. u e. t A. s e. ( F " t ) ( F ` u ) C_ s ) )
43 38 42 bitr4d 
 |-  ( F : _V -1-1-onto-> On -> ( E. u e. t A. v e. t -. v R u <-> E. r e. ( F " t ) A. s e. ( F " t ) r C_ s ) )
44 15 43 sylibrd 
 |-  ( F : _V -1-1-onto-> On -> ( t =/= (/) -> E. u e. t A. v e. t -. v R u ) )
45 44 alrimiv 
 |-  ( F : _V -1-1-onto-> On -> A. t ( t =/= (/) -> E. u e. t A. v e. t -. v R u ) )
46 df-fr 
 |-  ( R Fr _V <-> A. t ( ( t C_ _V /\ t =/= (/) ) -> E. u e. t A. v e. t -. v R u ) )
47 33 biantrur 
 |-  ( t =/= (/) <-> ( t C_ _V /\ t =/= (/) ) )
48 47 imbi1i 
 |-  ( ( t =/= (/) -> E. u e. t A. v e. t -. v R u ) <-> ( ( t C_ _V /\ t =/= (/) ) -> E. u e. t A. v e. t -. v R u ) )
49 48 albii 
 |-  ( A. t ( t =/= (/) -> E. u e. t A. v e. t -. v R u ) <-> A. t ( ( t C_ _V /\ t =/= (/) ) -> E. u e. t A. v e. t -. v R u ) )
50 46 49 bitr4i 
 |-  ( R Fr _V <-> A. t ( t =/= (/) -> E. u e. t A. v e. t -. v R u ) )
51 45 50 sylibr 
 |-  ( F : _V -1-1-onto-> On -> R Fr _V )
52 2 ffvelcdmda 
 |-  ( ( F : _V -1-1-onto-> On /\ w e. _V ) -> ( F ` w ) e. On )
53 52 elvd 
 |-  ( F : _V -1-1-onto-> On -> ( F ` w ) e. On )
54 2 ffvelcdmda 
 |-  ( ( F : _V -1-1-onto-> On /\ z e. _V ) -> ( F ` z ) e. On )
55 54 elvd 
 |-  ( F : _V -1-1-onto-> On -> ( F ` z ) e. On )
56 oneltri 
 |-  ( ( ( F ` w ) e. On /\ ( F ` z ) e. On ) -> ( ( F ` w ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` w ) \/ ( F ` w ) = ( F ` z ) ) )
57 53 55 56 syl2anc 
 |-  ( F : _V -1-1-onto-> On -> ( ( F ` w ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` w ) \/ ( F ` w ) = ( F ` z ) ) )
58 3orcomb 
 |-  ( ( ( F ` w ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` w ) \/ ( F ` w ) = ( F ` z ) ) <-> ( ( F ` w ) e. ( F ` z ) \/ ( F ` w ) = ( F ` z ) \/ ( F ` z ) e. ( F ` w ) ) )
59 57 58 sylib 
 |-  ( F : _V -1-1-onto-> On -> ( ( F ` w ) e. ( F ` z ) \/ ( F ` w ) = ( F ` z ) \/ ( F ` z ) e. ( F ` w ) ) )
60 vex 
 |-  w e. _V
61 vex 
 |-  z e. _V
62 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
63 62 eleq1d 
 |-  ( x = w -> ( ( F ` x ) e. ( F ` y ) <-> ( F ` w ) e. ( F ` y ) ) )
64 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
65 64 eleq2d 
 |-  ( y = z -> ( ( F ` w ) e. ( F ` y ) <-> ( F ` w ) e. ( F ` z ) ) )
66 60 61 63 65 1 brab 
 |-  ( w R z <-> ( F ` w ) e. ( F ` z ) )
67 66 biimpri 
 |-  ( ( F ` w ) e. ( F ` z ) -> w R z )
68 67 a1i 
 |-  ( F : _V -1-1-onto-> On -> ( ( F ` w ) e. ( F ` z ) -> w R z ) )
69 f1of1 
 |-  ( F : _V -1-1-onto-> On -> F : _V -1-1-> On )
70 f1veqaeq 
 |-  ( ( F : _V -1-1-> On /\ ( w e. _V /\ z e. _V ) ) -> ( ( F ` w ) = ( F ` z ) -> w = z ) )
71 60 61 70 mpanr12 
 |-  ( F : _V -1-1-> On -> ( ( F ` w ) = ( F ` z ) -> w = z ) )
72 69 71 syl 
 |-  ( F : _V -1-1-onto-> On -> ( ( F ` w ) = ( F ` z ) -> w = z ) )
73 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
74 73 eleq1d 
 |-  ( x = z -> ( ( F ` x ) e. ( F ` y ) <-> ( F ` z ) e. ( F ` y ) ) )
75 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
76 75 eleq2d 
 |-  ( y = w -> ( ( F ` z ) e. ( F ` y ) <-> ( F ` z ) e. ( F ` w ) ) )
77 61 60 74 76 1 brab 
 |-  ( z R w <-> ( F ` z ) e. ( F ` w ) )
78 77 biimpri 
 |-  ( ( F ` z ) e. ( F ` w ) -> z R w )
79 78 a1i 
 |-  ( F : _V -1-1-onto-> On -> ( ( F ` z ) e. ( F ` w ) -> z R w ) )
80 68 72 79 3orim123d 
 |-  ( F : _V -1-1-onto-> On -> ( ( ( F ` w ) e. ( F ` z ) \/ ( F ` w ) = ( F ` z ) \/ ( F ` z ) e. ( F ` w ) ) -> ( w R z \/ w = z \/ z R w ) ) )
81 59 80 mpd 
 |-  ( F : _V -1-1-onto-> On -> ( w R z \/ w = z \/ z R w ) )
82 81 ralrimivw 
 |-  ( F : _V -1-1-onto-> On -> A. z e. _V ( w R z \/ w = z \/ z R w ) )
83 82 ralrimivw 
 |-  ( F : _V -1-1-onto-> On -> A. w e. _V A. z e. _V ( w R z \/ w = z \/ z R w ) )
84 dfwe2 
 |-  ( R We _V <-> ( R Fr _V /\ A. w e. _V A. z e. _V ( w R z \/ w = z \/ z R w ) ) )
85 51 83 84 sylanbrc 
 |-  ( F : _V -1-1-onto-> On -> R We _V )