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

Theorem fodomr 9075
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 8892 . . . 4 Rel ≼
21brrelex2i 5690 . . 3 (𝐵𝐴𝐴 ∈ V)
32adantl 483 . 2 ((∅ ≺ 𝐵𝐵𝐴) → 𝐴 ∈ V)
41brrelex1i 5689 . . . 4 (𝐵𝐴𝐵 ∈ V)
5 0sdomg 9051 . . . . 5 (𝐵 ∈ V → (∅ ≺ 𝐵𝐵 ≠ ∅))
6 n0 4307 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧𝐵)
75, 6bitrdi 287 . . . 4 (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧𝐵))
84, 7syl 17 . . 3 (𝐵𝐴 → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧𝐵))
98biimpac 480 . 2 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑧 𝑧𝐵)
10 brdomi 8901 . . 3 (𝐵𝐴 → ∃𝑔 𝑔:𝐵1-1𝐴)
1110adantl 483 . 2 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑔 𝑔:𝐵1-1𝐴)
12 difexg 5285 . . . . . . . . . 10 (𝐴 ∈ V → (𝐴 ∖ ran 𝑔) ∈ V)
13 vsnex 5387 . . . . . . . . . 10 {𝑧} ∈ V
14 xpexg 7685 . . . . . . . . . 10 (((𝐴 ∖ ran 𝑔) ∈ V ∧ {𝑧} ∈ V) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
1512, 13, 14sylancl 587 . . . . . . . . 9 (𝐴 ∈ V → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
16 vex 3448 . . . . . . . . . 10 𝑔 ∈ V
1716cnvex 7863 . . . . . . . . 9 𝑔 ∈ V
1815, 17jctil 521 . . . . . . . 8 (𝐴 ∈ V → (𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V))
19 unexb 7683 . . . . . . . 8 ((𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V) ↔ (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
2018, 19sylib 217 . . . . . . 7 (𝐴 ∈ V → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
21 df-f1 6502 . . . . . . . . . . . . 13 (𝑔:𝐵1-1𝐴 ↔ (𝑔:𝐵𝐴 ∧ Fun 𝑔))
2221simprbi 498 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → Fun 𝑔)
23 vex 3448 . . . . . . . . . . . . . 14 𝑧 ∈ V
2423fconst 6729 . . . . . . . . . . . . 13 ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧}
25 ffun 6672 . . . . . . . . . . . . 13 (((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝐴 ∖ ran 𝑔) × {𝑧}))
2624, 25ax-mp 5 . . . . . . . . . . . 12 Fun ((𝐴 ∖ ran 𝑔) × {𝑧})
2722, 26jctir 522 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → (Fun 𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})))
28 df-rn 5645 . . . . . . . . . . . . . 14 ran 𝑔 = dom 𝑔
2928eqcomi 2742 . . . . . . . . . . . . 13 dom 𝑔 = ran 𝑔
3023snnz 4738 . . . . . . . . . . . . . 14 {𝑧} ≠ ∅
31 dmxp 5885 . . . . . . . . . . . . . 14 ({𝑧} ≠ ∅ → dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)
3329, 32ineq12i 4171 . . . . . . . . . . . 12 (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔))
34 disjdif 4432 . . . . . . . . . . . 12 (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅
3533, 34eqtri 2761 . . . . . . . . . . 11 (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅
36 funun 6548 . . . . . . . . . . 11 (((Fun 𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
3727, 35, 36sylancl 587 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
3837adantl 483 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
39 dmun 5867 . . . . . . . . . . . 12 dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
4028uneq1i 4120 . . . . . . . . . . . 12 (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
4132uneq2i 4121 . . . . . . . . . . . 12 (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
4239, 40, 413eqtr2i 2767 . . . . . . . . . . 11 dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
43 f1f 6739 . . . . . . . . . . . . 13 (𝑔:𝐵1-1𝐴𝑔:𝐵𝐴)
4443frnd 6677 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → ran 𝑔𝐴)
45 undif 4442 . . . . . . . . . . . 12 (ran 𝑔𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
4644, 45sylib 217 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
4742, 46eqtrid 2785 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
4847adantl 483 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
49 df-fn 6500 . . . . . . . . 9 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴))
5038, 48, 49sylanbrc 584 . . . . . . . 8 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴)
51 rnun 6099 . . . . . . . . 9 ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))
52 dfdm4 5852 . . . . . . . . . . . 12 dom 𝑔 = ran 𝑔
53 f1dm 6743 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → dom 𝑔 = 𝐵)
5452, 53eqtr3id 2787 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → ran 𝑔 = 𝐵)
5554uneq1d 4123 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})))
56 xpeq1 5648 . . . . . . . . . . . . . . . . 17 ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧}))
57 0xp 5731 . . . . . . . . . . . . . . . . 17 (∅ × {𝑧}) = ∅
5856, 57eqtrdi 2789 . . . . . . . . . . . . . . . 16 ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
5958rneqd 5894 . . . . . . . . . . . . . . 15 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅)
60 rn0 5882 . . . . . . . . . . . . . . 15 ran ∅ = ∅
6159, 60eqtrdi 2789 . . . . . . . . . . . . . 14 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
62 0ss 4357 . . . . . . . . . . . . . 14 ∅ ⊆ 𝐵
6361, 62eqsstrdi 3999 . . . . . . . . . . . . 13 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
6463a1d 25 . . . . . . . . . . . 12 ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
65 rnxp 6123 . . . . . . . . . . . . . . 15 ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
6665adantr 482 . . . . . . . . . . . . . 14 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
67 snssi 4769 . . . . . . . . . . . . . . 15 (𝑧𝐵 → {𝑧} ⊆ 𝐵)
6867adantl 483 . . . . . . . . . . . . . 14 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → {𝑧} ⊆ 𝐵)
6966, 68eqsstrd 3983 . . . . . . . . . . . . 13 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
7069ex 414 . . . . . . . . . . . 12 ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
7164, 70pm2.61ine 3025 . . . . . . . . . . 11 (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
72 ssequn2 4144 . . . . . . . . . . 11 (ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7371, 72sylib 217 . . . . . . . . . 10 (𝑧𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7455, 73sylan9eqr 2795 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7551, 74eqtrid 2785 . . . . . . . 8 ((𝑧𝐵𝑔:𝐵1-1𝐴) → ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
76 df-fo 6503 . . . . . . . 8 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵 ↔ ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵))
7750, 75, 76sylanbrc 584 . . . . . . 7 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵)
78 foeq1 6753 . . . . . . . 8 (𝑓 = (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝐴onto𝐵 ↔ (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵))
7978spcegv 3555 . . . . . . 7 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V → ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵 → ∃𝑓 𝑓:𝐴onto𝐵))
8020, 77, 79syl2im 40 . . . . . 6 (𝐴 ∈ V → ((𝑧𝐵𝑔:𝐵1-1𝐴) → ∃𝑓 𝑓:𝐴onto𝐵))
8180expdimp 454 . . . . 5 ((𝐴 ∈ V ∧ 𝑧𝐵) → (𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵))
8281exlimdv 1937 . . . 4 ((𝐴 ∈ V ∧ 𝑧𝐵) → (∃𝑔 𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵))
8382ex 414 . . 3 (𝐴 ∈ V → (𝑧𝐵 → (∃𝑔 𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵)))
8483exlimdv 1937 . 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 397   = wceq 1542  wex 1782  wcel 2107  wne 2940  Vcvv 3444  cdif 3908  cun 3909  cin 3910  wss 3911  c0 4283  {csn 4587   class class class wbr 5106   × cxp 5632  ccnv 5633  dom cdm 5634  ran crn 5635  Fun wfun 6491   Fn wfn 6492  wf 6493  1-1wf1 6494  ontowfo 6495  cdom 8884  csdm 8885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-en 8887  df-dom 8888  df-sdom 8889
This theorem is referenced by:  pwdom  9076  fodomfib  9273  domwdom  9515  iunfictbso  10055  fodomb  10467  brdom3  10469  konigthlem  10509  1stcfb  22812  ovoliunnul  24887  sigapildsys  32818  carsgclctunlem3  32977  ovoliunnfl  36166  voliunnfl  36168  volsupnfl  36169  nnfoctb  43343  caragenunicl  44851
  Copyright terms: Public domain W3C validator