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

Theorem fodomfib 8787
Description: Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 9937 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.)
Assertion
Ref Expression
fodomfib (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴onto𝐵) ↔ (∅ ≺ 𝐵𝐵𝐴)))
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem fodomfib
StepHypRef Expression
1 fof 6587 . . . . . . . . . . . . 13 (𝑓:𝐴onto𝐵𝑓:𝐴𝐵)
21fdmd 6520 . . . . . . . . . . . 12 (𝑓:𝐴onto𝐵 → dom 𝑓 = 𝐴)
32eqeq1d 2828 . . . . . . . . . . 11 (𝑓:𝐴onto𝐵 → (dom 𝑓 = ∅ ↔ 𝐴 = ∅))
4 dm0rn0 5794 . . . . . . . . . . . 12 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
5 forn 6590 . . . . . . . . . . . . 13 (𝑓:𝐴onto𝐵 → ran 𝑓 = 𝐵)
65eqeq1d 2828 . . . . . . . . . . . 12 (𝑓:𝐴onto𝐵 → (ran 𝑓 = ∅ ↔ 𝐵 = ∅))
74, 6syl5bb 284 . . . . . . . . . . 11 (𝑓:𝐴onto𝐵 → (dom 𝑓 = ∅ ↔ 𝐵 = ∅))
83, 7bitr3d 282 . . . . . . . . . 10 (𝑓:𝐴onto𝐵 → (𝐴 = ∅ ↔ 𝐵 = ∅))
98necon3bid 3065 . . . . . . . . 9 (𝑓:𝐴onto𝐵 → (𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅))
109biimpac 479 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝑓:𝐴onto𝐵) → 𝐵 ≠ ∅)
1110adantll 710 . . . . . . 7 (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴onto𝐵) → 𝐵 ≠ ∅)
12 vex 3503 . . . . . . . . . . . 12 𝑓 ∈ V
1312rnex 7605 . . . . . . . . . . 11 ran 𝑓 ∈ V
145, 13syl6eqelr 2927 . . . . . . . . . 10 (𝑓:𝐴onto𝐵𝐵 ∈ V)
1514adantl 482 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝑓:𝐴onto𝐵) → 𝐵 ∈ V)
16 0sdomg 8635 . . . . . . . . 9 (𝐵 ∈ V → (∅ ≺ 𝐵𝐵 ≠ ∅))
1715, 16syl 17 . . . . . . . 8 ((𝐴 ∈ Fin ∧ 𝑓:𝐴onto𝐵) → (∅ ≺ 𝐵𝐵 ≠ ∅))
1817adantlr 711 . . . . . . 7 (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴onto𝐵) → (∅ ≺ 𝐵𝐵 ≠ ∅))
1911, 18mpbird 258 . . . . . 6 (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) ∧ 𝑓:𝐴onto𝐵) → ∅ ≺ 𝐵)
2019ex 413 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴onto𝐵 → ∅ ≺ 𝐵))
21 fodomfi 8786 . . . . . . 7 ((𝐴 ∈ Fin ∧ 𝑓:𝐴onto𝐵) → 𝐵𝐴)
2221ex 413 . . . . . 6 (𝐴 ∈ Fin → (𝑓:𝐴onto𝐵𝐵𝐴))
2322adantr 481 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴onto𝐵𝐵𝐴))
2420, 23jcad 513 . . . 4 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝑓:𝐴onto𝐵 → (∅ ≺ 𝐵𝐵𝐴)))
2524exlimdv 1927 . . 3 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (∃𝑓 𝑓:𝐴onto𝐵 → (∅ ≺ 𝐵𝐵𝐴)))
2625expimpd 454 . 2 (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴onto𝐵) → (∅ ≺ 𝐵𝐵𝐴)))
27 sdomdomtr 8639 . . . 4 ((∅ ≺ 𝐵𝐵𝐴) → ∅ ≺ 𝐴)
28 0sdomg 8635 . . . 4 (𝐴 ∈ Fin → (∅ ≺ 𝐴𝐴 ≠ ∅))
2927, 28syl5ib 245 . . 3 (𝐴 ∈ Fin → ((∅ ≺ 𝐵𝐵𝐴) → 𝐴 ≠ ∅))
30 fodomr 8657 . . 3 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑓 𝑓:𝐴onto𝐵)
3129, 30jca2 514 . 2 (𝐴 ∈ Fin → ((∅ ≺ 𝐵𝐵𝐴) → (𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴onto𝐵)))
3226, 31impbid 213 1 (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴onto𝐵) ↔ (∅ ≺ 𝐵𝐵𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wex 1773  wcel 2107  wne 3021  Vcvv 3500  c0 4295   class class class wbr 5063  dom cdm 5554  ran crn 5555  ontowfo 6350  cdom 8496  csdm 8497  Fincfn 8498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-om 7569  df-1o 8093  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator