Metamath Proof Explorer

Theorem vonf1oonfo

Description: If F is a bijection from the ordinals to the universe and A is non-empty, then H maps the ordinals onto A . This is the ZFC version of (5 -> 8) in https://tinyurl.com/hamkins-gblac , though it neglects to specify that A must be non-empty. Note that in NBG set theory the antecedent would be something like A. X ( -. X e.V -> E. F F : X -1-1-onto-> On ) , but since we cannot quantify over classes, we instead consider only the case X = V which is sufficient for this proof. This theorem can also be viewed as (2 -> 8). (Contributed by BTernaryTau, 11-Jun-2026)

Ref Expression
Hypotheses vonf1oonfo.1 
|- H = ( x e. On |-> if ( ( F ` x ) e. A , ( F ` x ) , D ) )
vonf1oonfo.2 
|- D = ( F ` |^| { y e. On | ( F ` y ) e. A } )
Assertion vonf1oonfo 
|- ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> H : On -onto-> A )

Proof

Step Hyp Ref Expression
1 vonf1oonfo.1 
 |-  H = ( x e. On |-> if ( ( F ` x ) e. A , ( F ` x ) , D ) )
2 vonf1oonfo.2 
 |-  D = ( F ` |^| { y e. On | ( F ` y ) e. A } )
3 1 rnmpt 
 |-  ran H = { z | E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) }
4 iffalse 
 |-  ( -. ( F ` x ) e. A -> if ( ( F ` x ) e. A , ( F ` x ) , D ) = D )
5 4 3ad2ant3 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) /\ -. ( F ` x ) e. A ) -> if ( ( F ` x ) e. A , ( F ` x ) , D ) = D )
6 n0 
 |-  ( A =/= (/) <-> E. w w e. A )
7 19.42v 
 |-  ( E. w ( F : On -1-1-onto-> _V /\ w e. A ) <-> ( F : On -1-1-onto-> _V /\ E. w w e. A ) )
8 f1ofo 
 |-  ( F : On -1-1-onto-> _V -> F : On -onto-> _V )
9 foelcdmi 
 |-  ( ( F : On -onto-> _V /\ w e. _V ) -> E. y e. On ( F ` y ) = w )
10 9 elvd 
 |-  ( F : On -onto-> _V -> E. y e. On ( F ` y ) = w )
11 8 10 syl 
 |-  ( F : On -1-1-onto-> _V -> E. y e. On ( F ` y ) = w )
12 r19.41v 
 |-  ( E. y e. On ( ( F ` y ) = w /\ w e. A ) <-> ( E. y e. On ( F ` y ) = w /\ w e. A ) )
13 eleq1 
 |-  ( ( F ` y ) = w -> ( ( F ` y ) e. A <-> w e. A ) )
14 13 biimpar 
 |-  ( ( ( F ` y ) = w /\ w e. A ) -> ( F ` y ) e. A )
15 14 reximi 
 |-  ( E. y e. On ( ( F ` y ) = w /\ w e. A ) -> E. y e. On ( F ` y ) e. A )
16 12 15 sylbir 
 |-  ( ( E. y e. On ( F ` y ) = w /\ w e. A ) -> E. y e. On ( F ` y ) e. A )
17 11 16 sylan 
 |-  ( ( F : On -1-1-onto-> _V /\ w e. A ) -> E. y e. On ( F ` y ) e. A )
18 17 exlimiv 
 |-  ( E. w ( F : On -1-1-onto-> _V /\ w e. A ) -> E. y e. On ( F ` y ) e. A )
19 7 18 sylbir 
 |-  ( ( F : On -1-1-onto-> _V /\ E. w w e. A ) -> E. y e. On ( F ` y ) e. A )
20 6 19 sylan2b 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> E. y e. On ( F ` y ) e. A )
21 nfcv 
 |-  F/_ y F
22 nfrab1 
 |-  F/_ y { y e. On | ( F ` y ) e. A }
23 22 nfint 
 |-  F/_ y |^| { y e. On | ( F ` y ) e. A }
24 21 23 nffv 
 |-  F/_ y ( F ` |^| { y e. On | ( F ` y ) e. A } )
25 24 nfel1 
 |-  F/ y ( F ` |^| { y e. On | ( F ` y ) e. A } ) e. A
26 fveq2 
 |-  ( y = |^| { y e. On | ( F ` y ) e. A } -> ( F ` y ) = ( F ` |^| { y e. On | ( F ` y ) e. A } ) )
27 26 eleq1d 
 |-  ( y = |^| { y e. On | ( F ` y ) e. A } -> ( ( F ` y ) e. A <-> ( F ` |^| { y e. On | ( F ` y ) e. A } ) e. A ) )
28 25 27 onminsb 
 |-  ( E. y e. On ( F ` y ) e. A -> ( F ` |^| { y e. On | ( F ` y ) e. A } ) e. A )
29 2 28 eqeltrid 
 |-  ( E. y e. On ( F ` y ) e. A -> D e. A )
30 20 29 syl 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> D e. A )
31 30 3adant3 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) /\ -. ( F ` x ) e. A ) -> D e. A )
32 5 31 eqeltrd 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) /\ -. ( F ` x ) e. A ) -> if ( ( F ` x ) e. A , ( F ` x ) , D ) e. A )
33 32 3expia 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> ( -. ( F ` x ) e. A -> if ( ( F ` x ) e. A , ( F ` x ) , D ) e. A ) )
34 iftrue 
 |-  ( ( F ` x ) e. A -> if ( ( F ` x ) e. A , ( F ` x ) , D ) = ( F ` x ) )
35 id 
 |-  ( ( F ` x ) e. A -> ( F ` x ) e. A )
36 34 35 eqeltrd 
 |-  ( ( F ` x ) e. A -> if ( ( F ` x ) e. A , ( F ` x ) , D ) e. A )
37 33 36 pm2.61d2 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> if ( ( F ` x ) e. A , ( F ` x ) , D ) e. A )
38 eleq1 
 |-  ( z = if ( ( F ` x ) e. A , ( F ` x ) , D ) -> ( z e. A <-> if ( ( F ` x ) e. A , ( F ` x ) , D ) e. A ) )
39 37 38 syl5ibrcom 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> ( z = if ( ( F ` x ) e. A , ( F ` x ) , D ) -> z e. A ) )
40 39 rexlimdvw 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> ( E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) -> z e. A ) )
41 40 abssdv 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> { z | E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) } C_ A )
42 3 41 eqsstrid 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> ran H C_ A )
43 fveqeq2 
 |-  ( x = ( `' F ` z ) -> ( ( F ` x ) = z <-> ( F ` ( `' F ` z ) ) = z ) )
44 f1ocnvdm 
 |-  ( ( F : On -1-1-onto-> _V /\ z e. _V ) -> ( `' F ` z ) e. On )
45 44 elvd 
 |-  ( F : On -1-1-onto-> _V -> ( `' F ` z ) e. On )
46 f1ocnvfv2 
 |-  ( ( F : On -1-1-onto-> _V /\ z e. _V ) -> ( F ` ( `' F ` z ) ) = z )
47 46 elvd 
 |-  ( F : On -1-1-onto-> _V -> ( F ` ( `' F ` z ) ) = z )
48 43 45 47 rspcedvdw 
 |-  ( F : On -1-1-onto-> _V -> E. x e. On ( F ` x ) = z )
49 eleq1 
 |-  ( ( F ` x ) = z -> ( ( F ` x ) e. A <-> z e. A ) )
50 49 biimpar 
 |-  ( ( ( F ` x ) = z /\ z e. A ) -> ( F ` x ) e. A )
51 50 iftrued 
 |-  ( ( ( F ` x ) = z /\ z e. A ) -> if ( ( F ` x ) e. A , ( F ` x ) , D ) = ( F ` x ) )
52 simpl 
 |-  ( ( ( F ` x ) = z /\ z e. A ) -> ( F ` x ) = z )
53 51 52 eqtr2d 
 |-  ( ( ( F ` x ) = z /\ z e. A ) -> z = if ( ( F ` x ) e. A , ( F ` x ) , D ) )
54 53 expcom 
 |-  ( z e. A -> ( ( F ` x ) = z -> z = if ( ( F ` x ) e. A , ( F ` x ) , D ) ) )
55 54 reximdv 
 |-  ( z e. A -> ( E. x e. On ( F ` x ) = z -> E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) ) )
56 48 55 syl5com 
 |-  ( F : On -1-1-onto-> _V -> ( z e. A -> E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) ) )
57 56 ralrimiv 
 |-  ( F : On -1-1-onto-> _V -> A. z e. A E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) )
58 ssabral 
 |-  ( A C_ { z | E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) } <-> A. z e. A E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) )
59 57 58 sylibr 
 |-  ( F : On -1-1-onto-> _V -> A C_ { z | E. x e. On z = if ( ( F ` x ) e. A , ( F ` x ) , D ) } )
60 59 3 sseqtrrdi 
 |-  ( F : On -1-1-onto-> _V -> A C_ ran H )
61 60 adantr 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> A C_ ran H )
62 42 61 eqssd 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> ran H = A )
63 fvex 
 |-  ( F ` x ) e. _V
64 2 fvexi 
 |-  D e. _V
65 63 64 ifex 
 |-  if ( ( F ` x ) e. A , ( F ` x ) , D ) e. _V
66 65 1 fnmpti 
 |-  H Fn On
67 df-fo 
 |-  ( H : On -onto-> A <-> ( H Fn On /\ ran H = A ) )
68 66 67 mpbiran 
 |-  ( H : On -onto-> A <-> ran H = A )
69 62 68 sylibr 
 |-  ( ( F : On -1-1-onto-> _V /\ A =/= (/) ) -> H : On -onto-> A )