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

Theorem fodomr 7423
Description: There exists a mapping from a set onto any (non-empty) set that it dominates. (Contributed by NM, 23-Mar-2006.)
Assertion
Ref Expression
fodomr
Distinct variable groups:   ,   ,

Proof of Theorem fodomr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 7279 . . . 4
21brrelex2i 4902 . . 3
32adantl 454 . 2
41brrelexi 4901 . . . 4
5 0sdomg 7401 . . . . 5
6 n0 3682 . . . . 5
75, 6syl6bb 254 . . . 4
84, 7syl 16 . . 3
98biimpac 474 . 2
10 brdomi 7283 . . 3
1110adantl 454 . 2
12 difexg 4466 . . . . . . . . . 10
13 snex 4556 . . . . . . . . . 10
14 xpexg 6517 . . . . . . . . . 10
1512, 13, 14sylancl 645 . . . . . . . . 9
16 vex 3018 . . . . . . . . . 10
1716cnvex 6533 . . . . . . . . 9
1815, 17jctil 525 . . . . . . . 8
19 unexb 6390 . . . . . . . 8
2018, 19sylib 190 . . . . . . 7
21 df-f1 5443 . . . . . . . . . . . . 13
2221simprbi 452 . . . . . . . . . . . 12
23 vex 3018 . . . . . . . . . . . . . 14
2423fconst 5613 . . . . . . . . . . . . 13
25 ffun 5579 . . . . . . . . . . . . 13
2624, 25ax-mp 5 . . . . . . . . . . . 12
2722, 26jctir 526 . . . . . . . . . . 11
28 df-rn 4873 . . . . . . . . . . . . . 14
2928eqcomi 2493 . . . . . . . . . . . . 13
3023snnz 4022 . . . . . . . . . . . . . 14
31 dmxp 5080 . . . . . . . . . . . . . 14
3230, 31ax-mp 5 . . . . . . . . . . . . 13
3329, 32ineq12i 3586 . . . . . . . . . . . 12
34 disjdif 3786 . . . . . . . . . . . 12
3533, 34eqtri 2509 . . . . . . . . . . 11
36 funun 5480 . . . . . . . . . . 11
3727, 35, 36sylancl 645 . . . . . . . . . 10
3837adantl 454 . . . . . . . . 9
39 dmun 5068 . . . . . . . . . . . 12
4028uneq1i 3543 . . . . . . . . . . . 12
4132uneq2i 3544 . . . . . . . . . . . 12
4239, 40, 413eqtr2i 2515 . . . . . . . . . . 11
43 f1f 5623 . . . . . . . . . . . . 13
44 frn 5583 . . . . . . . . . . . . 13
4543, 44syl 16 . . . . . . . . . . . 12
46 undif 3794 . . . . . . . . . . . 12
4745, 46sylib 190 . . . . . . . . . . 11
4842, 47syl5eq 2533 . . . . . . . . . 10
4948adantl 454 . . . . . . . . 9
50 df-fn 5441 . . . . . . . . 9
5138, 49, 50sylanbrc 647 . . . . . . . 8
52 rnun 5267 . . . . . . . . 9
53 dfdm4 5054 . . . . . . . . . . . 12
54 f1dm 5627 . . . . . . . . . . . 12
5553, 54syl5eqr 2535 . . . . . . . . . . 11
5655uneq1d 3546 . . . . . . . . . 10
57 xpeq1 4876 . . . . . . . . . . . . . . . . 17
58 0xp 4939 . . . . . . . . . . . . . . . . 17
5957, 58syl6eq 2537 . . . . . . . . . . . . . . . 16
6059rneqd 5089 . . . . . . . . . . . . . . 15
61 rn0 5113 . . . . . . . . . . . . . . 15
6260, 61syl6eq 2537 . . . . . . . . . . . . . 14
63 0ss 3701 . . . . . . . . . . . . . 14
6462, 63syl6eqss 3443 . . . . . . . . . . . . 13
6564a1d 24 . . . . . . . . . . . 12
66 rnxp 5289 . . . . . . . . . . . . . . 15
6766adantr 453 . . . . . . . . . . . . . 14
68 snssi 4042 . . . . . . . . . . . . . . 15
6968adantl 454 . . . . . . . . . . . . . 14
7067, 69eqsstrd 3427 . . . . . . . . . . . . 13
7170ex 425 . . . . . . . . . . . 12
7265, 71pm2.61ine 2733 . . . . . . . . . . 11
73 ssequn2 3566 . . . . . . . . . . 11
7472, 73sylib 190 . . . . . . . . . 10
7556, 74sylan9eqr 2543 . . . . . . . . 9
7652, 75syl5eq 2533 . . . . . . . 8
77 df-fo 5444 . . . . . . . 8
7851, 76, 77sylanbrc 647 . . . . . . 7
79 foeq1 5633 . . . . . . . 8
8079spcegv 3098 . . . . . . 7
8120, 78, 80syl2im 37 . . . . . 6
8281expdimp 428 . . . . 5
8382exlimdv 1664 . . . 4
8483ex 425 . . 3
8584exlimdv 1664 . 2
863, 9, 11, 85syl3c 60 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  E.wex 1565  =wceq 1670  e.wcel 1732  =/=wne 2652   cvv 3015  \cdif 3362  u.cun 3363  i^icin 3364  C_wss 3365   c0 3673  {csn 3909   class class class wbr 4318  X.cxp 4860  `'ccnv 4861  domcdm 4862  rancrn 4863  Funwfun 5432  Fnwfn 5433  -->wf 5434  -1-1->wf1 5435  -onto->wfo 5436   cdom 7271   csdm 7272
This theorem is referenced by:  pwdom  7424  fodomfib  7552  domwdom  7709  iunfictbso  8166  fodomb  8575  brdom3  8577  konigthlem  8614  1stcfb  18523  ovoliunnul  20418  ovoliunnfl  27613  voliunnfl  27615  volsupnfl  27616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-mpt 4378  df-id 4657  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-er 7067  df-en 7274  df-dom 7275  df-sdom 7276
  Copyright terms: Public domain W3C validator