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

Theorem exmidfodomrlemrALT 6776
Description: The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 6775. In particular, this proof uses eldju 6706 instead of djur 6704 and avoids djulclb 6694. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
Assertion
Ref Expression
exmidfodomrlemrALT  |-  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  -> EXMID )
Distinct variable group:    x, f, y, z

Proof of Theorem exmidfodomrlemrALT
Dummy variables  u  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1464 . . . . . . . . 9  |-  F/ f ( E. z  z  e.  y  /\  y  ~<_  x )
2 nfe1 1428 . . . . . . . . 9  |-  F/ f E. f  f : x -onto-> y
31, 2nfim 1507 . . . . . . . 8  |-  F/ f ( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )
43nfal 1511 . . . . . . 7  |-  F/ f A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )
54nfal 1511 . . . . . 6  |-  F/ f A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )
6 nfv 1464 . . . . . 6  |-  F/ f  u  C_  { (/) }
75, 6nfan 1500 . . . . 5  |-  F/ f ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )
8 nfv 1464 . . . . 5  |-  F/ fDECID  (/)  e.  u
9 simpl 107 . . . . . 6  |-  ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  ->  A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y ) )
10 p0ex 3999 . . . . . . . . . . . 12  |-  { (/) }  e.  _V
11 ssdomg 6449 . . . . . . . . . . . 12  |-  ( {
(/) }  e.  _V  ->  ( u  C_  { (/) }  ->  u  ~<_  { (/) } ) )
1210, 11ax-mp 7 . . . . . . . . . . 11  |-  ( u 
C_  { (/) }  ->  u  ~<_  { (/) } )
13 df1o2 6150 . . . . . . . . . . 11  |-  1o  =  { (/) }
1412, 13syl6breqr 3862 . . . . . . . . . 10  |-  ( u 
C_  { (/) }  ->  u  ~<_  1o )
15 1onn 6233 . . . . . . . . . . 11  |-  1o  e.  om
16 domrefg 6438 . . . . . . . . . . 11  |-  ( 1o  e.  om  ->  1o  ~<_  1o )
1715, 16ax-mp 7 . . . . . . . . . 10  |-  1o  ~<_  1o
18 djudom 6734 . . . . . . . . . 10  |-  ( ( u  ~<_  1o  /\  1o  ~<_  1o )  ->  ( u 1o )  ~<_  ( 1o 1o ) )
1914, 17, 18sylancl 404 . . . . . . . . 9  |-  ( u 
C_  { (/) }  ->  ( u 1o )  ~<_  ( 1o 1o ) )
20 dju1p1e2 6770 . . . . . . . . 9  |-  ( 1o 1o )  ~~  2o
21 domentr 6462 . . . . . . . . 9  |-  ( ( ( u 1o )  ~<_  ( 1o 1o )  /\  ( 1o 1o )  ~~  2o )  ->  ( u 1o )  ~<_  2o )
2219, 20, 21sylancl 404 . . . . . . . 8  |-  ( u 
C_  { (/) }  ->  ( u 1o )  ~<_  2o )
2322adantl 271 . . . . . . 7  |-  ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  ->  ( u 1o )  ~<_  2o )
24 0lt1o 6160 . . . . . . . . 9  |-  (/)  e.  1o
25 djurcl 6691 . . . . . . . . 9  |-  ( (/)  e.  1o  ->  (inr `  (/) )  e.  ( u 1o )
)
2624, 25ax-mp 7 . . . . . . . 8  |-  (inr `  (/) )  e.  ( u 1o )
27 elex2 2629 . . . . . . . 8  |-  ( (inr
`  (/) )  e.  ( u 1o )  ->  E. z 
z  e.  ( u 1o ) )
2826, 27ax-mp 7 . . . . . . 7  |-  E. z 
z  e.  ( u 1o )
2923, 28jctil 305 . . . . . 6  |-  ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  ->  ( E. z 
z  e.  ( u 1o )  /\  (
u 1o )  ~<_  2o ) )
30 vex 2618 . . . . . . . 8  |-  u  e. 
_V
31 djuex 6683 . . . . . . . 8  |-  ( ( u  e.  _V  /\  1o  e.  om )  -> 
( u 1o )  e.  _V )
3230, 15, 31mp2an 417 . . . . . . 7  |-  ( u 1o )  e.  _V
33 2onn 6234 . . . . . . . 8  |-  2o  e.  om
34 breq2 3826 . . . . . . . . . . . 12  |-  ( x  =  2o  ->  (
y  ~<_  x  <->  y  ~<_  2o ) )
3534anbi2d 452 . . . . . . . . . . 11  |-  ( x  =  2o  ->  (
( E. z  z  e.  y  /\  y  ~<_  x )  <->  ( E. z  z  e.  y  /\  y  ~<_  2o )
) )
36 foeq2 5195 . . . . . . . . . . . 12  |-  ( x  =  2o  ->  (
f : x -onto-> y  <-> 
f : 2o -onto-> y
) )
3736exbidv 1750 . . . . . . . . . . 11  |-  ( x  =  2o  ->  ( E. f  f :
x -onto-> y  <->  E. f 
f : 2o -onto-> y
) )
3835, 37imbi12d 232 . . . . . . . . . 10  |-  ( x  =  2o  ->  (
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  <->  ( ( E. z  z  e.  y  /\  y  ~<_  2o )  ->  E. f  f : 2o -onto-> y ) ) )
3938albidv 1749 . . . . . . . . 9  |-  ( x  =  2o  ->  ( A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  <->  A. y
( ( E. z 
z  e.  y  /\  y  ~<_  2o )  ->  E. f  f : 2o -onto-> y ) ) )
4039spcgv 2699 . . . . . . . 8  |-  ( 2o  e.  om  ->  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  ->  A. y
( ( E. z 
z  e.  y  /\  y  ~<_  2o )  ->  E. f  f : 2o -onto-> y ) ) )
4133, 40ax-mp 7 . . . . . . 7  |-  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  ->  A. y
( ( E. z 
z  e.  y  /\  y  ~<_  2o )  ->  E. f  f : 2o -onto-> y ) )
42 eleq2 2148 . . . . . . . . . . 11  |-  ( y  =  ( u 1o )  ->  ( z  e.  y  <->  z  e.  ( u 1o ) ) )
4342exbidv 1750 . . . . . . . . . 10  |-  ( y  =  ( u 1o )  ->  ( E. z 
z  e.  y  <->  E. z 
z  e.  ( u 1o ) ) )
44 breq1 3825 . . . . . . . . . 10  |-  ( y  =  ( u 1o )  ->  ( y  ~<_  2o  <->  ( u 1o )  ~<_  2o ) )
4543, 44anbi12d 457 . . . . . . . . 9  |-  ( y  =  ( u 1o )  ->  ( ( E. z  z  e.  y  /\  y  ~<_  2o )  <-> 
( E. z  z  e.  ( u 1o )  /\  ( u 1o )  ~<_  2o ) ) )
46 foeq3 5196 . . . . . . . . . 10  |-  ( y  =  ( u 1o )  ->  ( f : 2o -onto-> y  <->  f : 2o -onto-> ( u 1o ) ) )
4746exbidv 1750 . . . . . . . . 9  |-  ( y  =  ( u 1o )  ->  ( E. f 
f : 2o -onto-> y  <->  E. f  f : 2o -onto->
( u 1o )
) )
4845, 47imbi12d 232 . . . . . . . 8  |-  ( y  =  ( u 1o )  ->  ( ( ( E. z  z  e.  y  /\  y  ~<_  2o )  ->  E. f 
f : 2o -onto-> y
)  <->  ( ( E. z  z  e.  ( u 1o )  /\  (
u 1o )  ~<_  2o )  ->  E. f  f : 2o -onto-> ( u 1o ) ) ) )
4948spcgv 2699 . . . . . . 7  |-  ( ( u 1o )  e.  _V  ->  ( A. y ( ( E. z  z  e.  y  /\  y  ~<_  2o )  ->  E. f 
f : 2o -onto-> y
)  ->  ( ( E. z  z  e.  ( u 1o )  /\  ( u 1o )  ~<_  2o )  ->  E. f 
f : 2o -onto-> (
u 1o ) ) ) )
5032, 41, 49mpsyl 64 . . . . . 6  |-  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  ->  ( ( E. z  z  e.  ( u 1o )  /\  ( u 1o )  ~<_  2o )  ->  E. f 
f : 2o -onto-> (
u 1o ) ) )
519, 29, 50sylc 61 . . . . 5  |-  ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  ->  E. f  f : 2o -onto-> ( u 1o ) )
52 simprl 498 . . . . . . . 8  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( (/)  e.  u  /\  ( f `  (/) )  =  ( (inl  |`  u
) `  (/) ) ) )  ->  (/)  e.  u
)
5352orcd 685 . . . . . . 7  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( (/)  e.  u  /\  ( f `  (/) )  =  ( (inl  |`  u
) `  (/) ) ) )  ->  ( (/)  e.  u  \/  -.  (/)  e.  u ) )
54 df-dc 779 . . . . . . 7  |-  (DECID  (/)  e.  u  <->  (
(/)  e.  u  \/  -.  (/)  e.  u ) )
5553, 54sylibr 132 . . . . . 6  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( (/)  e.  u  /\  ( f `  (/) )  =  ( (inl  |`  u
) `  (/) ) ) )  -> DECID  (/)  e.  u )
56 simprl 498 . . . . . . . . 9  |-  ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  /\  u  C_  {
(/) } )  /\  f : 2o -onto-> ( u 1o ) )  /\  (
f `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  ( (/)  e.  u  /\  ( f `  1o )  =  ( (inl  |`  u ) `  (/) ) ) )  ->  (/)  e.  u
)
5756orcd 685 . . . . . . . 8  |-  ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  /\  u  C_  {
(/) } )  /\  f : 2o -onto-> ( u 1o ) )  /\  (
f `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  ( (/)  e.  u  /\  ( f `  1o )  =  ( (inl  |`  u ) `  (/) ) ) )  ->  ( (/)  e.  u  \/  -.  (/)  e.  u ) )
5857, 54sylibr 132 . . . . . . 7  |-  ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  /\  u  C_  {
(/) } )  /\  f : 2o -onto-> ( u 1o ) )  /\  (
f `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  ( (/)  e.  u  /\  ( f `  1o )  =  ( (inl  |`  u ) `  (/) ) ) )  -> DECID  (/)  e.  u )
59 simp-4r 509 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  -> 
f : 2o -onto-> (
u 1o ) )
60 djulcl 6690 . . . . . . . . . . . . 13  |-  ( (/)  e.  u  ->  (inl `  (/) )  e.  ( u 1o ) )
6160adantl 271 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  -> 
(inl `  (/) )  e.  ( u 1o )
)
62 foelrn 5494 . . . . . . . . . . . 12  |-  ( ( f : 2o -onto-> (
u 1o )  /\  (inl `  (/) )  e.  (
u 1o ) )  ->  E. w  e.  2o  (inl `  (/) )  =  ( f `  w ) )
6359, 61, 62syl2anc 403 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  ->  E. w  e.  2o  (inl `  (/) )  =  ( f `  w ) )
64 simprr 499 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  -> 
(inl `  (/) )  =  ( f `  w
) )
65 fvres 5294 . . . . . . . . . . . . . . . . 17  |-  ( (/)  e.  u  ->  ( (inl  |`  u ) `  (/) )  =  (inl `  (/) ) )
6665eqeq1d 2093 . . . . . . . . . . . . . . . 16  |-  ( (/)  e.  u  ->  ( ( (inl  |`  u ) `  (/) )  =  ( f `
 w )  <->  (inl `  (/) )  =  ( f `  w
) ) )
6766ad2antlr 473 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  -> 
( ( (inl  |`  u
) `  (/) )  =  ( f `  w
)  <->  (inl `  (/) )  =  ( f `  w
) ) )
6864, 67mpbird 165 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  -> 
( (inl  |`  u
) `  (/) )  =  ( f `  w
) )
6968adantr 270 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  (/) )  -> 
( (inl  |`  u
) `  (/) )  =  ( f `  w
) )
70 simpr 108 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  (/) )  ->  w  =  (/) )
7170fveq2d 5274 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  (/) )  -> 
( f `  w
)  =  ( f `
 (/) ) )
72 simp-5r 511 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  (/) )  -> 
( f `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )
7369, 71, 723eqtrd 2121 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  (/) )  -> 
( (inl  |`  u
) `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )
7468adantr 270 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  1o )  ->  ( (inl  |`  u
) `  (/) )  =  ( f `  w
) )
75 simpr 108 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  1o )  ->  w  =  1o )
7675fveq2d 5274 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  1o )  ->  ( f `  w
)  =  ( f `
 1o ) )
77 simp-4r 509 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  1o )  ->  ( f `  1o )  =  ( (inr  |`  1o ) `  (/) ) )
7874, 76, 773eqtrd 2121 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  /\  w  =  1o )  ->  ( (inl  |`  u
) `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )
79 elpri 3454 . . . . . . . . . . . . . 14  |-  ( w  e.  { (/) ,  1o }  ->  ( w  =  (/)  \/  w  =  1o ) )
80 df2o3 6151 . . . . . . . . . . . . . 14  |-  2o  =  { (/) ,  1o }
8179, 80eleq2s 2179 . . . . . . . . . . . . 13  |-  ( w  e.  2o  ->  (
w  =  (/)  \/  w  =  1o ) )
8281ad2antrl 474 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  -> 
( w  =  (/)  \/  w  =  1o ) )
8373, 78, 82mpjaodan 745 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  /\  ( w  e.  2o  /\  (inl `  (/) )  =  ( f `  w
) ) )  -> 
( (inl  |`  u
) `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )
8463, 83rexlimddv 2489 . . . . . . . . . 10  |-  ( ( ( ( ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  -> 
( (inl  |`  u
) `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )
85 0ex 3943 . . . . . . . . . . . . . 14  |-  (/)  e.  _V
86 djune 6716 . . . . . . . . . . . . . 14  |-  ( (
(/)  e.  _V  /\  (/)  e.  _V )  ->  (inl `  (/) )  =/=  (inr `  (/) ) )
8785, 85, 86mp2an 417 . . . . . . . . . . . . 13  |-  (inl `  (/) )  =/=  (inr `  (/) )
8887neii 2253 . . . . . . . . . . . 12  |-  -.  (inl `  (/) )  =  (inr `  (/) )
89 fvres 5294 . . . . . . . . . . . . . . 15  |-  ( (/)  e.  1o  ->  ( (inr  |`  1o ) `  (/) )  =  (inr `  (/) ) )
9024, 89ax-mp 7 . . . . . . . . . . . . . 14  |-  ( (inr  |`  1o ) `  (/) )  =  (inr `  (/) )
9190a1i 9 . . . . . . . . . . . . 13  |-  ( (/)  e.  u  ->  ( (inr  |`  1o ) `  (/) )  =  (inr `  (/) ) )
9265, 91eqeq12d 2099 . . . . . . . . . . . 12  |-  ( (/)  e.  u  ->  ( ( (inl  |`  u ) `  (/) )  =  ( (inr  |`  1o ) `  (/) )  <->  (inl `  (/) )  =  (inr `  (/) ) ) )
9388, 92mtbiri 633 . . . . . . . . . . 11  |-  ( (/)  e.  u  ->  -.  (
(inl  |`  u ) `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )
9493adantl 271 . . . . . . . . . 10  |-  ( ( ( ( ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  /\  (
f `  1o )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  (/) 
e.  u )  ->  -.  ( (inl  |`  u
) `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )
9584, 94pm2.65da 620 . . . . . . . . 9  |-  ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  /\  u  C_  {
(/) } )  /\  f : 2o -onto-> ( u 1o ) )  /\  (
f `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  ( f `  1o )  =  ( (inr  |`  1o ) `  (/) ) )  ->  -.  (/)  e.  u
)
9695olcd 686 . . . . . . . 8  |-  ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  /\  u  C_  {
(/) } )  /\  f : 2o -onto-> ( u 1o ) )  /\  (
f `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  ( f `  1o )  =  ( (inr  |`  1o ) `  (/) ) )  ->  ( (/)  e.  u  \/  -.  (/)  e.  u ) )
9796, 54sylibr 132 . . . . . . 7  |-  ( ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  /\  u  C_  {
(/) } )  /\  f : 2o -onto-> ( u 1o ) )  /\  (
f `  (/) )  =  ( (inr  |`  1o ) `
 (/) ) )  /\  ( f `  1o )  =  ( (inr  |`  1o ) `  (/) ) )  -> DECID  (/) 
e.  u )
98 simplr 497 . . . . . . . . . 10  |-  ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  ->  u  C_  { (/) } )
9998, 13syl6sseqr 3062 . . . . . . . . 9  |-  ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  ->  u  C_  1o )
10099adantr 270 . . . . . . . 8  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  ->  u  C_  1o )
101 fof 5198 . . . . . . . . . . 11  |-  ( f : 2o -onto-> ( u 1o )  ->  f : 2o --> ( u 1o ) )
102101adantl 271 . . . . . . . . . 10  |-  ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  ->  f : 2o
--> ( u 1o )
)
103102adantr 270 . . . . . . . . 9  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  ->  f : 2o --> ( u 1o ) )
104 1oex 6145 . . . . . . . . . . . 12  |-  1o  e.  _V
105104prid2 3534 . . . . . . . . . . 11  |-  1o  e.  {
(/) ,  1o }
106105, 80eleqtrri 2160 . . . . . . . . . 10  |-  1o  e.  2o
107106a1i 9 . . . . . . . . 9  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  ->  1o  e.  2o )
108103, 107ffvelrnd 5400 . . . . . . . 8  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  ->  (
f `  1o )  e.  ( u 1o )
)
109100, 108exmidfodomrlemreseldju 6773 . . . . . . 7  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  ->  (
( (/)  e.  u  /\  ( f `  1o )  =  ( (inl  |`  u ) `  (/) ) )  \/  ( f `  1o )  =  (
(inr  |`  1o ) `  (/) ) ) )
11058, 97, 109mpjaodan 745 . . . . . 6  |-  ( ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  /\  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) )  -> DECID  (/)  e.  u )
111 elelsuc 4212 . . . . . . . . . . 11  |-  ( (/)  e.  1o  ->  (/)  e.  suc  1o )
11224, 111ax-mp 7 . . . . . . . . . 10  |-  (/)  e.  suc  1o
113 df-2o 6138 . . . . . . . . . 10  |-  2o  =  suc  1o
114112, 113eleqtrri 2160 . . . . . . . . 9  |-  (/)  e.  2o
115114a1i 9 . . . . . . . 8  |-  ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  ->  (/)  e.  2o )
116102, 115ffvelrnd 5400 . . . . . . 7  |-  ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  ->  ( f `  (/) )  e.  ( u 1o ) )
11799, 116exmidfodomrlemreseldju 6773 . . . . . 6  |-  ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  ->  ( ( (/) 
e.  u  /\  (
f `  (/) )  =  ( (inl  |`  u
) `  (/) ) )  \/  ( f `  (/) )  =  ( (inr  |`  1o ) `  (/) ) ) )
11855, 110, 117mpjaodan 745 . . . . 5  |-  ( ( ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f  f : x -onto-> y )  /\  u  C_  { (/) } )  /\  f : 2o -onto->
( u 1o )
)  -> DECID  (/)  e.  u )
1197, 8, 51, 118exlimdd 1797 . . . 4  |-  ( ( A. x A. y
( ( E. z 
z  e.  y  /\  y  ~<_  x )  ->  E. f  f :
x -onto-> y )  /\  u  C_  { (/) } )  -> DECID  (/) 
e.  u )
120119ex 113 . . 3  |-  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  ->  ( u  C_ 
{ (/) }  -> DECID  (/)  e.  u ) )
121120alrimiv 1799 . 2  |-  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  ->  A. u
( u  C_  { (/) }  -> DECID  (/) 
e.  u ) )
122 df-exmid 4006 . 2  |-  (EXMID  <->  A. u
( u  C_  { (/) }  -> DECID  (/) 
e.  u ) )
123121, 122sylibr 132 1  |-  ( A. x A. y ( ( E. z  z  e.  y  /\  y  ~<_  x )  ->  E. f 
f : x -onto-> y )  -> EXMID )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 662  DECID wdc 778   A.wal 1285    = wceq 1287   E.wex 1424    e. wcel 1436    =/= wne 2251   E.wrex 2356   _Vcvv 2615    C_ wss 2988   (/)c0 3275   {csn 3431   {cpr 3432   class class class wbr 3822  EXMIDwem 4005   suc csuc 4168   omcom 4380    |` cres 4415   -->wf 4979   -onto->wfo 4981   ` cfv 4983   1oc1o 6130   2oc2o 6131    ~~ cen 6409    ~<_ cdom 6410   ⊔ cdju 6677  inlcinl 6684  inrcinr 6685
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-coll 3931  ax-sep 3934  ax-nul 3942  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-iinf 4378
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  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-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  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 3639  df-int 3674  df-iun 3717  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-exmid 4006  df-id 4096  df-iord 4169  df-on 4171  df-suc 4174  df-iom 4381  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-1st 5870  df-2nd 5871  df-1o 6137  df-2o 6138  df-er 6246  df-en 6412  df-dom 6413  df-dju 6678  df-inl 6686  df-inr 6687  df-case 6722
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator