ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exmidfodomrlemim Unicode version

Theorem exmidfodomrlemim 6764
Description: Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
Assertion
Ref Expression
exmidfodomrlemim  |-  (EXMID  ->  A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y ) )
Distinct variable groups:    x, f, z   
y, f, z

Proof of Theorem exmidfodomrlemim
Dummy variables  g  u  v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdomi 6412 . . . . 5  |-  ( y  ~<_  x  ->  E. g 
g : y -1-1-> x
)
21ad2antll 475 . . . 4  |-  ( (EXMID  /\  ( E. z  z  e.  y  /\  y  ~<_  x ) )  ->  E. g  g :
y -1-1-> x )
3 df-f1 4983 . . . . . . . . . . . . . . . . 17  |-  ( g : y -1-1-> x  <->  ( g : y --> x  /\  Fun  `' g ) )
43simprbi 269 . . . . . . . . . . . . . . . 16  |-  ( g : y -1-1-> x  ->  Fun  `' g )
5 vex 2618 . . . . . . . . . . . . . . . . . 18  |-  z  e. 
_V
65fconst 5163 . . . . . . . . . . . . . . . . 17  |-  ( ( x  \  ran  g
)  X.  { z } ) : ( x  \  ran  g
) --> { z }
7 ffun 5126 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  \  ran  g )  X.  {
z } ) : ( x  \  ran  g ) --> { z }  ->  Fun  ( ( x  \  ran  g
)  X.  { z } ) )
86, 7ax-mp 7 . . . . . . . . . . . . . . . 16  |-  Fun  (
( x  \  ran  g )  X.  {
z } )
94, 8jctir 306 . . . . . . . . . . . . . . 15  |-  ( g : y -1-1-> x  -> 
( Fun  `' g  /\  Fun  ( ( x 
\  ran  g )  X.  { z } ) ) )
10 df-rn 4421 . . . . . . . . . . . . . . . . . 18  |-  ran  g  =  dom  `' g
1110eqcomi 2089 . . . . . . . . . . . . . . . . 17  |-  dom  `' g  =  ran  g
125snm 3543 . . . . . . . . . . . . . . . . . 18  |-  E. w  w  e.  { z }
13 dmxpm 4623 . . . . . . . . . . . . . . . . . 18  |-  ( E. w  w  e.  {
z }  ->  dom  ( ( x  \  ran  g )  X.  {
z } )  =  ( x  \  ran  g ) )
1412, 13ax-mp 7 . . . . . . . . . . . . . . . . 17  |-  dom  (
( x  \  ran  g )  X.  {
z } )  =  ( x  \  ran  g )
1511, 14ineq12i 3188 . . . . . . . . . . . . . . . 16  |-  ( dom  `' g  i^i  dom  (
( x  \  ran  g )  X.  {
z } ) )  =  ( ran  g  i^i  ( x  \  ran  g ) )
16 disjdif 3343 . . . . . . . . . . . . . . . 16  |-  ( ran  g  i^i  ( x 
\  ran  g )
)  =  (/)
1715, 16eqtri 2105 . . . . . . . . . . . . . . 15  |-  ( dom  `' g  i^i  dom  (
( x  \  ran  g )  X.  {
z } ) )  =  (/)
18 funun 5020 . . . . . . . . . . . . . . 15  |-  ( ( ( Fun  `' g  /\  Fun  ( ( x  \  ran  g
)  X.  { z } ) )  /\  ( dom  `' g  i^i 
dom  ( ( x 
\  ran  g )  X.  { z } ) )  =  (/) )  ->  Fun  ( `' g  u.  ( ( x  \  ran  g )  X.  {
z } ) ) )
199, 17, 18sylancl 404 . . . . . . . . . . . . . 14  |-  ( g : y -1-1-> x  ->  Fun  ( `' g  u.  ( ( x  \  ran  g )  X.  {
z } ) ) )
2019adantl 271 . . . . . . . . . . . . 13  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  ->  Fun  ( `' g  u.  ( ( x  \  ran  g )  X.  {
z } ) ) )
21 f1rn 5174 . . . . . . . . . . . . . . . 16  |-  ( g : y -1-1-> x  ->  ran  g  C_  x )
2221adantl 271 . . . . . . . . . . . . . . 15  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  ->  ran  g  C_  x )
23 exmidexmid 4004 . . . . . . . . . . . . . . . . 17  |-  (EXMID  -> DECID  u  e.  ran  g )
2423ralrimivw 2443 . . . . . . . . . . . . . . . 16  |-  (EXMID  ->  A. u  e.  x DECID  u  e.  ran  g )
2524ad2antrr 472 . . . . . . . . . . . . . . 15  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  ->  A. u  e.  x DECID  u  e.  ran  g )
26 undifdcss 6579 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ran  g  u.  ( x  \  ran  g ) )  <->  ( ran  g  C_  x  /\  A. u  e.  x DECID  u  e.  ran  g ) )
2722, 25, 26sylanbrc 408 . . . . . . . . . . . . . 14  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  ->  x  =  ( ran  g  u.  ( x  \  ran  g ) ) )
28 dmun 4610 . . . . . . . . . . . . . . 15  |-  dom  ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) )  =  ( dom  `' g  u.  dom  ( ( x  \  ran  g
)  X.  { z } ) )
2910uneq1i 3139 . . . . . . . . . . . . . . 15  |-  ( ran  g  u.  dom  (
( x  \  ran  g )  X.  {
z } ) )  =  ( dom  `' g  u.  dom  ( ( x  \  ran  g
)  X.  { z } ) )
3014uneq2i 3140 . . . . . . . . . . . . . . 15  |-  ( ran  g  u.  dom  (
( x  \  ran  g )  X.  {
z } ) )  =  ( ran  g  u.  ( x  \  ran  g ) )
3128, 29, 303eqtr2i 2111 . . . . . . . . . . . . . 14  |-  dom  ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) )  =  ( ran  g  u.  ( x  \  ran  g ) )
3227, 31syl6reqr 2136 . . . . . . . . . . . . 13  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  ->  dom  ( `' g  u.  ( ( x  \  ran  g )  X.  {
z } ) )  =  x )
33 df-fn 4981 . . . . . . . . . . . . 13  |-  ( ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) )  Fn  x  <->  ( Fun  ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) )  /\  dom  ( `' g  u.  ( ( x  \  ran  g
)  X.  { z } ) )  =  x ) )
3420, 32, 33sylanbrc 408 . . . . . . . . . . . 12  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  -> 
( `' g  u.  ( ( x  \  ran  g )  X.  {
z } ) )  Fn  x )
35 rnun 4803 . . . . . . . . . . . . 13  |-  ran  ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) )  =  ( ran  `' g  u.  ran  ( ( x  \  ran  g
)  X.  { z } ) )
36 dfdm4 4595 . . . . . . . . . . . . . . . 16  |-  dom  g  =  ran  `' g
37 f1dm 5178 . . . . . . . . . . . . . . . 16  |-  ( g : y -1-1-> x  ->  dom  g  =  y
)
3836, 37syl5eqr 2131 . . . . . . . . . . . . . . 15  |-  ( g : y -1-1-> x  ->  ran  `' g  =  y
)
3938uneq1d 3142 . . . . . . . . . . . . . 14  |-  ( g : y -1-1-> x  -> 
( ran  `' g  u.  ran  ( ( x 
\  ran  g )  X.  { z } ) )  =  ( y  u.  ran  ( ( x  \  ran  g
)  X.  { z } ) ) )
40 exmidexmid 4004 . . . . . . . . . . . . . . . . . 18  |-  (EXMID  -> DECID  E. v  v  e.  ( x  \  ran  g ) )
41 exmiddc 780 . . . . . . . . . . . . . . . . . 18  |-  (DECID  E. v 
v  e.  ( x 
\  ran  g )  ->  ( E. v  v  e.  ( x  \  ran  g )  \/  -.  E. v  v  e.  ( x  \  ran  g
) ) )
4240, 41syl 14 . . . . . . . . . . . . . . . . 17  |-  (EXMID  ->  ( E. v  v  e.  ( x  \  ran  g
)  \/  -.  E. v  v  e.  (
x  \  ran  g ) ) )
43 rnxpm 4823 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. v  v  e.  ( x  \  ran  g
)  ->  ran  ( ( x  \  ran  g
)  X.  { z } )  =  {
z } )
4443adantr 270 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E. v  v  e.  ( x  \  ran  g )  /\  z  e.  y )  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  =  { z } )
45 snssi 3564 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  y  ->  { z }  C_  y )
4645adantl 271 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E. v  v  e.  ( x  \  ran  g )  /\  z  e.  y )  ->  { z }  C_  y )
4744, 46eqsstrd 3049 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E. v  v  e.  ( x  \  ran  g )  /\  z  e.  y )  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  C_  y )
4847ex 113 . . . . . . . . . . . . . . . . . 18  |-  ( E. v  v  e.  ( x  \  ran  g
)  ->  ( z  e.  y  ->  ran  (
( x  \  ran  g )  X.  {
z } )  C_  y ) )
49 notm0 3292 . . . . . . . . . . . . . . . . . . 19  |-  ( -. 
E. v  v  e.  ( x  \  ran  g )  <->  ( x  \  ran  g )  =  (/) )
50 xpeq1 4424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  \  ran  g
)  =  (/)  ->  (
( x  \  ran  g )  X.  {
z } )  =  ( (/)  X.  { z } ) )
51 0xp 4485 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (/)  X. 
{ z } )  =  (/)
5250, 51syl6eq 2133 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  \  ran  g
)  =  (/)  ->  (
( x  \  ran  g )  X.  {
z } )  =  (/) )
5352rneqd 4631 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  \  ran  g
)  =  (/)  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  =  ran  (/) )
54 rn0 4656 . . . . . . . . . . . . . . . . . . . . . 22  |-  ran  (/)  =  (/)
5553, 54syl6eq 2133 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  \  ran  g
)  =  (/)  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  =  (/) )
56 0ss 3309 . . . . . . . . . . . . . . . . . . . . 21  |-  (/)  C_  y
5755, 56syl6eqss 3065 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  \  ran  g
)  =  (/)  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  C_  y )
5857a1d 22 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  \  ran  g
)  =  (/)  ->  (
z  e.  y  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  C_  y ) )
5949, 58sylbi 119 . . . . . . . . . . . . . . . . . 18  |-  ( -. 
E. v  v  e.  ( x  \  ran  g )  ->  (
z  e.  y  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  C_  y ) )
6048, 59jaoi 669 . . . . . . . . . . . . . . . . 17  |-  ( ( E. v  v  e.  ( x  \  ran  g )  \/  -.  E. v  v  e.  ( x  \  ran  g
) )  ->  (
z  e.  y  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  C_  y ) )
6142, 60syl 14 . . . . . . . . . . . . . . . 16  |-  (EXMID  ->  (
z  e.  y  ->  ran  ( ( x  \  ran  g )  X.  {
z } )  C_  y ) )
6261imp 122 . . . . . . . . . . . . . . 15  |-  ( (EXMID  /\  z  e.  y )  ->  ran  ( (
x  \  ran  g )  X.  { z } )  C_  y )
63 ssequn2 3162 . . . . . . . . . . . . . . 15  |-  ( ran  ( ( x  \  ran  g )  X.  {
z } )  C_  y 
<->  ( y  u.  ran  ( ( x  \  ran  g )  X.  {
z } ) )  =  y )
6462, 63sylib 120 . . . . . . . . . . . . . 14  |-  ( (EXMID  /\  z  e.  y )  ->  ( y  u. 
ran  ( ( x 
\  ran  g )  X.  { z } ) )  =  y )
6539, 64sylan9eqr 2139 . . . . . . . . . . . . 13  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  -> 
( ran  `' g  u.  ran  ( ( x 
\  ran  g )  X.  { z } ) )  =  y )
6635, 65syl5eq 2129 . . . . . . . . . . . 12  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  ->  ran  ( `' g  u.  ( ( x  \  ran  g )  X.  {
z } ) )  =  y )
67 df-fo 4984 . . . . . . . . . . . 12  |-  ( ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) ) : x -onto-> y  <->  ( ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) )  Fn  x  /\  ran  ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) )  =  y ) )
6834, 66, 67sylanbrc 408 . . . . . . . . . . 11  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  -> 
( `' g  u.  ( ( x  \  ran  g )  X.  {
z } ) ) : x -onto-> y )
69 vex 2618 . . . . . . . . . . . . . 14  |-  g  e. 
_V
7069cnvex 4932 . . . . . . . . . . . . 13  |-  `' g  e.  _V
71 vex 2618 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
72 difexg 3954 . . . . . . . . . . . . . . 15  |-  ( x  e.  _V  ->  (
x  \  ran  g )  e.  _V )
7371, 72ax-mp 7 . . . . . . . . . . . . . 14  |-  ( x 
\  ran  g )  e.  _V
745snex 3993 . . . . . . . . . . . . . 14  |-  { z }  e.  _V
7573, 74xpex 4520 . . . . . . . . . . . . 13  |-  ( ( x  \  ran  g
)  X.  { z } )  e.  _V
7670, 75unex 4239 . . . . . . . . . . . 12  |-  ( `' g  u.  ( ( x  \  ran  g
)  X.  { z } ) )  e. 
_V
77 foeq1 5186 . . . . . . . . . . . 12  |-  ( f  =  ( `' g  u.  ( ( x 
\  ran  g )  X.  { z } ) )  ->  ( f : x -onto-> y  <->  ( `' g  u.  ( (
x  \  ran  g )  X.  { z } ) ) : x
-onto-> y ) )
7876, 77spcev 2706 . . . . . . . . . . 11  |-  ( ( `' g  u.  (
( x  \  ran  g )  X.  {
z } ) ) : x -onto-> y  ->  E. f  f :
x -onto-> y )
7968, 78syl 14 . . . . . . . . . 10  |-  ( ( (EXMID 
/\  z  e.  y )  /\  g : y -1-1-> x )  ->  E. f  f :
x -onto-> y )
8079an32s 533 . . . . . . . . 9  |-  ( ( (EXMID 
/\  g : y
-1-1-> x )  /\  z  e.  y )  ->  E. f 
f : x -onto-> y )
8180ex 113 . . . . . . . 8  |-  ( (EXMID  /\  g : y -1-1-> x
)  ->  ( z  e.  y  ->  E. f 
f : x -onto-> y ) )
8281exlimdv 1744 . . . . . . 7  |-  ( (EXMID  /\  g : y -1-1-> x
)  ->  ( E. z  z  e.  y  ->  E. f  f : x -onto-> y ) )
8382imp 122 . . . . . 6  |-  ( ( (EXMID 
/\  g : y
-1-1-> x )  /\  E. z  z  e.  y
)  ->  E. f 
f : x -onto-> y )
8483an32s 533 . . . . 5  |-  ( ( (EXMID 
/\  E. z  z  e.  y )  /\  g : y -1-1-> x )  ->  E. f  f : x -onto-> y )
8584adantlrr 467 . . . 4  |-  ( ( (EXMID 
/\  ( E. z 
z  e.  y  /\  y  ~<_  x ) )  /\  g : y
-1-1-> x )  ->  E. f 
f : x -onto-> y )
862, 85exlimddv 1823 . . 3  |-  ( (EXMID  /\  ( E. z  z  e.  y  /\  y  ~<_  x ) )  ->  E. f  f :
x -onto-> y )
8786ex 113 . 2  |-  (EXMID  ->  (
( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y ) )
8887alrimivv 1800 1  |-  (EXMID  ->  A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    \/ wo 662  DECID wdc 778   A.wal 1285    = wceq 1287   E.wex 1424    e. wcel 1436   A.wral 2355   _Vcvv 2615    \ cdif 2985    u. cun 2986    i^i cin 2987    C_ wss 2988   (/)c0 3275   {csn 3431   class class class wbr 3820  EXMIDwem 4002    X. cxp 4408   `'ccnv 4409   dom cdm 4410   ran crn 4411   Fun wfun 4972    Fn wfn 4973   -->wf 4974   -1-1->wf1 4975   -onto->wfo 4976    ~<_ cdom 6402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3931  ax-nul 3939  ax-pow 3983  ax-pr 4009  ax-un 4233
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-br 3821  df-opab 3875  df-mpt 3876  df-exmid 4003  df-id 4093  df-xp 4416  df-rel 4417  df-cnv 4418  df-co 4419  df-dm 4420  df-rn 4421  df-fun 4980  df-fn 4981  df-f 4982  df-f1 4983  df-fo 4984  df-dom 6405
This theorem is referenced by:  exmidfodomr  6767
  Copyright terms: Public domain W3C validator