Metamath Proof Explorer

Theorem fodomfi

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodomg for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006) (Proof shortened by Mario Carneiro, 16-Nov-2014) Avoid ax-pow . (Revised by BTernaryTau, 20-Jun-2025)

Ref Expression
Assertion fodomfi ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 foima ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 “ 𝐴 ) = 𝐵 )
2 1 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 “ 𝐴 ) = 𝐵 )
3 imaeq2 ⊢ ( 𝑥 = ∅ → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ∅ ) )
4 ima0 ⊢ ( 𝐹 “ ∅ ) = ∅
5 3 4 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝐹 “ 𝑥 ) = ∅ )
6 id ⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
7 5 6 breq12d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 “ 𝑥 ) ≼ 𝑥 ↔ ∅ ≼ ∅ ) )
8 7 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝑥 ) ≼ 𝑥 ) ↔ ( 𝐹 Fn 𝐴 → ∅ ≼ ∅ ) ) )
9 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑦 ) )
10 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
11 9 10 breq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 “ 𝑥 ) ≼ 𝑥 ↔ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝑥 ) ≼ 𝑥 ) ↔ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) )
13 imaeq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) )
14 id ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → 𝑥 = ( 𝑦 ∪ { 𝑧 } ) )
15 13 14 breq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐹 “ 𝑥 ) ≼ 𝑥 ↔ ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) ) )
16 15 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝑥 ) ≼ 𝑥 ) ↔ ( 𝐹 Fn 𝐴 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) ) ) )
17 imaeq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝐴 ) )
18 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
19 17 18 breq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 “ 𝑥 ) ≼ 𝑥 ↔ ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝑥 ) ≼ 𝑥 ) ↔ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) ) )
21 0ex ⊢ ∅ ∈ V
22 21 0dom ⊢ ∅ ≼ ∅
23 22 a1i ⊢ ( 𝐹 Fn 𝐴 → ∅ ≼ ∅ )
24 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
25 24 ad2antrl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → Fun 𝐹 )
26 funressn ⊢ ( Fun 𝐹 → ( 𝐹 ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
27 rnss ⊢ ( ( 𝐹 ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } → ran ( 𝐹 ↾ { 𝑧 } ) ⊆ ran { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
28 25 26 27 3syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ran ( 𝐹 ↾ { 𝑧 } ) ⊆ ran { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
29 df-ima ⊢ ( 𝐹 “ { 𝑧 } ) = ran ( 𝐹 ↾ { 𝑧 } )
30 vex ⊢ 𝑧 ∈ V
31 30 rnsnop ⊢ ran { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } = { ( 𝐹 ‘ 𝑧 ) }
32 31 eqcomi ⊢ { ( 𝐹 ‘ 𝑧 ) } = ran { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ }
33 28 29 32 3sstr4g ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ { 𝑧 } ) ⊆ { ( 𝐹 ‘ 𝑧 ) } )
34 snfi ⊢ { ( 𝐹 ‘ 𝑧 ) } ∈ Fin
35 ssexg ⊢ ( ( ( 𝐹 “ { 𝑧 } ) ⊆ { ( 𝐹 ‘ 𝑧 ) } ∧ { ( 𝐹 ‘ 𝑧 ) } ∈ Fin ) → ( 𝐹 “ { 𝑧 } ) ∈ V )
36 33 34 35 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ { 𝑧 } ) ∈ V )
37 fvi ⊢ ( ( 𝐹 “ { 𝑧 } ) ∈ V → ( I ‘ ( 𝐹 “ { 𝑧 } ) ) = ( 𝐹 “ { 𝑧 } ) )
38 36 37 syl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( I ‘ ( 𝐹 “ { 𝑧 } ) ) = ( 𝐹 “ { 𝑧 } ) )
39 38 uneq2d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( ( 𝐹 “ 𝑦 ) ∪ ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ) = ( ( 𝐹 “ 𝑦 ) ∪ ( 𝐹 “ { 𝑧 } ) ) )
40 imaundi ⊢ ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝐹 “ 𝑦 ) ∪ ( 𝐹 “ { 𝑧 } ) )
41 39 40 eqtr4di ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( ( 𝐹 “ 𝑦 ) ∪ ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ) = ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) )
42 simprr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ 𝑦 ) ≼ 𝑦 )
43 ssdomfi ⊢ ( { ( 𝐹 ‘ 𝑧 ) } ∈ Fin → ( ( 𝐹 “ { 𝑧 } ) ⊆ { ( 𝐹 ‘ 𝑧 ) } → ( 𝐹 “ { 𝑧 } ) ≼ { ( 𝐹 ‘ 𝑧 ) } ) )
44 34 33 43 mpsyl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ { 𝑧 } ) ≼ { ( 𝐹 ‘ 𝑧 ) } )
45 fvex ⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
46 en2sn ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ V ∧ 𝑧 ∈ V ) → { ( 𝐹 ‘ 𝑧 ) } ≈ { 𝑧 } )
47 45 30 46 mp2an ⊢ { ( 𝐹 ‘ 𝑧 ) } ≈ { 𝑧 }
48 endom ⊢ ( { ( 𝐹 ‘ 𝑧 ) } ≈ { 𝑧 } → { ( 𝐹 ‘ 𝑧 ) } ≼ { 𝑧 } )
49 domtrfi ⊢ ( ( { ( 𝐹 ‘ 𝑧 ) } ∈ Fin ∧ ( 𝐹 “ { 𝑧 } ) ≼ { ( 𝐹 ‘ 𝑧 ) } ∧ { ( 𝐹 ‘ 𝑧 ) } ≼ { 𝑧 } ) → ( 𝐹 “ { 𝑧 } ) ≼ { 𝑧 } )
50 34 49 mp3an1 ⊢ ( ( ( 𝐹 “ { 𝑧 } ) ≼ { ( 𝐹 ‘ 𝑧 ) } ∧ { ( 𝐹 ‘ 𝑧 ) } ≼ { 𝑧 } ) → ( 𝐹 “ { 𝑧 } ) ≼ { 𝑧 } )
51 48 50 sylan2 ⊢ ( ( ( 𝐹 “ { 𝑧 } ) ≼ { ( 𝐹 ‘ 𝑧 ) } ∧ { ( 𝐹 ‘ 𝑧 ) } ≈ { 𝑧 } ) → ( 𝐹 “ { 𝑧 } ) ≼ { 𝑧 } )
52 44 47 51 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ { 𝑧 } ) ≼ { 𝑧 } )
53 38 52 eqbrtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ≼ { 𝑧 } )
54 simplr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ¬ 𝑧 ∈ 𝑦 )
55 disjsn ⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
56 54 55 sylibr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
57 undom ⊢ ( ( ( ( 𝐹 “ 𝑦 ) ≼ 𝑦 ∧ ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ≼ { 𝑧 } ) ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) → ( ( 𝐹 “ 𝑦 ) ∪ ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) )
58 42 53 56 57 syl21anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( ( 𝐹 “ 𝑦 ) ∪ ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) )
59 41 58 eqbrtrrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) )
60 59 exp32 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝐹 Fn 𝐴 → ( ( 𝐹 “ 𝑦 ) ≼ 𝑦 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) ) ) )
61 60 a2d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) → ( 𝐹 Fn 𝐴 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) ) ) )
62 8 12 16 20 23 61 findcard2s ⊢ ( 𝐴 ∈ Fin → ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) )
63 fofn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
64 62 63 impel ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )
65 2 64 eqbrtrrd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 )