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

Theorem fodomr 7731
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  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  E. f 
f : A -onto-> B
)
Distinct variable groups:    A, f    B, f

Proof of Theorem fodomr
Dummy variables  g 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 7585 . . . 4  |-  Rel  ~<_
21brrelex2i 4894 . . 3  |-  ( B  ~<_  A  ->  A  e.  _V )
32adantl 468 . 2  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  A  e.  _V )
41brrelexi 4893 . . . 4  |-  ( B  ~<_  A  ->  B  e.  _V )
5 0sdomg 7709 . . . . 5  |-  ( B  e.  _V  ->  ( (/) 
~<  B  <->  B  =/=  (/) ) )
6 n0 3773 . . . . 5  |-  ( B  =/=  (/)  <->  E. z  z  e.  B )
75, 6syl6bb 265 . . . 4  |-  ( B  e.  _V  ->  ( (/) 
~<  B  <->  E. z  z  e.  B ) )
84, 7syl 17 . . 3  |-  ( B  ~<_  A  ->  ( (/)  ~<  B  <->  E. z 
z  e.  B ) )
98biimpac 489 . 2  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  E. z 
z  e.  B )
10 brdomi 7590 . . 3  |-  ( B  ~<_  A  ->  E. g 
g : B -1-1-> A
)
1110adantl 468 . 2  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  E. g 
g : B -1-1-> A
)
12 difexg 4571 . . . . . . . . . 10  |-  ( A  e.  _V  ->  ( A  \  ran  g )  e.  _V )
13 snex 4661 . . . . . . . . . 10  |-  { z }  e.  _V
14 xpexg 6606 . . . . . . . . . 10  |-  ( ( ( A  \  ran  g )  e.  _V  /\ 
{ z }  e.  _V )  ->  ( ( A  \  ran  g
)  X.  { z } )  e.  _V )
1512, 13, 14sylancl 667 . . . . . . . . 9  |-  ( A  e.  _V  ->  (
( A  \  ran  g )  X.  {
z } )  e. 
_V )
16 vex 3085 . . . . . . . . . 10  |-  g  e. 
_V
1716cnvex 6753 . . . . . . . . 9  |-  `' g  e.  _V
1815, 17jctil 540 . . . . . . . 8  |-  ( A  e.  _V  ->  ( `' g  e.  _V  /\  ( ( A  \  ran  g )  X.  {
z } )  e. 
_V ) )
19 unexb 6604 . . . . . . . 8  |-  ( ( `' g  e.  _V  /\  ( ( A  \  ran  g )  X.  {
z } )  e. 
_V )  <->  ( `' g  u.  ( ( A  \  ran  g )  X.  { z } ) )  e.  _V )
2018, 19sylib 200 . . . . . . 7  |-  ( A  e.  _V  ->  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  e.  _V )
21 df-f1 5605 . . . . . . . . . . . . 13  |-  ( g : B -1-1-> A  <->  ( g : B --> A  /\  Fun  `' g ) )
2221simprbi 466 . . . . . . . . . . . 12  |-  ( g : B -1-1-> A  ->  Fun  `' g )
23 vex 3085 . . . . . . . . . . . . . 14  |-  z  e. 
_V
2423fconst 5785 . . . . . . . . . . . . 13  |-  ( ( A  \  ran  g
)  X.  { z } ) : ( A  \  ran  g
) --> { z }
25 ffun 5747 . . . . . . . . . . . . 13  |-  ( ( ( A  \  ran  g )  X.  {
z } ) : ( A  \  ran  g ) --> { z }  ->  Fun  ( ( A  \  ran  g
)  X.  { z } ) )
2624, 25ax-mp 5 . . . . . . . . . . . 12  |-  Fun  (
( A  \  ran  g )  X.  {
z } )
2722, 26jctir 541 . . . . . . . . . . 11  |-  ( g : B -1-1-> A  -> 
( Fun  `' g  /\  Fun  ( ( A 
\  ran  g )  X.  { z } ) ) )
28 df-rn 4863 . . . . . . . . . . . . . 14  |-  ran  g  =  dom  `' g
2928eqcomi 2436 . . . . . . . . . . . . 13  |-  dom  `' g  =  ran  g
3023snnz 4117 . . . . . . . . . . . . . 14  |-  { z }  =/=  (/)
31 dmxp 5071 . . . . . . . . . . . . . 14  |-  ( { z }  =/=  (/)  ->  dom  ( ( A  \  ran  g )  X.  {
z } )  =  ( A  \  ran  g ) )
3230, 31ax-mp 5 . . . . . . . . . . . . 13  |-  dom  (
( A  \  ran  g )  X.  {
z } )  =  ( A  \  ran  g )
3329, 32ineq12i 3664 . . . . . . . . . . . 12  |-  ( dom  `' g  i^i  dom  (
( A  \  ran  g )  X.  {
z } ) )  =  ( ran  g  i^i  ( A  \  ran  g ) )
34 disjdif 3869 . . . . . . . . . . . 12  |-  ( ran  g  i^i  ( A 
\  ran  g )
)  =  (/)
3533, 34eqtri 2452 . . . . . . . . . . 11  |-  ( dom  `' g  i^i  dom  (
( A  \  ran  g )  X.  {
z } ) )  =  (/)
36 funun 5642 . . . . . . . . . . 11  |-  ( ( ( Fun  `' g  /\  Fun  ( ( A  \  ran  g
)  X.  { z } ) )  /\  ( dom  `' g  i^i 
dom  ( ( A 
\  ran  g )  X.  { z } ) )  =  (/) )  ->  Fun  ( `' g  u.  ( ( A  \  ran  g )  X.  {
z } ) ) )
3727, 35, 36sylancl 667 . . . . . . . . . 10  |-  ( g : B -1-1-> A  ->  Fun  ( `' g  u.  ( ( A  \  ran  g )  X.  {
z } ) ) )
3837adantl 468 . . . . . . . . 9  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  Fun  ( `' g  u.  ( ( A  \  ran  g )  X.  { z } ) ) )
39 dmun 5059 . . . . . . . . . . . 12  |-  dom  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  =  ( dom  `' g  u.  dom  ( ( A  \  ran  g
)  X.  { z } ) )
4028uneq1i 3618 . . . . . . . . . . . 12  |-  ( ran  g  u.  dom  (
( A  \  ran  g )  X.  {
z } ) )  =  ( dom  `' g  u.  dom  ( ( A  \  ran  g
)  X.  { z } ) )
4132uneq2i 3619 . . . . . . . . . . . 12  |-  ( ran  g  u.  dom  (
( A  \  ran  g )  X.  {
z } ) )  =  ( ran  g  u.  ( A  \  ran  g ) )
4239, 40, 413eqtr2i 2458 . . . . . . . . . . 11  |-  dom  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  =  ( ran  g  u.  ( A  \  ran  g ) )
43 f1f 5795 . . . . . . . . . . . . 13  |-  ( g : B -1-1-> A  -> 
g : B --> A )
44 frn 5751 . . . . . . . . . . . . 13  |-  ( g : B --> A  ->  ran  g  C_  A )
4543, 44syl 17 . . . . . . . . . . . 12  |-  ( g : B -1-1-> A  ->  ran  g  C_  A )
46 undif 3878 . . . . . . . . . . . 12  |-  ( ran  g  C_  A  <->  ( ran  g  u.  ( A  \  ran  g ) )  =  A )
4745, 46sylib 200 . . . . . . . . . . 11  |-  ( g : B -1-1-> A  -> 
( ran  g  u.  ( A  \  ran  g
) )  =  A )
4842, 47syl5eq 2476 . . . . . . . . . 10  |-  ( g : B -1-1-> A  ->  dom  ( `' g  u.  ( ( A  \  ran  g )  X.  {
z } ) )  =  A )
4948adantl 468 . . . . . . . . 9  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  dom  ( `' g  u.  ( ( A  \  ran  g )  X.  { z } ) )  =  A )
50 df-fn 5603 . . . . . . . . 9  |-  ( ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  Fn  A  <->  ( Fun  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  /\  dom  ( `' g  u.  ( ( A  \  ran  g
)  X.  { z } ) )  =  A ) )
5138, 49, 50sylanbrc 669 . . . . . . . 8  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  ( `' g  u.  ( ( A 
\  ran  g )  X.  { z } ) )  Fn  A )
52 rnun 5262 . . . . . . . . 9  |-  ran  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  =  ( ran  `' g  u.  ran  ( ( A  \  ran  g
)  X.  { z } ) )
53 dfdm4 5045 . . . . . . . . . . . 12  |-  dom  g  =  ran  `' g
54 f1dm 5799 . . . . . . . . . . . 12  |-  ( g : B -1-1-> A  ->  dom  g  =  B
)
5553, 54syl5eqr 2478 . . . . . . . . . . 11  |-  ( g : B -1-1-> A  ->  ran  `' g  =  B
)
5655uneq1d 3621 . . . . . . . . . 10  |-  ( g : B -1-1-> A  -> 
( ran  `' g  u.  ran  ( ( A 
\  ran  g )  X.  { z } ) )  =  ( B  u.  ran  ( ( A  \  ran  g
)  X.  { z } ) ) )
57 xpeq1 4866 . . . . . . . . . . . . . . . . 17  |-  ( ( A  \  ran  g
)  =  (/)  ->  (
( A  \  ran  g )  X.  {
z } )  =  ( (/)  X.  { z } ) )
58 0xp 4933 . . . . . . . . . . . . . . . . 17  |-  ( (/)  X. 
{ z } )  =  (/)
5957, 58syl6eq 2480 . . . . . . . . . . . . . . . 16  |-  ( ( A  \  ran  g
)  =  (/)  ->  (
( A  \  ran  g )  X.  {
z } )  =  (/) )
6059rneqd 5080 . . . . . . . . . . . . . . 15  |-  ( ( A  \  ran  g
)  =  (/)  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  =  ran  (/) )
61 rn0 5104 . . . . . . . . . . . . . . 15  |-  ran  (/)  =  (/)
6260, 61syl6eq 2480 . . . . . . . . . . . . . 14  |-  ( ( A  \  ran  g
)  =  (/)  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  =  (/) )
63 0ss 3793 . . . . . . . . . . . . . 14  |-  (/)  C_  B
6462, 63syl6eqss 3516 . . . . . . . . . . . . 13  |-  ( ( A  \  ran  g
)  =  (/)  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B )
6564a1d 27 . . . . . . . . . . . 12  |-  ( ( A  \  ran  g
)  =  (/)  ->  (
z  e.  B  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B ) )
66 rnxp 5285 . . . . . . . . . . . . . . 15  |-  ( ( A  \  ran  g
)  =/=  (/)  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  =  { z } )
6766adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( A  \  ran  g )  =/=  (/)  /\  z  e.  B )  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  =  { z } )
68 snssi 4143 . . . . . . . . . . . . . . 15  |-  ( z  e.  B  ->  { z }  C_  B )
6968adantl 468 . . . . . . . . . . . . . 14  |-  ( ( ( A  \  ran  g )  =/=  (/)  /\  z  e.  B )  ->  { z }  C_  B )
7067, 69eqsstrd 3500 . . . . . . . . . . . . 13  |-  ( ( ( A  \  ran  g )  =/=  (/)  /\  z  e.  B )  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B )
7170ex 436 . . . . . . . . . . . 12  |-  ( ( A  \  ran  g
)  =/=  (/)  ->  (
z  e.  B  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B ) )
7265, 71pm2.61ine 2738 . . . . . . . . . . 11  |-  ( z  e.  B  ->  ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B )
73 ssequn2 3641 . . . . . . . . . . 11  |-  ( ran  ( ( A  \  ran  g )  X.  {
z } )  C_  B 
<->  ( B  u.  ran  ( ( A  \  ran  g )  X.  {
z } ) )  =  B )
7472, 73sylib 200 . . . . . . . . . 10  |-  ( z  e.  B  ->  ( B  u.  ran  ( ( A  \  ran  g
)  X.  { z } ) )  =  B )
7556, 74sylan9eqr 2486 . . . . . . . . 9  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  ( ran  `' g  u.  ran  ( ( A  \  ran  g
)  X.  { z } ) )  =  B )
7652, 75syl5eq 2476 . . . . . . . 8  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  ran  ( `' g  u.  ( ( A  \  ran  g )  X.  { z } ) )  =  B )
77 df-fo 5606 . . . . . . . 8  |-  ( ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) ) : A -onto-> B  <->  ( ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  Fn  A  /\  ran  ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  =  B ) )
7851, 76, 77sylanbrc 669 . . . . . . 7  |-  ( ( z  e.  B  /\  g : B -1-1-> A )  ->  ( `' g  u.  ( ( A 
\  ran  g )  X.  { z } ) ) : A -onto-> B
)
79 foeq1 5805 . . . . . . . 8  |-  ( f  =  ( `' g  u.  ( ( A 
\  ran  g )  X.  { z } ) )  ->  ( f : A -onto-> B  <->  ( `' g  u.  ( ( A 
\  ran  g )  X.  { z } ) ) : A -onto-> B
) )
8079spcegv 3168 . . . . . . 7  |-  ( ( `' g  u.  (
( A  \  ran  g )  X.  {
z } ) )  e.  _V  ->  (
( `' g  u.  ( ( A  \  ran  g )  X.  {
z } ) ) : A -onto-> B  ->  E. f  f : A -onto-> B ) )
8120, 78, 80syl2im 40 . . . . . 6  |-  ( A  e.  _V  ->  (
( z  e.  B  /\  g : B -1-1-> A
)  ->  E. f 
f : A -onto-> B
) )
8281expdimp 439 . . . . 5  |-  ( ( A  e.  _V  /\  z  e.  B )  ->  ( g : B -1-1-> A  ->  E. f  f : A -onto-> B ) )
8382exlimdv 1769 . . . 4  |-  ( ( A  e.  _V  /\  z  e.  B )  ->  ( E. g  g : B -1-1-> A  ->  E. f  f : A -onto-> B ) )
8483ex 436 . . 3  |-  ( A  e.  _V  ->  (
z  e.  B  -> 
( E. g  g : B -1-1-> A  ->  E. f  f : A -onto-> B ) ) )
8584exlimdv 1769 . 2  |-  ( A  e.  _V  ->  ( E. z  z  e.  B  ->  ( E. g 
g : B -1-1-> A  ->  E. f  f : A -onto-> B ) ) )
863, 9, 11, 85syl3c 64 1  |-  ( (
(/)  ~<  B  /\  B  ~<_  A )  ->  E. f 
f : A -onto-> B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1438   E.wex 1660    e. wcel 1869    =/= wne 2619   _Vcvv 3082    \ cdif 3435    u. cun 3436    i^i cin 3437    C_ wss 3438   (/)c0 3763   {csn 3998   class class class wbr 4422    X. cxp 4850   `'ccnv 4851   dom cdm 4852   ran crn 4853   Fun wfun 5594    Fn wfn 5595   -->wf 5596   -1-1->wf1 5597   -onto->wfo 5598    ~<_ cdom 7577    ~< csdm 7578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4219  df-br 4423  df-opab 4482  df-mpt 4483  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-er 7373  df-en 7580  df-dom 7581  df-sdom 7582
This theorem is referenced by:  pwdom  7732  fodomfib  7859  domwdom  8097  iunfictbso  8551  fodomb  8960  brdom3  8962  konigthlem  8999  1stcfb  20456  ovoliunnul  22456  sigapildsys  28990  carsgclctunlem3  29158  ovoliunnfl  31944  voliunnfl  31946  volsupnfl  31947  nnfoctb  37292  caragenunicl  38172
  Copyright terms: Public domain W3C validator