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

Theorem fodomr 8972
Description: There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.)
Assertion
Ref Expression
fodomr ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑓 𝑓:𝐴onto𝐵)
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem fodomr
Dummy variables 𝑔 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 8789 . . . 4 Rel ≼
21brrelex2i 5663 . . 3 (𝐵𝐴𝐴 ∈ V)
32adantl 482 . 2 ((∅ ≺ 𝐵𝐵𝐴) → 𝐴 ∈ V)
41brrelex1i 5662 . . . 4 (𝐵𝐴𝐵 ∈ V)
5 0sdomg 8948 . . . . 5 (𝐵 ∈ V → (∅ ≺ 𝐵𝐵 ≠ ∅))
6 n0 4291 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧𝐵)
75, 6bitrdi 286 . . . 4 (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧𝐵))
84, 7syl 17 . . 3 (𝐵𝐴 → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧𝐵))
98biimpac 479 . 2 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑧 𝑧𝐵)
10 brdomi 8798 . . 3 (𝐵𝐴 → ∃𝑔 𝑔:𝐵1-1𝐴)
1110adantl 482 . 2 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑔 𝑔:𝐵1-1𝐴)
12 difexg 5266 . . . . . . . . . 10 (𝐴 ∈ V → (𝐴 ∖ ran 𝑔) ∈ V)
13 snex 5369 . . . . . . . . . 10 {𝑧} ∈ V
14 xpexg 7642 . . . . . . . . . 10 (((𝐴 ∖ ran 𝑔) ∈ V ∧ {𝑧} ∈ V) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
1512, 13, 14sylancl 586 . . . . . . . . 9 (𝐴 ∈ V → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
16 vex 3445 . . . . . . . . . 10 𝑔 ∈ V
1716cnvex 7819 . . . . . . . . 9 𝑔 ∈ V
1815, 17jctil 520 . . . . . . . 8 (𝐴 ∈ V → (𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V))
19 unexb 7640 . . . . . . . 8 ((𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V) ↔ (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
2018, 19sylib 217 . . . . . . 7 (𝐴 ∈ V → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
21 df-f1 6471 . . . . . . . . . . . . 13 (𝑔:𝐵1-1𝐴 ↔ (𝑔:𝐵𝐴 ∧ Fun 𝑔))
2221simprbi 497 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → Fun 𝑔)
23 vex 3445 . . . . . . . . . . . . . 14 𝑧 ∈ V
2423fconst 6698 . . . . . . . . . . . . 13 ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧}
25 ffun 6641 . . . . . . . . . . . . 13 (((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝐴 ∖ ran 𝑔) × {𝑧}))
2624, 25ax-mp 5 . . . . . . . . . . . 12 Fun ((𝐴 ∖ ran 𝑔) × {𝑧})
2722, 26jctir 521 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → (Fun 𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})))
28 df-rn 5619 . . . . . . . . . . . . . 14 ran 𝑔 = dom 𝑔
2928eqcomi 2746 . . . . . . . . . . . . 13 dom 𝑔 = ran 𝑔
3023snnz 4722 . . . . . . . . . . . . . 14 {𝑧} ≠ ∅
31 dmxp 5858 . . . . . . . . . . . . . 14 ({𝑧} ≠ ∅ → dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)
3329, 32ineq12i 4155 . . . . . . . . . . . 12 (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔))
34 disjdif 4416 . . . . . . . . . . . 12 (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅
3533, 34eqtri 2765 . . . . . . . . . . 11 (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅
36 funun 6517 . . . . . . . . . . 11 (((Fun 𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
3727, 35, 36sylancl 586 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
3837adantl 482 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
39 dmun 5840 . . . . . . . . . . . 12 dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
4028uneq1i 4104 . . . . . . . . . . . 12 (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
4132uneq2i 4105 . . . . . . . . . . . 12 (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
4239, 40, 413eqtr2i 2771 . . . . . . . . . . 11 dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
43 f1f 6708 . . . . . . . . . . . . 13 (𝑔:𝐵1-1𝐴𝑔:𝐵𝐴)
4443frnd 6646 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → ran 𝑔𝐴)
45 undif 4426 . . . . . . . . . . . 12 (ran 𝑔𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
4644, 45sylib 217 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
4742, 46eqtrid 2789 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
4847adantl 482 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
49 df-fn 6469 . . . . . . . . 9 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴))
5038, 48, 49sylanbrc 583 . . . . . . . 8 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴)
51 rnun 6072 . . . . . . . . 9 ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))
52 dfdm4 5825 . . . . . . . . . . . 12 dom 𝑔 = ran 𝑔
53 f1dm 6712 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → dom 𝑔 = 𝐵)
5452, 53eqtr3id 2791 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → ran 𝑔 = 𝐵)
5554uneq1d 4107 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})))
56 xpeq1 5622 . . . . . . . . . . . . . . . . 17 ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧}))
57 0xp 5704 . . . . . . . . . . . . . . . . 17 (∅ × {𝑧}) = ∅
5856, 57eqtrdi 2793 . . . . . . . . . . . . . . . 16 ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
5958rneqd 5867 . . . . . . . . . . . . . . 15 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅)
60 rn0 5855 . . . . . . . . . . . . . . 15 ran ∅ = ∅
6159, 60eqtrdi 2793 . . . . . . . . . . . . . 14 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
62 0ss 4341 . . . . . . . . . . . . . 14 ∅ ⊆ 𝐵
6361, 62eqsstrdi 3985 . . . . . . . . . . . . 13 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
6463a1d 25 . . . . . . . . . . . 12 ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
65 rnxp 6096 . . . . . . . . . . . . . . 15 ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
6665adantr 481 . . . . . . . . . . . . . 14 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
67 snssi 4753 . . . . . . . . . . . . . . 15 (𝑧𝐵 → {𝑧} ⊆ 𝐵)
6867adantl 482 . . . . . . . . . . . . . 14 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → {𝑧} ⊆ 𝐵)
6966, 68eqsstrd 3969 . . . . . . . . . . . . 13 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
7069ex 413 . . . . . . . . . . . 12 ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
7164, 70pm2.61ine 3026 . . . . . . . . . . 11 (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
72 ssequn2 4128 . . . . . . . . . . 11 (ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7371, 72sylib 217 . . . . . . . . . 10 (𝑧𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7455, 73sylan9eqr 2799 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7551, 74eqtrid 2789 . . . . . . . 8 ((𝑧𝐵𝑔:𝐵1-1𝐴) → ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
76 df-fo 6472 . . . . . . . 8 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵 ↔ ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵))
7750, 75, 76sylanbrc 583 . . . . . . 7 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵)
78 foeq1 6722 . . . . . . . 8 (𝑓 = (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝐴onto𝐵 ↔ (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵))
7978spcegv 3545 . . . . . . 7 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V → ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵 → ∃𝑓 𝑓:𝐴onto𝐵))
8020, 77, 79syl2im 40 . . . . . 6 (𝐴 ∈ V → ((𝑧𝐵𝑔:𝐵1-1𝐴) → ∃𝑓 𝑓:𝐴onto𝐵))
8180expdimp 453 . . . . 5 ((𝐴 ∈ V ∧ 𝑧𝐵) → (𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵))
8281exlimdv 1935 . . . 4 ((𝐴 ∈ V ∧ 𝑧𝐵) → (∃𝑔 𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵))
8382ex 413 . . 3 (𝐴 ∈ V → (𝑧𝐵 → (∃𝑔 𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵)))
8483exlimdv 1935 . 2 (𝐴 ∈ V → (∃𝑧 𝑧𝐵 → (∃𝑔 𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵)))
853, 9, 11, 84syl3c 66 1 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑓 𝑓:𝐴onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wex 1780  wcel 2105  wne 2941  Vcvv 3441  cdif 3894  cun 3895  cin 3896  wss 3897  c0 4267  {csn 4571   class class class wbr 5087   × cxp 5606  ccnv 5607  dom cdm 5608  ran crn 5609  Fun wfun 6460   Fn wfn 6461  wf 6462  1-1wf1 6463  ontowfo 6464  cdom 8781  csdm 8782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-en 8784  df-dom 8785  df-sdom 8786
This theorem is referenced by:  pwdom  8973  fodomfib  9170  domwdom  9410  iunfictbso  9950  fodomb  10362  brdom3  10364  konigthlem  10404  1stcfb  22679  ovoliunnul  24754  sigapildsys  32270  carsgclctunlem3  32427  ovoliunnfl  35891  voliunnfl  35893  volsupnfl  35894  nnfoctb  42829  caragenunicl  44313
  Copyright terms: Public domain W3C validator