Theorem exmidfodomrlemrALT 7311

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 7310. In particular, this proof uses eldju 7170 instead of djur 7171 and avoids djulclb 7157. (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 1551	. . . . . . . . 9 |- F/ f ( E. z z e. y /\ y ~<_ x )
2		nfe1 1519	. . . . . . . . 9 |- F/ f E. f f : x -onto-> y
3	1, 2	nfim 1595	. . . . . . . 8 |- F/ f ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
4	3	nfal 1599	. . . . . . 7 |- F/ f A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
5	4	nfal 1599	. . . . . 6 |- F/ f A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
6		nfv 1551	. . . . . 6 |- F/ f u C_ { (/) }
7	5, 6	nfan 1588	. . . . 5 |- F/ f ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) /\ u C_ { (/) } )
8		nfv 1551	. . . . 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 4232	. . . . . . . . . . . 12 |- { (/) } e. _V
11		ssdomg 6870	. . . . . . . . . . . 12 |- ( { (/) } e. _V -> ( u C_ { (/) } -> u ~<_ { (/) } ) )
12	10, 11	ax-mp 5	. . . . . . . . . . 11 |- ( u C_ { (/) } -> u ~<_ { (/) } )
13		df1o2 6515	. . . . . . . . . . 11 |- 1o = { (/) }
14	12, 13	breqtrrdi 4086	. . . . . . . . . 10 |- ( u C_ { (/) } -> u ~<_ 1o )
15		1onn 6606	. . . . . . . . . . 11 |- 1o e. om
16		domrefg 6858	. . . . . . . . . . 11 |- ( 1o e. om -> 1o ~<_ 1o )
17	15, 16	ax-mp 5	. . . . . . . . . 10 |- 1o ~<_ 1o
18		djudom 7195	. . . . . . . . . 10 |- ( ( u ~<_ 1o /\ 1o ~<_ 1o ) -> ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) )
19	14, 17, 18	sylancl 413	. . . . . . . . 9 |- ( u C_ { (/) } -> ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) )
20		dju1p1e2 7305	. . . . . . . . 9 |- ( 1o ⊔ 1o ) ~~ 2o
21		domentr 6883	. . . . . . . . 9 |- ( ( ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) /\ ( 1o ⊔ 1o ) ~~ 2o ) -> ( u ⊔ 1o ) ~<_ 2o )
22	19, 20, 21	sylancl 413	. . . . . . . 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 6526	. . . . . . . . 9 |- (/) e. 1o
25		djurcl 7154	. . . . . . . . 9 |- ( (/) e. 1o -> (inr ` (/) ) e. ( u ⊔ 1o ) )
26	24, 25	ax-mp 5	. . . . . . . 8 |- (inr ` (/) ) e. ( u ⊔ 1o )
27		elex2 2788	. . . . . . . 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 2775	. . . . . . . 8 |- u e. _V
31		djuex 7145	. . . . . . . 8 |- ( ( u e. _V /\ 1o e. om ) -> ( u ⊔ 1o ) e. _V )
32	30, 15, 31	mp2an 426	. . . . . . 7 |- ( u ⊔ 1o ) e. _V
33		2onn 6607	. . . . . . . 8 |- 2o e. om
34		breq2 4048	. . . . . . . . . . . 12 |- ( x = 2o -> ( y ~<_ x <-> y ~<_ 2o ) )
35	34	anbi2d 464	. . . . . . . . . . 11 |- ( x = 2o -> ( ( E. z z e. y /\ y ~<_ x ) <-> ( E. z z e. y /\ y ~<_ 2o ) ) )
36		foeq2 5495	. . . . . . . . . . . 12 |- ( x = 2o -> ( f : x -onto-> y <-> f : 2o -onto-> y ) )
37	36	exbidv 1848	. . . . . . . . . . 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 1847	. . . . . . . . 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 2860	. . . . . . . 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 2269	. . . . . . . . . . 11 |- ( y = ( u ⊔ 1o ) -> ( z e. y <-> z e. ( u ⊔ 1o ) ) )
43	42	exbidv 1848	. . . . . . . . . 10 |- ( y = ( u ⊔ 1o ) -> ( E. z z e. y <-> E. z z e. ( u ⊔ 1o ) ) )
44		breq1 4047	. . . . . . . . . 10 |- ( y = ( u ⊔ 1o ) -> ( y ~<_ 2o <-> ( u ⊔ 1o ) ~<_ 2o ) )
45	43, 44	anbi12d 473	. . . . . . . . 9 |- ( y = ( u ⊔ 1o ) -> ( ( E. z z e. y /\ y ~<_ 2o ) <-> ( E. z z e. ( u ⊔ 1o ) /\ ( u ⊔ 1o ) ~<_ 2o ) ) )
46		foeq3 5496	. . . . . . . . . 10 |- ( y = ( u ⊔ 1o ) -> ( f : 2o -onto-> y <-> f : 2o -onto-> ( u ⊔ 1o ) ) )
47	46	exbidv 1848	. . . . . . . . 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 2860	. . . . . . 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 529	. . . . . . . 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 735	. . . . . . 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 837	. . . . . . 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 529	. . . . . . . . 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 735	. . . . . . . 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 542	. . . . . . . . . . . 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 7153	. . . . . . . . . . . . 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 5821	. . . . . . . . . . . 12 |- ( ( f : 2o -onto-> ( u ⊔ 1o ) /\ (inl ` (/) ) e. ( u ⊔ 1o ) ) -> E. w e. 2o (inl ` (/) ) = ( f ` w ) )
63	59, 61, 62	syl2anc 411	. . . . . . . . . . 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 531	. . . . . . . . . . . . . . 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 5600	. . . . . . . . . . . . . . . . 17 |- ( (/) e. u -> ( (inl |` u ) ` (/) ) = (inl ` (/) ) )
66	65	eqeq1d 2214	. . . . . . . . . . . . . . . 16 |- ( (/) e. u -> ( ( (inl |` u ) ` (/) ) = ( f ` w ) <-> (inl ` (/) ) = ( f ` w ) ) )
67	66	ad2antlr 489	. . . . . . . . . . . . . . 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 5580	. . . . . . . . . . . . 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 544	. . . . . . . . . . . . 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 2242	. . . . . . . . . . . 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 5580	. . . . . . . . . . . . 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 542	. . . . . . . . . . . . 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 2242	. . . . . . . . . . . 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 3656	. . . . . . . . . . . . . 14 |- ( w e. { (/) , 1o } -> ( w = (/) \/ w = 1o ) )
80		df2o3 6516	. . . . . . . . . . . . . 14 |- 2o = { (/) , 1o }
81	79, 80	eleq2s 2300	. . . . . . . . . . . . 13 |- ( w e. 2o -> ( w = (/) \/ w = 1o ) )
82	81	ad2antrl 490	. . . . . . . . . . . 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 800	. . . . . . . . . . 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 2628	. . . . . . . . . 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 4171	. . . . . . . . . . . . . 14 |- (/) e. _V
86		djune 7180	. . . . . . . . . . . . . 14 |- ( ( (/) e. _V /\ (/) e. _V ) -> (inl ` (/) ) =/= (inr ` (/) ) )
87	85, 85, 86	mp2an 426	. . . . . . . . . . . . 13 |- (inl ` (/) ) =/= (inr ` (/) )
88	87	neii 2378	. . . . . . . . . . . 12 |- -. (inl ` (/) ) = (inr ` (/) )
89		fvres 5600	. . . . . . . . . . . . . . 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 2220	. . . . . . . . . . . 12 |- ( (/) e. u -> ( ( (inl |` u ) ` (/) ) = ( (inr |` 1o ) ` (/) ) <-> (inl ` (/) ) = (inr ` (/) ) ) )
93	88, 92	mtbiri 677	. . . . . . . . . . 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 663	. . . . . . . . 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 736	. . . . . . . 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 528	. . . . . . . . . 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 3242	. . . . . . . . 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 5498	. . . . . . . . . . 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 6510	. . . . . . . . . . . 12 |- 1o e. _V
105	104	prid2 3740	. . . . . . . . . . 11 |- 1o e. { (/) , 1o }
106	105, 80	eleqtrri 2281	. . . . . . . . . 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 5716	. . . . . . . 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 7308	. . . . . . 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 800	. . . . . 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 4456	. . . . . . . . . . 11 |- ( (/) e. 1o -> (/) e. suc 1o )
112	24, 111	ax-mp 5	. . . . . . . . . 10 |- (/) e. suc 1o
113		df-2o 6503	. . . . . . . . . 10 |- 2o = suc 1o
114	112, 113	eleqtrri 2281	. . . . . . . . 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 5716	. . . . . . 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 7308	. . . . . 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 800	. . . . 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 1895	. . . 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 1897	. 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 4239	. 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 )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 710  DECID wdc 836   A.wal 1371   = wceq 1373   E.wex 1515   e. wcel 2176   =/= wne 2376   E.wrex 2485   _Vcvv 2772   C_ wss 3166   (/)c0 3460   {csn 3633   {cpr 3634   class class class wbr 4044  EXMIDwem 4238   suc csuc 4412   omcom 4638   |` cres 4677   -->wf 5267   -onto->wfo 5269   ` cfv 5271   1oc1o 6495   2oc2o 6496   ~~ cen 6825   ~<_ cdom 6826   ⊔ cdju 7139  inlcinl 7147  inrcinr 7148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-coll 4159  ax-sep 4162  ax-nul 4170  ax-pow 4218  ax-pr 4253  ax-un 4480  ax-setind 4585  ax-iinf 4636

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-ral 2489  df-rex 2490  df-reu 2491  df-rab 2493  df-v 2774  df-sbc 2999  df-csb 3094  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3461  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-int 3886  df-iun 3929  df-br 4045  df-opab 4106  df-mpt 4107  df-tr 4143  df-exmid 4239  df-id 4340  df-iord 4413  df-on 4415  df-suc 4418  df-iom 4639  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-res 4687  df-ima 4688  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-1st 6226  df-2nd 6227  df-1o 6502  df-2o 6503  df-er 6620  df-en 6828  df-dom 6829  df-dju 7140  df-inl 7149  df-inr 7150  df-case 7186

This theorem is referenced by: (None)