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

Theorem fodomfi 9269
Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 10459 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 6761 . . 3 (𝐹:𝐴onto𝐵 → (𝐹𝐴) = 𝐵)
21adantl 482 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → (𝐹𝐴) = 𝐵)
3 imaeq2 6009 . . . . . . 7 (𝑥 = ∅ → (𝐹𝑥) = (𝐹 “ ∅))
4 ima0 6029 . . . . . . 7 (𝐹 “ ∅) = ∅
53, 4eqtrdi 2792 . . . . . 6 (𝑥 = ∅ → (𝐹𝑥) = ∅)
6 id 22 . . . . . 6 (𝑥 = ∅ → 𝑥 = ∅)
75, 6breq12d 5118 . . . . 5 (𝑥 = ∅ → ((𝐹𝑥) ≼ 𝑥 ↔ ∅ ≼ ∅))
87imbi2d 340 . . . 4 (𝑥 = ∅ → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → ∅ ≼ ∅)))
9 imaeq2 6009 . . . . . 6 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
10 id 22 . . . . . 6 (𝑥 = 𝑦𝑥 = 𝑦)
119, 10breq12d 5118 . . . . 5 (𝑥 = 𝑦 → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹𝑦) ≼ 𝑦))
1211imbi2d 340 . . . 4 (𝑥 = 𝑦 → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹𝑦) ≼ 𝑦)))
13 imaeq2 6009 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹𝑥) = (𝐹 “ (𝑦 ∪ {𝑧})))
14 id 22 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = (𝑦 ∪ {𝑧}))
1513, 14breq12d 5118 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))
1615imbi2d 340 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
17 imaeq2 6009 . . . . . 6 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
18 id 22 . . . . . 6 (𝑥 = 𝐴𝑥 = 𝐴)
1917, 18breq12d 5118 . . . . 5 (𝑥 = 𝐴 → ((𝐹𝑥) ≼ 𝑥 ↔ (𝐹𝐴) ≼ 𝐴))
2019imbi2d 340 . . . 4 (𝑥 = 𝐴 → ((𝐹 Fn 𝐴 → (𝐹𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹𝐴) ≼ 𝐴)))
21 0ex 5264 . . . . . 6 ∅ ∈ V
22210dom 9050 . . . . 5 ∅ ≼ ∅
2322a1i 11 . . . 4 (𝐹 Fn 𝐴 → ∅ ≼ ∅)
24 fnfun 6602 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → Fun 𝐹)
2524ad2antrl 726 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → Fun 𝐹)
26 funressn 7105 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝐹 ↾ {𝑧}) ⊆ {⟨𝑧, (𝐹𝑧)⟩})
27 rnss 5894 . . . . . . . . . . . . 13 ((𝐹 ↾ {𝑧}) ⊆ {⟨𝑧, (𝐹𝑧)⟩} → ran (𝐹 ↾ {𝑧}) ⊆ ran {⟨𝑧, (𝐹𝑧)⟩})
2825, 26, 273syl 18 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ran (𝐹 ↾ {𝑧}) ⊆ ran {⟨𝑧, (𝐹𝑧)⟩})
29 df-ima 5646 . . . . . . . . . . . 12 (𝐹 “ {𝑧}) = ran (𝐹 ↾ {𝑧})
30 vex 3449 . . . . . . . . . . . . . 14 𝑧 ∈ V
3130rnsnop 6176 . . . . . . . . . . . . 13 ran {⟨𝑧, (𝐹𝑧)⟩} = {(𝐹𝑧)}
3231eqcomi 2745 . . . . . . . . . . . 12 {(𝐹𝑧)} = ran {⟨𝑧, (𝐹𝑧)⟩}
3328, 29, 323sstr4g 3989 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)})
34 snex 5388 . . . . . . . . . . 11 {(𝐹𝑧)} ∈ V
35 ssexg 5280 . . . . . . . . . . 11 (((𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)} ∧ {(𝐹𝑧)} ∈ V) → (𝐹 “ {𝑧}) ∈ V)
3633, 34, 35sylancl 586 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ∈ V)
37 fvi 6917 . . . . . . . . . 10 ((𝐹 “ {𝑧}) ∈ V → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧}))
3836, 37syl 17 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧}))
3938uneq2d 4123 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = ((𝐹𝑦) ∪ (𝐹 “ {𝑧})))
40 imaundi 6102 . . . . . . . 8 (𝐹 “ (𝑦 ∪ {𝑧})) = ((𝐹𝑦) ∪ (𝐹 “ {𝑧}))
4139, 40eqtr4di 2794 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = (𝐹 “ (𝑦 ∪ {𝑧})))
42 simprr 771 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹𝑦) ≼ 𝑦)
43 ssdomg 8940 . . . . . . . . . . 11 ({(𝐹𝑧)} ∈ V → ((𝐹 “ {𝑧}) ⊆ {(𝐹𝑧)} → (𝐹 “ {𝑧}) ≼ {(𝐹𝑧)}))
4434, 33, 43mpsyl 68 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {(𝐹𝑧)})
45 fvex 6855 . . . . . . . . . . . 12 (𝐹𝑧) ∈ V
4645ensn1 8961 . . . . . . . . . . 11 {(𝐹𝑧)} ≈ 1o
4730ensn1 8961 . . . . . . . . . . 11 {𝑧} ≈ 1o
4846, 47entr4i 8951 . . . . . . . . . 10 {(𝐹𝑧)} ≈ {𝑧}
49 domentr 8953 . . . . . . . . . 10 (((𝐹 “ {𝑧}) ≼ {(𝐹𝑧)} ∧ {(𝐹𝑧)} ≈ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧})
5044, 48, 49sylancl 586 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {𝑧})
5138, 50eqbrtrd 5127 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧})
52 simplr 767 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ¬ 𝑧𝑦)
53 disjsn 4672 . . . . . . . . 9 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
5452, 53sylibr 233 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅)
55 undom 9003 . . . . . . . 8 ((((𝐹𝑦) ≼ 𝑦 ∧ ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧}))
5642, 51, 54, 55syl21anc 836 . . . . . . 7 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → ((𝐹𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧}))
5741, 56eqbrtrrd 5129 . . . . . 6 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹𝑦) ≼ 𝑦)) → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))
5857exp32 421 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝐹 Fn 𝐴 → ((𝐹𝑦) ≼ 𝑦 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
5958a2d 29 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐹 Fn 𝐴 → (𝐹𝑦) ≼ 𝑦) → (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))))
608, 12, 16, 20, 23, 59findcard2s 9109 . . 3 (𝐴 ∈ Fin → (𝐹 Fn 𝐴 → (𝐹𝐴) ≼ 𝐴))
61 fofn 6758 . . 3 (𝐹:𝐴onto𝐵𝐹 Fn 𝐴)
6260, 61impel 506 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → (𝐹𝐴) ≼ 𝐴)
632, 62eqbrtrrd 5129 1 ((𝐴 ∈ Fin ∧ 𝐹:𝐴onto𝐵) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wcel 2106  Vcvv 3445  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586  cop 4592   class class class wbr 5105   I cid 5530  ran crn 5634  cres 5635  cima 5636  Fun wfun 6490   Fn wfn 6491  ontowfo 6494  cfv 6496  1oc1o 8405  cen 8880  cdom 8881  Fincfn 8883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-fin 8887
This theorem is referenced by:  fodomfib  9270  fofinf1o  9271  fidomdm  9273  fofi  9282  pwfilemOLD  9290  cmpsub  22751  alexsubALT  23402  phpreu  36062  poimirlem26  36104
  Copyright terms: Public domain W3C validator