MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fodomfi Structured version   Visualization version   GIF version

Theorem fodomfi 8446
Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 9597 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.)
Assertion
Ref Expression
fodomfi ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → 𝐵𝐴)

Proof of Theorem fodomfi
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 foima 6303 . . 3 (𝐹:𝐴onto𝐵 → (𝐹𝐴) = 𝐵)
21adantl 473 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → (𝐹𝐴) = 𝐵)
3 fofn 6300 . . . 4 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
4 imaeq2 5644 . . . . . . . 8 (𝑥 = ∅ → (𝐹𝑥) = (𝐹 “ ∅))
5 ima0 5663 . . . . . . . 8 (𝐹 “ ∅) = ∅
64, 5syl6eq 2815 . . . . . . 7 (𝑥 = ∅ → (𝐹𝑥) = ∅)
7 id 22 . . . . . . 7 (𝑥 = ∅ → 𝑥 = ∅)
86, 7breq12d 4822 . . . . . 6 (𝑥 = ∅ → ((𝐹𝑥) ≼ 𝑥 ↔ ∅ ≼ ∅))
98imbi2d 331 . . . . 5 (𝑥 = ∅ → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → ∅ ≼ ∅)))
10 imaeq2 5644 . . . . . . 7 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
11 id 22 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑦)
1210, 11breq12d 4822 . . . . . 6 (𝑥 = 𝑦 → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹𝑦) ≼ 𝑦))
1312imbi2d 331 . . . . 5 (𝑥 = 𝑦 → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹𝑦) ≼ 𝑦)))
14 imaeq2 5644 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹𝑥) = (𝐹 “ (𝑦 ∪ {𝑧})))
15 id 22 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = (𝑦 ∪ {𝑧}))
1614, 15breq12d 4822 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))
1716imbi2d 331 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
18 imaeq2 5644 . . . . . . 7 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
19 id 22 . . . . . . 7 (𝑥 = 𝐴𝑥 = 𝐴)
2018, 19breq12d 4822 . . . . . 6 (𝑥 = 𝐴 → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹𝐴) ≼ 𝐴))
2120imbi2d 331 . . . . 5 (𝑥 = 𝐴 → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹𝐴) ≼ 𝐴)))
22 0ex 4950 . . . . . . 7 ∅ ∈ V
23220dom 8297 . . . . . 6 ∅ ≼ ∅
2423a1i 11 . . . . 5 (𝐹 Fn 𝐴 → ∅ ≼ ∅)
25 fnfun 6166 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐴 → Fun 𝐹)
2625ad2antrl 719 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → Fun 𝐹)
27 funressn 6618 . . . . . . . . . . . . . 14 (Fun 𝐹 → (𝐹 ↾ {𝑧}) ⊆ {⟨𝑧, (𝐹𝑧)⟩})
28 rnss 5522 . . . . . . . . . . . . . 14 ((𝐹 ↾ {𝑧}) ⊆ {⟨𝑧, (𝐹𝑧)⟩} → ran (𝐹 ↾ {𝑧}) ⊆ ran {⟨𝑧, (𝐹𝑧)⟩})
2926, 27, 283syl 18 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ran (𝐹 ↾ {𝑧}) ⊆ ran {⟨𝑧, (𝐹𝑧)⟩})
30 df-ima 5290 . . . . . . . . . . . . 13 (𝐹 “ {𝑧}) = ran (𝐹 ↾ {𝑧})
31 vex 3353 . . . . . . . . . . . . . . 15 𝑧 ∈ V
3231rnsnop 5801 . . . . . . . . . . . . . 14 ran {⟨𝑧, (𝐹𝑧)⟩} = {(𝐹𝑧)}
3332eqcomi 2774 . . . . . . . . . . . . 13 {(𝐹𝑧)} = ran {⟨𝑧, (𝐹𝑧)⟩}
3429, 30, 333sstr4g 3806 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)})
35 snex 5064 . . . . . . . . . . . 12 {(𝐹𝑧)} ∈ V
36 ssexg 4965 . . . . . . . . . . . 12 (((𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)} ∧ {(𝐹𝑧)} ∈ V) → (𝐹 “ {𝑧}) ∈ V)
3734, 35, 36sylancl 580 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ∈ V)
38 fvi 6444 . . . . . . . . . . 11 ((𝐹 “ {𝑧}) ∈ V → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧}))
3937, 38syl 17 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧}))
4039uneq2d 3929 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = ((𝐹𝑦) ∪ (𝐹 “ {𝑧})))
41 imaundi 5728 . . . . . . . . 9 (𝐹 “ (𝑦 ∪ {𝑧})) = ((𝐹𝑦) ∪ (𝐹 “ {𝑧}))
4240, 41syl6eqr 2817 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = (𝐹 “ (𝑦 ∪ {𝑧})))
43 simprr 789 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹𝑦) ≼ 𝑦)
44 ssdomg 8206 . . . . . . . . . . . 12 ({(𝐹𝑧)} ∈ V → ((𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)} → (𝐹 “ {𝑧}) ≼ {(𝐹𝑧)}))
4535, 34, 44mpsyl 68 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {(𝐹𝑧)})
46 fvex 6388 . . . . . . . . . . . . 13 (𝐹𝑧) ∈ V
4746ensn1 8224 . . . . . . . . . . . 12 {(𝐹𝑧)} ≈ 1𝑜
4831ensn1 8224 . . . . . . . . . . . 12 {𝑧} ≈ 1𝑜
4947, 48entr4i 8217 . . . . . . . . . . 11 {(𝐹𝑧)} ≈ {𝑧}
50 domentr 8219 . . . . . . . . . . 11 (((𝐹 “ {𝑧}) ≼ {(𝐹𝑧)} ∧ {(𝐹𝑧)} ≈ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧})
5145, 49, 50sylancl 580 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {𝑧})
5239, 51eqbrtrd 4831 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧})
53 simplr 785 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ¬ 𝑧𝑦)
54 disjsn 4402 . . . . . . . . . 10 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
5553, 54sylibr 225 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅)
56 undom 8255 . . . . . . . . 9 ((((𝐹𝑦) ≼ 𝑦 ∧ ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧}))
5743, 52, 55, 56syl21anc 866 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧}))
5842, 57eqbrtrrd 4833 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))
5958exp32 411 . . . . . 6 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝐹 Fn 𝐴 → ((𝐹𝑦) ≼ 𝑦 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
6059a2d 29 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐹 Fn 𝐴 → (𝐹𝑦) ≼ 𝑦) → (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
619, 13, 17, 21, 24, 60findcard2s 8408 . . . 4 (𝐴 ∈ Fin → (𝐹 Fn 𝐴 → (𝐹𝐴) ≼ 𝐴))
623, 61syl5 34 . . 3 (𝐴 ∈ Fin → (𝐹:𝐴onto𝐵 → (𝐹𝐴) ≼ 𝐴))
6362imp 395 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → (𝐹𝐴) ≼ 𝐴)
642, 63eqbrtrrd 4833 1 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1652  wcel 2155  Vcvv 3350  cun 3730  cin 3731  wss 3732  c0 4079  {csn 4334  cop 4340   class class class wbr 4809   I cid 5184  ran crn 5278  cres 5279  cima 5280  Fun wfun 6062   Fn wfn 6063  ontowfo 6066  cfv 6068  1𝑜c1o 7757  cen 8157  cdom 8158  Fincfn 8160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-om 7264  df-1o 7764  df-er 7947  df-en 8161  df-dom 8162  df-fin 8164
This theorem is referenced by:  fodomfib  8447  fofinf1o  8448  fidomdm  8450  fofi  8459  pwfilem  8467  cmpsub  21483  alexsubALT  22134  phpreu  33817  poimirlem26  33859
  Copyright terms: Public domain W3C validator