Metamath Proof Explorer

Theorem onvf1od

Description: If G is a global choice function, then F is a bijection from the ordinals to the universe. This is the ZFC version of (1 -> 2) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 5-Dec-2025)

Ref Expression
Hypotheses onvf1od.1 
|- ( ph -> A. z ( z =/= (/) -> ( G ` z ) e. z ) )
onvf1od.2 
|- M = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. ran w }
onvf1od.3 
|- N = ( G ` ( ( R1 ` M ) \ ran w ) )
onvf1od.4 
|- F = recs ( ( w e. _V |-> N ) )
Assertion onvf1od 
|- ( ph -> F : On -1-1-onto-> _V )

Proof

Step Hyp Ref Expression
1 onvf1od.1 
 |-  ( ph -> A. z ( z =/= (/) -> ( G ` z ) e. z ) )
2 onvf1od.2 
 |-  M = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. ran w }
3 onvf1od.3 
 |-  N = ( G ` ( ( R1 ` M ) \ ran w ) )
4 onvf1od.4 
 |-  F = recs ( ( w e. _V |-> N ) )
5 4 tfr1 
 |-  F Fn On
6 dffn2 
 |-  ( F Fn On <-> F : On --> _V )
7 5 6 mpbi 
 |-  F : On --> _V
8 eqid 
 |-  |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } = |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) }
9 eqid 
 |-  ( G ` ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) ) = ( G ` ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) )
10 2 3 4 8 9 onvf1odlem3 
 |-  ( t e. On -> ( F ` t ) = ( G ` ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) ) )
11 10 adantl 
 |-  ( ( ph /\ t e. On ) -> ( F ` t ) = ( G ` ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) ) )
12 fnfun 
 |-  ( F Fn On -> Fun F )
13 vex 
 |-  t e. _V
14 13 funimaex 
 |-  ( Fun F -> ( F " t ) e. _V )
15 5 12 14 mp2b 
 |-  ( F " t ) e. _V
16 1 8 9 onvf1odlem2 
 |-  ( ph -> ( ( F " t ) e. _V -> ( G ` ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) ) e. ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) ) )
17 15 16 mpi 
 |-  ( ph -> ( G ` ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) ) e. ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) )
18 17 eldifbd 
 |-  ( ph -> -. ( G ` ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) ) e. ( F " t ) )
19 18 adantr 
 |-  ( ( ph /\ t e. On ) -> -. ( G ` ( ( R1 ` |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " t ) } ) \ ( F " t ) ) ) e. ( F " t ) )
20 11 19 eqneltrd 
 |-  ( ( ph /\ t e. On ) -> -. ( F ` t ) e. ( F " t ) )
21 20 ralrimiva 
 |-  ( ph -> A. t e. On -. ( F ` t ) e. ( F " t ) )
22 fvex 
 |-  ( F ` t ) e. _V
23 eldif 
 |-  ( ( F ` t ) e. ( _V \ ( F " t ) ) <-> ( ( F ` t ) e. _V /\ -. ( F ` t ) e. ( F " t ) ) )
24 22 23 mpbiran 
 |-  ( ( F ` t ) e. ( _V \ ( F " t ) ) <-> -. ( F ` t ) e. ( F " t ) )
25 24 ralbii 
 |-  ( A. t e. On ( F ` t ) e. ( _V \ ( F " t ) ) <-> A. t e. On -. ( F ` t ) e. ( F " t ) )
26 5 tz7.48-2 
 |-  ( A. t e. On ( F ` t ) e. ( _V \ ( F " t ) ) -> Fun `' F )
27 25 26 sylbir 
 |-  ( A. t e. On -. ( F ` t ) e. ( F " t ) -> Fun `' F )
28 21 27 syl 
 |-  ( ph -> Fun `' F )
29 df-f1 
 |-  ( F : On -1-1-> _V <-> ( F : On --> _V /\ Fun `' F ) )
30 29 biimpri 
 |-  ( ( F : On --> _V /\ Fun `' F ) -> F : On -1-1-> _V )
31 7 28 30 sylancr 
 |-  ( ph -> F : On -1-1-> _V )
32 onprc 
 |-  -. On e. _V
33 f1f1orn 
 |-  ( F : On -1-1-> _V -> F : On -1-1-onto-> ran F )
34 f1of1 
 |-  ( F : On -1-1-onto-> ran F -> F : On -1-1-> ran F )
35 31 33 34 3syl 
 |-  ( ph -> F : On -1-1-> ran F )
36 f1dmex 
 |-  ( ( F : On -1-1-> ran F /\ ran F e. _V ) -> On e. _V )
37 35 36 sylan 
 |-  ( ( ph /\ ran F e. _V ) -> On e. _V )
38 37 stoic1a 
 |-  ( ( ph /\ -. On e. _V ) -> -. ran F e. _V )
39 32 38 mpan2 
 |-  ( ph -> -. ran F e. _V )
40 1 2 3 4 8 9 onvf1odlem4 
 |-  ( ph -> ( -. ran F e. _V -> ran F = _V ) )
41 39 40 mpd 
 |-  ( ph -> ran F = _V )
42 dff1o5 
 |-  ( F : On -1-1-onto-> _V <-> ( F : On -1-1-> _V /\ ran F = _V ) )
43 31 41 42 sylanbrc 
 |-  ( ph -> F : On -1-1-onto-> _V )