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 ⊢ 𝐻 = ( 𝑥 ∈ On ↦ if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) )
vonf1oonfo.2 ⊢ 𝐷 = ( 𝐹 ‘ ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } )
Assertion vonf1oonfo ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → 𝐻 : On –onto→ 𝐴 )

Proof

Step Hyp Ref Expression
1 vonf1oonfo.1 ⊢ 𝐻 = ( 𝑥 ∈ On ↦ if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) )
2 vonf1oonfo.2 ⊢ 𝐷 = ( 𝐹 ‘ ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } )
3 1 rnmpt ⊢ ran 𝐻 = { 𝑧 ∣ ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) }
4 iffalse ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 → if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) = 𝐷 )
5 4 3ad2ant3 ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) = 𝐷 )
6 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐴 )
7 19.42v ⊢ ( ∃ 𝑤 ( 𝐹 : On –1-1-onto→ V ∧ 𝑤 ∈ 𝐴 ) ↔ ( 𝐹 : On –1-1-onto→ V ∧ ∃ 𝑤 𝑤 ∈ 𝐴 ) )
8 f1ofo ⊢ ( 𝐹 : On –1-1-onto→ V → 𝐹 : On –onto→ V )
9 foelcdmi ⊢ ( ( 𝐹 : On –onto→ V ∧ 𝑤 ∈ V ) → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) = 𝑤 )
10 9 elvd ⊢ ( 𝐹 : On –onto→ V → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) = 𝑤 )
11 8 10 syl ⊢ ( 𝐹 : On –1-1-onto→ V → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) = 𝑤 )
12 r19.41v ⊢ ( ∃ 𝑦 ∈ On ( ( 𝐹 ‘ 𝑦 ) = 𝑤 ∧ 𝑤 ∈ 𝐴 ) ↔ ( ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) = 𝑤 ∧ 𝑤 ∈ 𝐴 ) )
13 eleq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
14 13 biimpar ⊢ ( ( ( 𝐹 ‘ 𝑦 ) = 𝑤 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
15 14 reximi ⊢ ( ∃ 𝑦 ∈ On ( ( 𝐹 ‘ 𝑦 ) = 𝑤 ∧ 𝑤 ∈ 𝐴 ) → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
16 12 15 sylbir ⊢ ( ( ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) = 𝑤 ∧ 𝑤 ∈ 𝐴 ) → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
17 11 16 sylan ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝑤 ∈ 𝐴 ) → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
18 17 exlimiv ⊢ ( ∃ 𝑤 ( 𝐹 : On –1-1-onto→ V ∧ 𝑤 ∈ 𝐴 ) → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
19 7 18 sylbir ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ ∃ 𝑤 𝑤 ∈ 𝐴 ) → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
20 6 19 sylan2b ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
21 nfcv ⊢ Ⅎ 𝑦 𝐹
22 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 }
23 22 nfint ⊢ Ⅎ 𝑦 ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 }
24 21 23 nffv ⊢ Ⅎ 𝑦 ( 𝐹 ‘ ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } )
25 24 nfel1 ⊢ Ⅎ 𝑦 ( 𝐹 ‘ ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } ) ∈ 𝐴
26 fveq2 ⊢ ( 𝑦 = ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } ) )
27 26 eleq1d ⊢ ( 𝑦 = ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 ↔ ( 𝐹 ‘ ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } ) ∈ 𝐴 ) )
28 25 27 onminsb ⊢ ( ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 → ( 𝐹 ‘ ∩ { 𝑦 ∈ On ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 } ) ∈ 𝐴 )
29 2 28 eqeltrid ⊢ ( ∃ 𝑦 ∈ On ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 → 𝐷 ∈ 𝐴 )
30 20 29 syl ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → 𝐷 ∈ 𝐴 )
31 30 3adant3 ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → 𝐷 ∈ 𝐴 )
32 5 31 eqeltrd ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ∈ 𝐴 )
33 32 3expia ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 → if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ∈ 𝐴 ) )
34 iftrue ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 → if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) = ( 𝐹 ‘ 𝑥 ) )
35 id ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
36 34 35 eqeltrd ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 → if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ∈ 𝐴 )
37 33 36 pm2.61d2 ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ∈ 𝐴 )
38 eleq1 ⊢ ( 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) → ( 𝑧 ∈ 𝐴 ↔ if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ∈ 𝐴 ) )
39 37 38 syl5ibrcom ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → ( 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) → 𝑧 ∈ 𝐴 ) )
40 39 rexlimdvw ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) → 𝑧 ∈ 𝐴 ) )
41 40 abssdv ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → { 𝑧 ∣ ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) } ⊆ 𝐴 )
42 3 41 eqsstrid ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → ran 𝐻 ⊆ 𝐴 )
43 fveqeq2 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑧 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 ) )
44 f1ocnvdm ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝑧 ∈ V ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ On )
45 44 elvd ⊢ ( 𝐹 : On –1-1-onto→ V → ( ◡ 𝐹 ‘ 𝑧 ) ∈ On )
46 f1ocnvfv2 ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝑧 ∈ V ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
47 46 elvd ⊢ ( 𝐹 : On –1-1-onto→ V → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
48 43 45 47 rspcedvdw ⊢ ( 𝐹 : On –1-1-onto→ V → ∃ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) = 𝑧 )
49 eleq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
50 49 biimpar ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑧 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
51 50 iftrued ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑧 ∧ 𝑧 ∈ 𝐴 ) → if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) = ( 𝐹 ‘ 𝑥 ) )
52 simpl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑧 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝑧 )
53 51 52 eqtr2d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑧 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) )
54 53 expcom ⊢ ( 𝑧 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = 𝑧 → 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ) )
55 54 reximdv ⊢ ( 𝑧 ∈ 𝐴 → ( ∃ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) = 𝑧 → ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ) )
56 48 55 syl5com ⊢ ( 𝐹 : On –1-1-onto→ V → ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ) )
57 56 ralrimiv ⊢ ( 𝐹 : On –1-1-onto→ V → ∀ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) )
58 ssabral ⊢ ( 𝐴 ⊆ { 𝑧 ∣ ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) } ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) )
59 57 58 sylibr ⊢ ( 𝐹 : On –1-1-onto→ V → 𝐴 ⊆ { 𝑧 ∣ ∃ 𝑥 ∈ On 𝑧 = if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) } )
60 59 3 sseqtrrdi ⊢ ( 𝐹 : On –1-1-onto→ V → 𝐴 ⊆ ran 𝐻 )
61 60 adantr ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ ran 𝐻 )
62 42 61 eqssd ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → ran 𝐻 = 𝐴 )
63 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
64 2 fvexi ⊢ 𝐷 ∈ V
65 63 64 ifex ⊢ if ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 𝐷 ) ∈ V
66 65 1 fnmpti ⊢ 𝐻 Fn On
67 df-fo ⊢ ( 𝐻 : On –onto→ 𝐴 ↔ ( 𝐻 Fn On ∧ ran 𝐻 = 𝐴 ) )
68 66 67 mpbiran ⊢ ( 𝐻 : On –onto→ 𝐴 ↔ ran 𝐻 = 𝐴 )
69 62 68 sylibr ⊢ ( ( 𝐹 : On –1-1-onto→ V ∧ 𝐴 ≠ ∅ ) → 𝐻 : On –onto→ 𝐴 )