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

Theorem fodomr 8399
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 8247 . . . 4 Rel ≼
21brrelex2i 5407 . . 3 (𝐵𝐴𝐴 ∈ V)
32adantl 475 . 2 ((∅ ≺ 𝐵𝐵𝐴) → 𝐴 ∈ V)
41brrelex1i 5406 . . . 4 (𝐵𝐴𝐵 ∈ V)
5 0sdomg 8377 . . . . 5 (𝐵 ∈ V → (∅ ≺ 𝐵𝐵 ≠ ∅))
6 n0 4158 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧𝐵)
75, 6syl6bb 279 . . . 4 (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧𝐵))
84, 7syl 17 . . 3 (𝐵𝐴 → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧𝐵))
98biimpac 472 . 2 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑧 𝑧𝐵)
10 brdomi 8252 . . 3 (𝐵𝐴 → ∃𝑔 𝑔:𝐵1-1𝐴)
1110adantl 475 . 2 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑔 𝑔:𝐵1-1𝐴)
12 difexg 5045 . . . . . . . . . 10 (𝐴 ∈ V → (𝐴 ∖ ran 𝑔) ∈ V)
13 snex 5140 . . . . . . . . . 10 {𝑧} ∈ V
14 xpexg 7237 . . . . . . . . . 10 (((𝐴 ∖ ran 𝑔) ∈ V ∧ {𝑧} ∈ V) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
1512, 13, 14sylancl 580 . . . . . . . . 9 (𝐴 ∈ V → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
16 vex 3400 . . . . . . . . . 10 𝑔 ∈ V
1716cnvex 7392 . . . . . . . . 9 𝑔 ∈ V
1815, 17jctil 515 . . . . . . . 8 (𝐴 ∈ V → (𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V))
19 unexb 7235 . . . . . . . 8 ((𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V) ↔ (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
2018, 19sylib 210 . . . . . . 7 (𝐴 ∈ V → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
21 df-f1 6140 . . . . . . . . . . . . 13 (𝑔:𝐵1-1𝐴 ↔ (𝑔:𝐵𝐴 ∧ Fun 𝑔))
2221simprbi 492 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → Fun 𝑔)
23 vex 3400 . . . . . . . . . . . . . 14 𝑧 ∈ V
2423fconst 6341 . . . . . . . . . . . . 13 ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧}
25 ffun 6294 . . . . . . . . . . . . 13 (((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝐴 ∖ ran 𝑔) × {𝑧}))
2624, 25ax-mp 5 . . . . . . . . . . . 12 Fun ((𝐴 ∖ ran 𝑔) × {𝑧})
2722, 26jctir 516 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → (Fun 𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})))
28 df-rn 5366 . . . . . . . . . . . . . 14 ran 𝑔 = dom 𝑔
2928eqcomi 2786 . . . . . . . . . . . . 13 dom 𝑔 = ran 𝑔
3023snnz 4541 . . . . . . . . . . . . . 14 {𝑧} ≠ ∅
31 dmxp 5589 . . . . . . . . . . . . . 14 ({𝑧} ≠ ∅ → dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)
3329, 32ineq12i 4034 . . . . . . . . . . . 12 (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔))
34 disjdif 4263 . . . . . . . . . . . 12 (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅
3533, 34eqtri 2801 . . . . . . . . . . 11 (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅
36 funun 6180 . . . . . . . . . . 11 (((Fun 𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ (dom 𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
3727, 35, 36sylancl 580 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
3837adantl 475 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
39 dmun 5576 . . . . . . . . . . . 12 dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
4028uneq1i 3985 . . . . . . . . . . . 12 (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
4132uneq2i 3986 . . . . . . . . . . . 12 (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
4239, 40, 413eqtr2i 2807 . . . . . . . . . . 11 dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
43 f1f 6351 . . . . . . . . . . . . 13 (𝑔:𝐵1-1𝐴𝑔:𝐵𝐴)
4443frnd 6298 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → ran 𝑔𝐴)
45 undif 4272 . . . . . . . . . . . 12 (ran 𝑔𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
4644, 45sylib 210 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
4742, 46syl5eq 2825 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
4847adantl 475 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
49 df-fn 6138 . . . . . . . . 9 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴))
5038, 48, 49sylanbrc 578 . . . . . . . 8 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴)
51 rnun 5795 . . . . . . . . 9 ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))
52 dfdm4 5561 . . . . . . . . . . . 12 dom 𝑔 = ran 𝑔
53 f1dm 6355 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐴 → dom 𝑔 = 𝐵)
5452, 53syl5eqr 2827 . . . . . . . . . . 11 (𝑔:𝐵1-1𝐴 → ran 𝑔 = 𝐵)
5554uneq1d 3988 . . . . . . . . . 10 (𝑔:𝐵1-1𝐴 → (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})))
56 xpeq1 5369 . . . . . . . . . . . . . . . . 17 ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧}))
57 0xp 5447 . . . . . . . . . . . . . . . . 17 (∅ × {𝑧}) = ∅
5856, 57syl6eq 2829 . . . . . . . . . . . . . . . 16 ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
5958rneqd 5598 . . . . . . . . . . . . . . 15 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅)
60 rn0 5623 . . . . . . . . . . . . . . 15 ran ∅ = ∅
6159, 60syl6eq 2829 . . . . . . . . . . . . . 14 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
62 0ss 4197 . . . . . . . . . . . . . 14 ∅ ⊆ 𝐵
6361, 62syl6eqss 3873 . . . . . . . . . . . . 13 ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
6463a1d 25 . . . . . . . . . . . 12 ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
65 rnxp 5818 . . . . . . . . . . . . . . 15 ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
6665adantr 474 . . . . . . . . . . . . . 14 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
67 snssi 4570 . . . . . . . . . . . . . . 15 (𝑧𝐵 → {𝑧} ⊆ 𝐵)
6867adantl 475 . . . . . . . . . . . . . 14 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → {𝑧} ⊆ 𝐵)
6966, 68eqsstrd 3857 . . . . . . . . . . . . 13 (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
7069ex 403 . . . . . . . . . . . 12 ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
7164, 70pm2.61ine 3052 . . . . . . . . . . 11 (𝑧𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
72 ssequn2 4008 . . . . . . . . . . 11 (ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7371, 72sylib 210 . . . . . . . . . 10 (𝑧𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7455, 73sylan9eqr 2835 . . . . . . . . 9 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (ran 𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
7551, 74syl5eq 2825 . . . . . . . 8 ((𝑧𝐵𝑔:𝐵1-1𝐴) → ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
76 df-fo 6141 . . . . . . . 8 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵 ↔ ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵))
7750, 75, 76sylanbrc 578 . . . . . . 7 ((𝑧𝐵𝑔:𝐵1-1𝐴) → (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵)
78 foeq1 6362 . . . . . . . 8 (𝑓 = (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝐴onto𝐵 ↔ (𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵))
7978spcegv 3495 . . . . . . 7 ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V → ((𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴onto𝐵 → ∃𝑓 𝑓:𝐴onto𝐵))
8020, 77, 79syl2im 40 . . . . . 6 (𝐴 ∈ V → ((𝑧𝐵𝑔:𝐵1-1𝐴) → ∃𝑓 𝑓:𝐴onto𝐵))
8180expdimp 446 . . . . 5 ((𝐴 ∈ V ∧ 𝑧𝐵) → (𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵))
8281exlimdv 1976 . . . 4 ((𝐴 ∈ V ∧ 𝑧𝐵) → (∃𝑔 𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵))
8382ex 403 . . 3 (𝐴 ∈ V → (𝑧𝐵 → (∃𝑔 𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵)))
8483exlimdv 1976 . 2 (𝐴 ∈ V → (∃𝑧 𝑧𝐵 → (∃𝑔 𝑔:𝐵1-1𝐴 → ∃𝑓 𝑓:𝐴onto𝐵)))
853, 9, 11, 84syl3c 66 1 ((∅ ≺ 𝐵𝐵𝐴) → ∃𝑓 𝑓:𝐴onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wex 1823  wcel 2106  wne 2968  Vcvv 3397  cdif 3788  cun 3789  cin 3790  wss 3791  c0 4140  {csn 4397   class class class wbr 4886   × cxp 5353  ccnv 5354  dom cdm 5355  ran crn 5356  Fun wfun 6129   Fn wfn 6130  wf 6131  1-1wf1 6132  ontowfo 6133  cdom 8239  csdm 8240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244
This theorem is referenced by:  pwdom  8400  fodomfib  8528  domwdom  8768  iunfictbso  9270  fodomb  9683  brdom3  9685  konigthlem  9725  1stcfb  21657  ovoliunnul  23711  sigapildsys  30823  carsgclctunlem3  30980  ovoliunnfl  34072  voliunnfl  34074  volsupnfl  34075  nnfoctb  40138  caragenunicl  41658
  Copyright terms: Public domain W3C validator