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

Theorem fodomfi 8407
Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 9557 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 6283 . . 3 (𝐹:𝐴onto𝐵 → (𝐹𝐴) = 𝐵)
21adantl 473 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → (𝐹𝐴) = 𝐵)
3 fofn 6280 . . . 4 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
4 imaeq2 5621 . . . . . . . 8 (𝑥 = ∅ → (𝐹𝑥) = (𝐹 “ ∅))
5 ima0 5640 . . . . . . . 8 (𝐹 “ ∅) = ∅
64, 5syl6eq 2811 . . . . . . 7 (𝑥 = ∅ → (𝐹𝑥) = ∅)
7 id 22 . . . . . . 7 (𝑥 = ∅ → 𝑥 = ∅)
86, 7breq12d 4818 . . . . . 6 (𝑥 = ∅ → ((𝐹𝑥) ≼ 𝑥 ↔ ∅ ≼ ∅))
98imbi2d 329 . . . . 5 (𝑥 = ∅ → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → ∅ ≼ ∅)))
10 imaeq2 5621 . . . . . . 7 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
11 id 22 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑦)
1210, 11breq12d 4818 . . . . . 6 (𝑥 = 𝑦 → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹𝑦) ≼ 𝑦))
1312imbi2d 329 . . . . 5 (𝑥 = 𝑦 → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹𝑦) ≼ 𝑦)))
14 imaeq2 5621 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹𝑥) = (𝐹 “ (𝑦 ∪ {𝑧})))
15 id 22 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = (𝑦 ∪ {𝑧}))
1614, 15breq12d 4818 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))
1716imbi2d 329 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
18 imaeq2 5621 . . . . . . 7 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
19 id 22 . . . . . . 7 (𝑥 = 𝐴𝑥 = 𝐴)
2018, 19breq12d 4818 . . . . . 6 (𝑥 = 𝐴 → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹𝐴) ≼ 𝐴))
2120imbi2d 329 . . . . 5 (𝑥 = 𝐴 → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹𝐴) ≼ 𝐴)))
22 0ex 4943 . . . . . . 7 ∅ ∈ V
23220dom 8258 . . . . . 6 ∅ ≼ ∅
2423a1i 11 . . . . 5 (𝐹 Fn 𝐴 → ∅ ≼ ∅)
25 fnfun 6150 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐴 → Fun 𝐹)
2625ad2antrl 766 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → Fun 𝐹)
27 funressn 6591 . . . . . . . . . . . . . 14 (Fun 𝐹 → (𝐹 ↾ {𝑧}) ⊆ {⟨𝑧, (𝐹𝑧)⟩})
28 rnss 5510 . . . . . . . . . . . . . 14 ((𝐹 ↾ {𝑧}) ⊆ {⟨𝑧, (𝐹𝑧)⟩} → ran (𝐹 ↾ {𝑧}) ⊆ ran {⟨𝑧, (𝐹𝑧)⟩})
2926, 27, 283syl 18 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ran (𝐹 ↾ {𝑧}) ⊆ ran {⟨𝑧, (𝐹𝑧)⟩})
30 df-ima 5280 . . . . . . . . . . . . 13 (𝐹 “ {𝑧}) = ran (𝐹 ↾ {𝑧})
31 vex 3344 . . . . . . . . . . . . . . 15 𝑧 ∈ V
3231rnsnop 5777 . . . . . . . . . . . . . 14 ran {⟨𝑧, (𝐹𝑧)⟩} = {(𝐹𝑧)}
3332eqcomi 2770 . . . . . . . . . . . . 13 {(𝐹𝑧)} = ran {⟨𝑧, (𝐹𝑧)⟩}
3429, 30, 333sstr4g 3788 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)})
35 snex 5058 . . . . . . . . . . . 12 {(𝐹𝑧)} ∈ V
36 ssexg 4957 . . . . . . . . . . . 12 (((𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)} ∧ {(𝐹𝑧)} ∈ V) → (𝐹 “ {𝑧}) ∈ V)
3734, 35, 36sylancl 697 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ∈ V)
38 fvi 6419 . . . . . . . . . . 11 ((𝐹 “ {𝑧}) ∈ V → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧}))
3937, 38syl 17 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧}))
4039uneq2d 3911 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = ((𝐹𝑦) ∪ (𝐹 “ {𝑧})))
41 imaundi 5704 . . . . . . . . 9 (𝐹 “ (𝑦 ∪ {𝑧})) = ((𝐹𝑦) ∪ (𝐹 “ {𝑧}))
4240, 41syl6eqr 2813 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = (𝐹 “ (𝑦 ∪ {𝑧})))
43 simprr 813 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹𝑦) ≼ 𝑦)
44 ssdomg 8170 . . . . . . . . . . . 12 ({(𝐹𝑧)} ∈ V → ((𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)} → (𝐹 “ {𝑧}) ≼ {(𝐹𝑧)}))
4535, 34, 44mpsyl 68 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {(𝐹𝑧)})
46 fvex 6364 . . . . . . . . . . . . 13 (𝐹𝑧) ∈ V
4746ensn1 8188 . . . . . . . . . . . 12 {(𝐹𝑧)} ≈ 1𝑜
4831ensn1 8188 . . . . . . . . . . . 12 {𝑧} ≈ 1𝑜
4947, 48entr4i 8181 . . . . . . . . . . 11 {(𝐹𝑧)} ≈ {𝑧}
50 domentr 8183 . . . . . . . . . . 11 (((𝐹 “ {𝑧}) ≼ {(𝐹𝑧)} ∧ {(𝐹𝑧)} ≈ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧})
5145, 49, 50sylancl 697 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {𝑧})
5239, 51eqbrtrd 4827 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧})
53 simplr 809 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ¬ 𝑧𝑦)
54 disjsn 4391 . . . . . . . . . 10 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
5553, 54sylibr 224 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅)
56 undom 8216 . . . . . . . . 9 ((((𝐹𝑦) ≼ 𝑦 ∧ ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧}))
5743, 52, 55, 56syl21anc 1476 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧}))
5842, 57eqbrtrrd 4829 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))
5958exp32 632 . . . . . 6 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝐹 Fn 𝐴 → ((𝐹𝑦) ≼ 𝑦 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
6059a2d 29 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐹 Fn 𝐴 → (𝐹𝑦) ≼ 𝑦) → (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
619, 13, 17, 21, 24, 60findcard2s 8369 . . . 4 (𝐴 ∈ Fin → (𝐹 Fn 𝐴 → (𝐹𝐴) ≼ 𝐴))
623, 61syl5 34 . . 3 (𝐴 ∈ Fin → (𝐹:𝐴onto𝐵 → (𝐹𝐴) ≼ 𝐴))
6362imp 444 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → (𝐹𝐴) ≼ 𝐴)
642, 63eqbrtrrd 4829 1 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1632  wcel 2140  Vcvv 3341  cun 3714  cin 3715  wss 3716  c0 4059  {csn 4322  cop 4328   class class class wbr 4805   I cid 5174  ran crn 5268  cres 5269  cima 5270  Fun wfun 6044   Fn wfn 6045  ontowfo 6048  cfv 6050  1𝑜c1o 7724  cen 8121  cdom 8122  Fincfn 8124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-om 7233  df-1o 7731  df-er 7914  df-en 8125  df-dom 8126  df-fin 8128
This theorem is referenced by:  fodomfib  8408  fofinf1o  8409  fidomdm  8411  fofi  8420  pwfilem  8428  cmpsub  21426  alexsubALT  22077  phpreu  33725  poimirlem26  33767
  Copyright terms: Public domain W3C validator