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.

Step	Hyp	Ref	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
3	1, 2	nfim 1507	. . . . . . . 8 |- F/ f ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
4	3	nfal 1511	. . . . . . 7 |- F/ f A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
5	4	nfal 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_ { (/) }
7	5, 6	nfan 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 ~<_ { (/) } ) )
12	10, 11	ax-mp 7	. . . . . . . . . . 11 |- ( u C_ { (/) } -> u ~<_ { (/) } )
13		df1o2 6150	. . . . . . . . . . 11 |- 1o = { (/) }
14	12, 13	syl6breqr 3862	. . . . . . . . . 10 |- ( u C_ { (/) } -> u ~<_ 1o )
15		1onn 6233	. . . . . . . . . . 11 |- 1o e. om
16		domrefg 6438	. . . . . . . . . . 11 |- ( 1o e. om -> 1o ~<_ 1o )
17	15, 16	ax-mp 7	. . . . . . . . . 10 |- 1o ~<_ 1o
18		djudom 6734	. . . . . . . . . 10 |- ( ( u ~<_ 1o /\ 1o ~<_ 1o ) -> ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) )
19	14, 17, 18	sylancl 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 )
22	19, 20, 21	sylancl 404	. . . . . . . 8 |- ( u C_ { (/) } -> ( u ⊔ 1o ) ~<_ 2o )
23	22	adantl 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 ) )
26	24, 25	ax-mp 7	. . . . . . . 8 |- (inr ` (/) ) e. ( u ⊔ 1o )
27		elex2 2629	. . . . . . . 8 |- ( (inr ` (/) ) e. ( u ⊔ 1o ) -> E. z z e. ( u ⊔ 1o ) )
28	26, 27	ax-mp 7	. . . . . . 7 |- E. z z e. ( u ⊔ 1o )
29	23, 28	jctil 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 )
32	30, 15, 31	mp2an 417	. . . . . . 7 |- ( u ⊔ 1o ) e. _V
33		2onn 6234	. . . . . . . 8 |- 2o e. om
34		breq2 3826	. . . . . . . . . . . 12 |- ( x = 2o -> ( y ~<_ x <-> y ~<_ 2o ) )
35	34	anbi2d 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 ) )
37	36	exbidv 1750	. . . . . . . . . . 11 |- ( x = 2o -> ( E. f f : x -onto-> y <-> E. f f : 2o -onto-> y ) )
38	35, 37	imbi12d 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 ) ) )
39	38	albidv 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 ) ) )
40	39	spcgv 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 ) ) )
41	33, 40	ax-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 ) ) )
43	42	exbidv 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 ) )
45	43, 44	anbi12d 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 ) ) )
47	46	exbidv 1750	. . . . . . . . 9 |- ( y = ( u ⊔ 1o ) -> ( E. f f : 2o -onto-> y <-> E. f f : 2o -onto-> ( u ⊔ 1o ) ) )
48	45, 47	imbi12d 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 ) ) ) )
49	48	spcgv 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 ) ) ) )
50	32, 41, 49	mpsyl 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 ) ) )
51	9, 29, 50	sylc 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 )
53	52	orcd 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 ) )
55	53, 54	sylibr 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 )
57	56	orcd 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 ) )
58	57, 54	sylibr 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 ) )
61	60	adantl 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 ) )
63	59, 61, 62	syl2anc 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 ` (/) ) )
66	65	eqeq1d 2093	. . . . . . . . . . . . . . . 16 |- ( (/) e. u -> ( ( (inl |` u ) ` (/) ) = ( f ` w ) <-> (inl ` (/) ) = ( f ` w ) ) )
67	66	ad2antlr 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 ) ) )
68	64, 67	mpbird 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 ) )
69	68	adantr 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 = (/) )
71	70	fveq2d 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 ) ` (/) ) )
73	69, 71, 72	3eqtrd 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 ) ` (/) ) )
74	68	adantr 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 )
76	75	fveq2d 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 ) ` (/) ) )
78	74, 76, 77	3eqtrd 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 }
81	79, 80	eleq2s 2179	. . . . . . . . . . . . 13 |- ( w e. 2o -> ( w = (/) \/ w = 1o ) )
82	81	ad2antrl 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 ) )
83	73, 78, 82	mpjaodan 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 ) ` (/) ) )
84	63, 83	rexlimddv 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 ` (/) ) )
87	85, 85, 86	mp2an 417	. . . . . . . . . . . . 13 |- (inl ` (/) ) =/= (inr ` (/) )
88	87	neii 2253	. . . . . . . . . . . 12 |- -. (inl ` (/) ) = (inr ` (/) )
89		fvres 5294	. . . . . . . . . . . . . . 15 |- ( (/) e. 1o -> ( (inr |` 1o ) ` (/) ) = (inr ` (/) ) )
90	24, 89	ax-mp 7	. . . . . . . . . . . . . 14 |- ( (inr |` 1o ) ` (/) ) = (inr ` (/) )
91	90	a1i 9	. . . . . . . . . . . . 13 |- ( (/) e. u -> ( (inr |` 1o ) ` (/) ) = (inr ` (/) ) )
92	65, 91	eqeq12d 2099	. . . . . . . . . . . 12 |- ( (/) e. u -> ( ( (inl |` u ) ` (/) ) = ( (inr |` 1o ) ` (/) ) <-> (inl ` (/) ) = (inr ` (/) ) ) )
93	88, 92	mtbiri 633	. . . . . . . . . . 11 |- ( (/) e. u -> -. ( (inl |` u ) ` (/) ) = ( (inr |` 1o ) ` (/) ) )
94	93	adantl 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 ) ` (/) ) )
95	84, 94	pm2.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 )
96	95	olcd 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 ) )
97	96, 54	sylibr 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_ { (/) } )
99	98, 13	syl6sseqr 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 )
100	99	adantr 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 ) )
102	101	adantl 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 ) )
103	102	adantr 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
105	104	prid2 3534	. . . . . . . . . . 11 |- 1o e. { (/) , 1o }
106	105, 80	eleqtrri 2160	. . . . . . . . . 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	ffvelrnd 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 ) )
109	100, 108	exmidfodomrlemreseldju 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 ) ` (/) ) ) )
110	58, 97, 109	mpjaodan 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 )
112	24, 111	ax-mp 7	. . . . . . . . . 10 |- (/) e. suc 1o
113		df-2o 6138	. . . . . . . . . 10 |- 2o = suc 1o
114	112, 113	eleqtrri 2160	. . . . . . . . 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	ffvelrnd 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 ) )
117	99, 116	exmidfodomrlemreseldju 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 ) ` (/) ) ) )
118	55, 110, 117	mpjaodan 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 )
119	7, 8, 51, 118	exlimdd 1797	. . . 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 113	. . 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 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 ) )
123	121, 122	sylibr 132	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 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)