Theorem exmidfodomrlemrALT 7263

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 7262. In particular, this proof uses eldju 7127 instead of djur 7128 and avoids djulclb 7114. (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 1539	. . . . . . . . 9 |- F/ f ( E. z z e. y /\ y ~<_ x )
2		nfe1 1507	. . . . . . . . 9 |- F/ f E. f f : x -onto-> y
3	1, 2	nfim 1583	. . . . . . . 8 |- F/ f ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
4	3	nfal 1587	. . . . . . 7 |- F/ f A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
5	4	nfal 1587	. . . . . 6 |- F/ f A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y )
6		nfv 1539	. . . . . 6 |- F/ f u C_ { (/) }
7	5, 6	nfan 1576	. . . . 5 |- F/ f ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) /\ u C_ { (/) } )
8		nfv 1539	. . . . 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 4217	. . . . . . . . . . . 12 |- { (/) } e. _V
11		ssdomg 6832	. . . . . . . . . . . 12 |- ( { (/) } e. _V -> ( u C_ { (/) } -> u ~<_ { (/) } ) )
12	10, 11	ax-mp 5	. . . . . . . . . . 11 |- ( u C_ { (/) } -> u ~<_ { (/) } )
13		df1o2 6482	. . . . . . . . . . 11 |- 1o = { (/) }
14	12, 13	breqtrrdi 4071	. . . . . . . . . 10 |- ( u C_ { (/) } -> u ~<_ 1o )
15		1onn 6573	. . . . . . . . . . 11 |- 1o e. om
16		domrefg 6821	. . . . . . . . . . 11 |- ( 1o e. om -> 1o ~<_ 1o )
17	15, 16	ax-mp 5	. . . . . . . . . 10 |- 1o ~<_ 1o
18		djudom 7152	. . . . . . . . . 10 |- ( ( u ~<_ 1o /\ 1o ~<_ 1o ) -> ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) )
19	14, 17, 18	sylancl 413	. . . . . . . . 9 |- ( u C_ { (/) } -> ( u ⊔ 1o ) ~<_ ( 1o ⊔ 1o ) )
20		dju1p1e2 7257	. . . . . . . . 9 |- ( 1o ⊔ 1o ) ~~ 2o
21		domentr 6845	. . . . . . . . 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 6493	. . . . . . . . 9 |- (/) e. 1o
25		djurcl 7111	. . . . . . . . 9 |- ( (/) e. 1o -> (inr ` (/) ) e. ( u ⊔ 1o ) )
26	24, 25	ax-mp 5	. . . . . . . 8 |- (inr ` (/) ) e. ( u ⊔ 1o )
27		elex2 2776	. . . . . . . 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 2763	. . . . . . . 8 |- u e. _V
31		djuex 7102	. . . . . . . 8 |- ( ( u e. _V /\ 1o e. om ) -> ( u ⊔ 1o ) e. _V )
32	30, 15, 31	mp2an 426	. . . . . . 7 |- ( u ⊔ 1o ) e. _V
33		2onn 6574	. . . . . . . 8 |- 2o e. om
34		breq2 4033	. . . . . . . . . . . 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 5473	. . . . . . . . . . . 12 |- ( x = 2o -> ( f : x -onto-> y <-> f : 2o -onto-> y ) )
37	36	exbidv 1836	. . . . . . . . . . 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 1835	. . . . . . . . 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 2847	. . . . . . . 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 2257	. . . . . . . . . . 11 |- ( y = ( u ⊔ 1o ) -> ( z e. y <-> z e. ( u ⊔ 1o ) ) )
43	42	exbidv 1836	. . . . . . . . . 10 |- ( y = ( u ⊔ 1o ) -> ( E. z z e. y <-> E. z z e. ( u ⊔ 1o ) ) )
44		breq1 4032	. . . . . . . . . 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 5474	. . . . . . . . . 10 |- ( y = ( u ⊔ 1o ) -> ( f : 2o -onto-> y <-> f : 2o -onto-> ( u ⊔ 1o ) ) )
47	46	exbidv 1836	. . . . . . . . 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 2847	. . . . . . 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 734	. . . . . . 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 836	. . . . . . 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 734	. . . . . . . 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 7110	. . . . . . . . . . . . 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 5795	. . . . . . . . . . . 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 5578	. . . . . . . . . . . . . . . . 17 |- ( (/) e. u -> ( (inl |` u ) ` (/) ) = (inl ` (/) ) )
66	65	eqeq1d 2202	. . . . . . . . . . . . . . . 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 5558	. . . . . . . . . . . . 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 2230	. . . . . . . . . . . 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 5558	. . . . . . . . . . . . 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 2230	. . . . . . . . . . . 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 3641	. . . . . . . . . . . . . 14 |- ( w e. { (/) , 1o } -> ( w = (/) \/ w = 1o ) )
80		df2o3 6483	. . . . . . . . . . . . . 14 |- 2o = { (/) , 1o }
81	79, 80	eleq2s 2288	. . . . . . . . . . . . 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 799	. . . . . . . . . . 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 2616	. . . . . . . . . 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 4156	. . . . . . . . . . . . . 14 |- (/) e. _V
86		djune 7137	. . . . . . . . . . . . . 14 |- ( ( (/) e. _V /\ (/) e. _V ) -> (inl ` (/) ) =/= (inr ` (/) ) )
87	85, 85, 86	mp2an 426	. . . . . . . . . . . . 13 |- (inl ` (/) ) =/= (inr ` (/) )
88	87	neii 2366	. . . . . . . . . . . 12 |- -. (inl ` (/) ) = (inr ` (/) )
89		fvres 5578	. . . . . . . . . . . . . . 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 2208	. . . . . . . . . . . 12 |- ( (/) e. u -> ( ( (inl |` u ) ` (/) ) = ( (inr |` 1o ) ` (/) ) <-> (inl ` (/) ) = (inr ` (/) ) ) )
93	88, 92	mtbiri 676	. . . . . . . . . . 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 662	. . . . . . . . 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 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 ) ` (/) ) ) /\ ( 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 3228	. . . . . . . . 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 5476	. . . . . . . . . . 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 6477	. . . . . . . . . . . 12 |- 1o e. _V
105	104	prid2 3725	. . . . . . . . . . 11 |- 1o e. { (/) , 1o }
106	105, 80	eleqtrri 2269	. . . . . . . . . 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 5694	. . . . . . . 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 7260	. . . . . . 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 799	. . . . . 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 4440	. . . . . . . . . . 11 |- ( (/) e. 1o -> (/) e. suc 1o )
112	24, 111	ax-mp 5	. . . . . . . . . 10 |- (/) e. suc 1o
113		df-2o 6470	. . . . . . . . . 10 |- 2o = suc 1o
114	112, 113	eleqtrri 2269	. . . . . . . . 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 5694	. . . . . . 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 7260	. . . . . 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 799	. . . . 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 1883	. . . 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 1885	. 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 4224	. 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 709  DECID wdc 835   A.wal 1362   = wceq 1364   E.wex 1503   e. wcel 2164   =/= wne 2364   E.wrex 2473   _Vcvv 2760   C_ wss 3153   (/)c0 3446   {csn 3618   {cpr 3619   class class class wbr 4029  EXMIDwem 4223   suc csuc 4396   omcom 4622   |` cres 4661   -->wf 5250   -onto->wfo 5252   ` cfv 5254   1oc1o 6462   2oc2o 6463   ~~ cen 6792   ~<_ cdom 6793   ⊔ cdju 7096  inlcinl 7104  inrcinr 7105

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-iinf 4620

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-exmid 4224  df-id 4324  df-iord 4397  df-on 4399  df-suc 4402  df-iom 4623  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-1st 6193  df-2nd 6194  df-1o 6469  df-2o 6470  df-er 6587  df-en 6795  df-dom 6796  df-dju 7097  df-inl 7106  df-inr 7107  df-case 7143

This theorem is referenced by: (None)