Theorem exmidfodomrlemrALT 7555

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 7554. In particular, this proof uses eldju 7408 instead of djur 7409 and avoids djulclb 7395. (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.

Step	Hyp	Ref	Expression
1		nfv 1581	. . . . . . . . 9 |- F/ f ( E. z z e. y /\ y ~<_ x )
2		nfe1 1549	. . . . . . . . 9 |- F/ f E. f f : x -onto-> y
3	1, 2	nfim 1625	. . . . . . . 8 |- F/ f ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
4	3	nfal 1629	. . . . . . 7 |- F/ f A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
5	4	nfal 1629	. . . . . 6 |- F/ f A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
6		nfv 1581	. . . . . 6 |- F/ f u C_ { (/) }
7	5, 6	nfan 1618	. . . . 5 |- F/ f ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) /\ u C_ { (/) } )
8		nfv 1581	. . . . 5 |- F/ fDECID (/) e. u
9		simpl 109	. . . . . 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 4325	. . . . . . . . . . . 12 |- { (/) } e. _V
11		ssdomg 7065	. . . . . . . . . . . 12 |- ( { (/) } e. _V -> ( u C_ { (/) } -> u ~<_ { (/) } ) )
12	10, 11	ax-mp 5	. . . . . . . . . . 11 |- ( u C_ { (/) } -> u ~<_ { (/) } )
13		df1o2 6701	. . . . . . . . . . 11 |- 1o = { (/) }
14	12, 13	breqtrrdi 4172	. . . . . . . . . 10 |- ( u C_ { (/) } -> u ~<_ 1o )
15		1onn 6793	. . . . . . . . . . 11 |- 1o e. om
16		domrefg 7053	. . . . . . . . . . 11 |- ( 1o e. om -> 1o ~<_ 1o )
17	15, 16	ax-mp 5	. . . . . . . . . 10 |- 1o ~<_ 1o
18		djudom 7433	. . . . . . . . . 10 |- ( ( u ~<_ 1o /\ 1o ~<_ 1o ) -> ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) )
19	14, 17, 18	sylancl 417	. . . . . . . . 9 |- ( u C_ { (/) } -> ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) )
20		dju1p1e2 7549	. . . . . . . . 9 |- ( 1o ⊔ 1o ) ~~ 2o
21		domentr 7078	. . . . . . . . 9 |- ( ( ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) /\ ( 1o ⊔ 1o ) ~~ 2o ) -> ( u ⊔ 1o ) ~<_ 2o )
22	19, 20, 21	sylancl 417	. . . . . . . 8 |- ( u C_ { (/) } -> ( u ⊔ 1o ) ~<_ 2o )
23	22	adantl 277	. . . . . . 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 6713	. . . . . . . . 9 |- (/) e. 1o
25		djurcl 7392	. . . . . . . . 9 |- ( (/) e. 1o -> (inr ` (/) ) e. ( u ⊔ 1o ) )
26	24, 25	ax-mp 5	. . . . . . . 8 |- (inr ` (/) ) e. ( u ⊔ 1o )
27		elex2 2838	. . . . . . . 8 |- ( (inr ` (/) ) e. ( u ⊔ 1o ) -> E. z z e. ( u ⊔ 1o ) )
28	26, 27	ax-mp 5	. . . . . . 7 |- E. z z e. ( u ⊔ 1o )
29	23, 28	jctil 312	. . . . . 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 2824	. . . . . . . 8 |- u e. _V
31		djuex 7383	. . . . . . . 8 |- ( ( u e. _V /\ 1o e. om ) -> ( u ⊔ 1o ) e. _V )
32	30, 15, 31	mp2an 430	. . . . . . 7 |- ( u ⊔ 1o ) e. _V
33		2onn 6794	. . . . . . . 8 |- 2o e. om
34		breq2 4134	. . . . . . . . . . . 12 |- ( x = 2o -> ( y ~<_ x <-> y ~<_ 2o ) )
35	34	anbi2d 468	. . . . . . . . . . 11 |- ( x = 2o -> ( ( E. z z e. y /\ y ~<_ x ) <-> ( E. z z e. y /\ y ~<_ 2o ) ) )
36		foeq2 5612	. . . . . . . . . . . 12 |- ( x = 2o -> ( f : x -onto-> y <-> f : 2o -onto-> y ) )
37	36	exbidv 1878	. . . . . . . . . . 11 |- ( x = 2o -> ( E. f f : x -onto-> y <-> E. f f : 2o -onto-> y ) )
38	35, 37	imbi12d 234	. . . . . . . . . 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 ) ) )
39	38	albidv 1877	. . . . . . . . 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 ) ) )
40	39	spcgv 2912	. . . . . . . 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 ) ) )
41	33, 40	ax-mp 5	. . . . . . 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 2302	. . . . . . . . . . 11 |- ( y = ( u ⊔ 1o ) -> ( z e. y <-> z e. ( u ⊔ 1o ) ) )
43	42	exbidv 1878	. . . . . . . . . 10 |- ( y = ( u ⊔ 1o ) -> ( E. z z e. y <-> E. z z e. ( u ⊔ 1o ) ) )
44		breq1 4133	. . . . . . . . . 10 |- ( y = ( u ⊔ 1o ) -> ( y ~<_ 2o <-> ( u ⊔ 1o ) ~<_ 2o ) )
45	43, 44	anbi12d 477	. . . . . . . . 9 |- ( y = ( u ⊔ 1o ) -> ( ( E. z z e. y /\ y ~<_ 2o ) <-> ( E. z z e. ( u ⊔ 1o ) /\ ( u ⊔ 1o ) ~<_ 2o ) ) )
46		foeq3 5613	. . . . . . . . . 10 |- ( y = ( u ⊔ 1o ) -> ( f : 2o -onto-> y <-> f : 2o -onto-> ( u ⊔ 1o ) ) )
47	46	exbidv 1878	. . . . . . . . 9 |- ( y = ( u ⊔ 1o ) -> ( E. f f : 2o -onto-> y <-> E. f f : 2o -onto-> ( u ⊔ 1o ) ) )
48	45, 47	imbi12d 234	. . . . . . . 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 ) ) ) )
49	48	spcgv 2912	. . . . . . 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 ) ) ) )
50	32, 41, 49	mpsyl 65	. . . . . 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 ) ) )
51	9, 29, 50	sylc 62	. . . . 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 535	. . . . . . . 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 )
53	52	orcd 745	. . . . . . 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 847	. . . . . . 7 |- (DECID (/) e. u <-> ( (/) e. u \/ -. (/) e. u ) )
55	53, 54	sylibr 134	. . . . . 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 535	. . . . . . . . 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 )
57	56	orcd 745	. . . . . . . 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 ) )
58	57, 54	sylibr 134	. . . . . . 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 548	. . . . . . . . . . . 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 7391	. . . . . . . . . . . . 13 |- ( (/) e. u -> (inl ` (/) ) e. ( u ⊔ 1o ) )
61	60	adantl 277	. . . . . . . . . . . 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 5958	. . . . . . . . . . . 12 |- ( ( f : 2o -onto-> ( u ⊔ 1o ) /\ (inl ` (/) ) e. ( u ⊔ 1o ) ) -> E. w e. 2o (inl ` (/) ) = ( f ` w ) )
63	59, 61, 62	syl2anc 415	. . . . . . . . . . 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 537	. . . . . . . . . . . . . . 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 5719	. . . . . . . . . . . . . . . . 17 |- ( (/) e. u -> ( (inl |` u ) ` (/) ) = (inl ` (/) ) )
66	65	eqeq1d 2247	. . . . . . . . . . . . . . . 16 |- ( (/) e. u -> ( ( (inl |` u ) ` (/) ) = ( f ` w ) <-> (inl ` (/) ) = ( f ` w ) ) )
67	66	ad2antlr 493	. . . . . . . . . . . . . . 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 ) ) )
68	64, 67	mpbird 167	. . . . . . . . . . . . . 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 ) )
69	68	adantr 276	. . . . . . . . . . . . 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 110	. . . . . . . . . . . . . 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 = (/) )
71	70	fveq2d 5699	. . . . . . . . . . . . 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 550	. . . . . . . . . . . . 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 ) ` (/) ) )
73	69, 71, 72	3eqtrd 2275	. . . . . . . . . . . 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 ) ` (/) ) )
74	68	adantr 276	. . . . . . . . . . . . 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 110	. . . . . . . . . . . . . 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 )
76	75	fveq2d 5699	. . . . . . . . . . . . 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 548	. . . . . . . . . . . . 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 ) ` (/) ) )
78	74, 76, 77	3eqtrd 2275	. . . . . . . . . . . 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 3732	. . . . . . . . . . . . . 14 |- ( w e. { (/) , 1o } -> ( w = (/) \/ w = 1o ) )
80		df2o3 6702	. . . . . . . . . . . . . 14 |- 2o = { (/) , 1o }
81	79, 80	eleq2s 2333	. . . . . . . . . . . . 13 |- ( w e. 2o -> ( w = (/) \/ w = 1o ) )
82	81	ad2antrl 494	. . . . . . . . . . . 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 ) )
83	73, 78, 82	mpjaodan 810	. . . . . . . . . . 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 ) ` (/) ) )
84	63, 83	rexlimddv 2673	. . . . . . . . . 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 4260	. . . . . . . . . . . . . 14 |- (/) e. _V
86		djune 7418	. . . . . . . . . . . . . 14 |- ( ( (/) e. _V /\ (/) e. _V ) -> (inl ` (/) ) =/= (inr ` (/) ) )
87	85, 85, 86	mp2an 430	. . . . . . . . . . . . 13 |- (inl ` (/) ) =/= (inr ` (/) )
88	87	neii 2422	. . . . . . . . . . . 12 |- -. (inl ` (/) ) = (inr ` (/) )
89		fvres 5719	. . . . . . . . . . . . . . 15 |- ( (/) e. 1o -> ( (inr |` 1o ) ` (/) ) = (inr ` (/) ) )
90	24, 89	ax-mp 5	. . . . . . . . . . . . . 14 |- ( (inr |` 1o ) ` (/) ) = (inr ` (/) )
91	90	a1i 9	. . . . . . . . . . . . 13 |- ( (/) e. u -> ( (inr |` 1o ) ` (/) ) = (inr ` (/) ) )
92	65, 91	eqeq12d 2253	. . . . . . . . . . . 12 |- ( (/) e. u -> ( ( (inl |` u ) ` (/) ) = ( (inr |` 1o ) ` (/) ) <-> (inl ` (/) ) = (inr ` (/) ) ) )
93	88, 92	mtbiri 686	. . . . . . . . . . 11 |- ( (/) e. u -> -. ( (inl |` u ) ` (/) ) = ( (inr |` 1o ) ` (/) ) )
94	93	adantl 277	. . . . . . . . . 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 ) ` (/) ) )
95	84, 94	pm2.65da 671	. . . . . . . . 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 )
96	95	olcd 746	. . . . . . . 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 ) )
97	96, 54	sylibr 134	. . . . . . 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 533	. . . . . . . . . 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_ { (/) } )
99	98, 13	sseqtrrdi 3297	. . . . . . . . 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 )
100	99	adantr 276	. . . . . . . 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 5615	. . . . . . . . . . 11 |- ( f : 2o -onto-> ( u ⊔ 1o ) -> f : 2o --> ( u ⊔ 1o ) )
102	101	adantl 277	. . . . . . . . . 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 ) )
103	102	adantr 276	. . . . . . . . 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 6695	. . . . . . . . . . . 12 |- 1o e. _V
105	104	prid2 3818	. . . . . . . . . . 11 |- 1o e. { (/) , 1o }
106	105, 80	eleqtrri 2314	. . . . . . . . . 10 |- 1o e. 2o
107	106	a1i 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 )
108	103, 107	ffvelcdmd 5844	. . . . . . . 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 ) )
109	100, 108	exmidfodomrlemreseldju 7552	. . . . . . 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 ) ` (/) ) ) )
110	58, 97, 109	mpjaodan 810	. . . . . 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 4554	. . . . . . . . . . 11 |- ( (/) e. 1o -> (/) e. suc 1o )
112	24, 111	ax-mp 5	. . . . . . . . . 10 |- (/) e. suc 1o
113		df-2o 6688	. . . . . . . . . 10 |- 2o = suc 1o
114	112, 113	eleqtrri 2314	. . . . . . . . 9 |- (/) e. 2o
115	114	a1i 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 )
116	102, 115	ffvelcdmd 5844	. . . . . . 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 ) )
117	99, 116	exmidfodomrlemreseldju 7552	. . . . . 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 ) ` (/) ) ) )
118	55, 110, 117	mpjaodan 810	. . . . 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 )
119	7, 8, 51, 118	exlimdd 1925	. . . 4 |- ( ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) /\ u C_ { (/) } ) -> DECID (/) e. u )
120	119	ex 115	. . 3 |- ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) -> ( u C_ { (/) } -> DECID (/) e. u ) )
121	120	alrimiv 1927	. 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 4332	. 2 |- (EXMID <-> A. u ( u C_ { (/) } -> DECID (/) e. u ) )
123	121, 122	sylibr 134	1 |- ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) -> EXMID )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720  DECID wdc 846   A.wal 1400   = wceq 1402   E.wex 1545   e. wcel 2209   =/= wne 2420   E.wrex 2529   _Vcvv 2821   C_ wss 3220   (/)c0 3520   {csn 3709   {cpr 3710   class class class wbr 4130  EXMIDwem 4331   suc csuc 4510   omcom 4737   |` cres 4776   -->wf 5373   -onto->wfo 5375   ` cfv 5377   1oc1o 6680   2oc2o 6681   ~~ cen 7020   ~<_ cdom 7021   ⊔ cdju 7377  inlcinl 7385  inrcinr 7386

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735

This proof depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-exmid 4332  df-id 4438  df-iord 4511  df-on 4513  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-1st 6374  df-2nd 6375  df-1o 6687  df-2o 6688  df-er 6807  df-en 7023  df-dom 7024  df-dju 7378  df-inl 7387  df-inr 7388  df-case 7424

This theorem is used by: (None)