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𝐵 ) → 𝐵𝐴 )