Metamath Proof Explorer

Theorem fodomfi

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006) (Proof shortened by Mario Carneiro, 16-Nov-2014)

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 snex ⊢ { ( 𝐹 ‘ 𝑧 ) } ∈ V
35 ssexg ⊢ ( ( ( 𝐹 “ { 𝑧 } ) ⊆ { ( 𝐹 ‘ 𝑧 ) } ∧ { ( 𝐹 ‘ 𝑧 ) } ∈ V ) → ( 𝐹 “ { 𝑧 } ) ∈ 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 ssdomg ⊢ ( { ( 𝐹 ‘ 𝑧 ) } ∈ V → ( ( 𝐹 “ { 𝑧 } ) ⊆ { ( 𝐹 ‘ 𝑧 ) } → ( 𝐹 “ { 𝑧 } ) ≼ { ( 𝐹 ‘ 𝑧 ) } ) )
44 34 33 43 mpsyl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ { 𝑧 } ) ≼ { ( 𝐹 ‘ 𝑧 ) } )
45 fvex ⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
46 45 ensn1 ⊢ { ( 𝐹 ‘ 𝑧 ) } ≈ 1o
47 30 ensn1 ⊢ { 𝑧 } ≈ 1o
48 46 47 entr4i ⊢ { ( 𝐹 ‘ 𝑧 ) } ≈ { 𝑧 }
49 domentr ⊢ ( ( ( 𝐹 “ { 𝑧 } ) ≼ { ( 𝐹 ‘ 𝑧 ) } ∧ { ( 𝐹 ‘ 𝑧 ) } ≈ { 𝑧 } ) → ( 𝐹 “ { 𝑧 } ) ≼ { 𝑧 } )
50 44 48 49 sylancl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ { 𝑧 } ) ≼ { 𝑧 } )
51 38 50 eqbrtrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ≼ { 𝑧 } )
52 simplr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ¬ 𝑧 ∈ 𝑦 )
53 disjsn ⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
54 52 53 sylibr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
55 undom ⊢ ( ( ( ( 𝐹 “ 𝑦 ) ≼ 𝑦 ∧ ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ≼ { 𝑧 } ) ∧ ( 𝑦 ∩ { 𝑧 } ) = ∅ ) → ( ( 𝐹 “ 𝑦 ) ∪ ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) )
56 42 51 54 55 syl21anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( ( 𝐹 “ 𝑦 ) ∪ ( I ‘ ( 𝐹 “ { 𝑧 } ) ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) )
57 41 56 eqbrtrrd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) ) → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) )
58 57 exp32 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝐹 Fn 𝐴 → ( ( 𝐹 “ 𝑦 ) ≼ 𝑦 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) ) ) )
59 58 a2d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝑦 ) ≼ 𝑦 ) → ( 𝐹 Fn 𝐴 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ≼ ( 𝑦 ∪ { 𝑧 } ) ) ) )
60 8 12 16 20 23 59 findcard2s ⊢ ( 𝐴 ∈ Fin → ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) )
61 fofn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
62 60 61 impel ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )
63 2 62 eqbrtrrd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 )