Theorem exmidfodomrlemr 7554

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. (Contributed by Jim Kingdon, 1-Jul-2022.)

Assertion

Ref	Expression
exmidfodomrlemr	⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)

Distinct variable group:   𝑥,𝑓,𝑦,𝑧

Proof of Theorem exmidfodomrlemr

Dummy variables 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1581	. . . . . . . . 9 ⊢ Ⅎ𝑓(∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥)
2		nfe1 1549	. . . . . . . . 9 ⊢ Ⅎ𝑓∃𝑓 𝑓:𝑥–onto→𝑦
3	1, 2	nfim 1625	. . . . . . . 8 ⊢ Ⅎ𝑓((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
4	3	nfal 1629	. . . . . . 7 ⊢ Ⅎ𝑓∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
5	4	nfal 1629	. . . . . 6 ⊢ Ⅎ𝑓∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
6		nfv 1581	. . . . . 6 ⊢ Ⅎ𝑓 𝑢 ⊆ {∅}
7	5, 6	nfan 1618	. . . . 5 ⊢ Ⅎ𝑓(∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅})
8		nfv 1581	. . . . 5 ⊢ Ⅎ𝑓DECID ∅ ∈ 𝑢
9		simpl 109	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦))
10		p0ex 4325	. . . . . . . . . . . 12 ⊢ {∅} ∈ V
11		ssdomg 7065	. . . . . . . . . . . 12 ⊢ ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
12	10, 11	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13		df1o2 6701	. . . . . . . . . . 11 ⊢ 1o = {∅}
14	12, 13	breqtrrdi 4172	. . . . . . . . . 10 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ 1o)
15		1onn 6793	. . . . . . . . . . 11 ⊢ 1o ∈ ω
16		domrefg 7053	. . . . . . . . . . 11 ⊢ (1o ∈ ω → 1o ≼ 1o)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ 1o ≼ 1o
18		djudom 7433	. . . . . . . . . 10 ⊢ ((𝑢 ≼ 1o ∧ 1o ≼ 1o) → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
19	14, 17, 18	sylancl 417	. . . . . . . . 9 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
20		dju1p1e2 7549	. . . . . . . . 9 ⊢ (1o ⊔ 1o) ≈ 2o
21		domentr 7078	. . . . . . . . 9 ⊢ (((𝑢 ⊔ 1o) ≼ (1o ⊔ 1o) ∧ (1o ⊔ 1o) ≈ 2o) → (𝑢 ⊔ 1o) ≼ 2o)
22	19, 20, 21	sylancl 417	. . . . . . . 8 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ 2o)
23	22	adantl 277	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (𝑢 ⊔ 1o) ≼ 2o)
24		0lt1o 6713	. . . . . . . . 9 ⊢ ∅ ∈ 1o
25		djurcl 7392	. . . . . . . . 9 ⊢ (∅ ∈ 1o → (inr‘∅) ∈ (𝑢 ⊔ 1o))
26	24, 25	ax-mp 5	. . . . . . . 8 ⊢ (inr‘∅) ∈ (𝑢 ⊔ 1o)
27		elex2 2838	. . . . . . . 8 ⊢ ((inr‘∅) ∈ (𝑢 ⊔ 1o) → ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o))
28	26, 27	ax-mp 5	. . . . . . 7 ⊢ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)
29	23, 28	jctil 312	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o))
30		vex 2824	. . . . . . . 8 ⊢ 𝑢 ∈ V
31		djuex 7383	. . . . . . . 8 ⊢ ((𝑢 ∈ V ∧ 1o ∈ ω) → (𝑢 ⊔ 1o) ∈ V)
32	30, 15, 31	mp2an 430	. . . . . . 7 ⊢ (𝑢 ⊔ 1o) ∈ V
33		2onn 6794	. . . . . . . 8 ⊢ 2o ∈ ω
34		breq2 4134	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑦 ≼ 𝑥 ↔ 𝑦 ≼ 2o))
35	34	anbi2d 468	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o)))
36		foeq2 5612	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑓:𝑥–onto→𝑦 ↔ 𝑓:2o–onto→𝑦))
37	36	exbidv 1878	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → (∃𝑓 𝑓:𝑥–onto→𝑦 ↔ ∃𝑓 𝑓:2o–onto→𝑦))
38	35, 37	imbi12d 234	. . . . . . . . . 10 ⊢ (𝑥 = 2o → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
39	38	albidv 1877	. . . . . . . . 9 ⊢ (𝑥 = 2o → (∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
40	39	spcgv 2912	. . . . . . . 8 ⊢ (2o ∈ ω → (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
41	33, 40	ax-mp 5	. . . . . . 7 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦))
42		eleq2 2302	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑢 ⊔ 1o)))
43	42	exbidv 1878	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)))
44		breq1 4133	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑦 ≼ 2o ↔ (𝑢 ⊔ 1o) ≼ 2o))
45	43, 44	anbi12d 477	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1o) → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o)))
46		foeq3 5613	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑓:2o–onto→𝑦 ↔ 𝑓:2o–onto→(𝑢 ⊔ 1o)))
47	46	exbidv 1878	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (∃𝑓 𝑓:2o–onto→𝑦 ↔ ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o)))
48	45, 47	imbi12d 234	. . . . . . . 8 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o))))
49	48	spcgv 2912	. . . . . . 7 ⊢ ((𝑢 ⊔ 1o) ∈ V → (∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o))))
50	32, 41, 49	mpsyl 65	. . . . . 6 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o)))
51	9, 29, 50	sylc 62	. . . . 5 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o))
52		simpr 110	. . . . . . . . . 10 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) = (inl‘∅))
53		fof 5615	. . . . . . . . . . . . 13 ⊢ (𝑓:2o–onto→(𝑢 ⊔ 1o) → 𝑓:2o⟶(𝑢 ⊔ 1o))
54	53	adantl 277	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
55		elelsuc 4554	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ 1o → ∅ ∈ suc 1o)
56	24, 55	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ suc 1o
57		df-2o 6688	. . . . . . . . . . . . . 14 ⊢ 2o = suc 1o
58	56, 57	eleqtrri 2314	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 2o
59	58	a1i 9	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ∅ ∈ 2o)
60	54, 59	ffvelcdmd 5844	. . . . . . . . . . 11 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
61	60	adantr 276	. . . . . . . . . 10 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
62	52, 61	eqeltrrd 2316	. . . . . . . . 9 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
63		0ex 4260	. . . . . . . . . 10 ⊢ ∅ ∈ V
64		djulclb 7395	. . . . . . . . . 10 ⊢ (∅ ∈ V → (∅ ∈ 𝑢 ↔ (inl‘∅) ∈ (𝑢 ⊔ 1o)))
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (∅ ∈ 𝑢 ↔ (inl‘∅) ∈ (𝑢 ⊔ 1o))
66	62, 65	sylibr 134	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → ∅ ∈ 𝑢)
67	66	orcd 745	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
68		df-dc 847	. . . . . . 7 ⊢ (DECID ∅ ∈ 𝑢 ↔ (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
69	67, 68	sylibr 134	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → DECID ∅ ∈ 𝑢)
70		simpr 110	. . . . . . . . . . 11 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → (𝑓‘1o) = (inl‘∅))
71	54	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
72		1oex 6695	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ V
73	72	prid2 3818	. . . . . . . . . . . . . . 15 ⊢ 1o ∈ {∅, 1o}
74		df2o3 6702	. . . . . . . . . . . . . . 15 ⊢ 2o = {∅, 1o}
75	73, 74	eleqtrri 2314	. . . . . . . . . . . . . 14 ⊢ 1o ∈ 2o
76	75	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 1o ∈ 2o)
77	71, 76	ffvelcdmd 5844	. . . . . . . . . . . 12 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → (𝑓‘1o) ∈ (𝑢 ⊔ 1o))
78	77	adantr 276	. . . . . . . . . . 11 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → (𝑓‘1o) ∈ (𝑢 ⊔ 1o))
79	70, 78	eqeltrrd 2316	. . . . . . . . . 10 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
80	79, 65	sylibr 134	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → ∅ ∈ 𝑢)
81	80	orcd 745	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
82	81, 68	sylibr 134	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → DECID ∅ ∈ 𝑢)
83		simp-4r 548	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → 𝑓:2o–onto→(𝑢 ⊔ 1o))
84		djulcl 7391	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1o))
85	84	adantl 277	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
86		foelrn 5958	. . . . . . . . . . . 12 ⊢ ((𝑓:2o–onto→(𝑢 ⊔ 1o) ∧ (inl‘∅) ∈ (𝑢 ⊔ 1o)) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓‘𝑤))
87	83, 85, 86	syl2anc 415	. . . . . . . . . . 11 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓‘𝑤))
88		simplrr 542	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (𝑓‘𝑤))
89		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → 𝑤 = ∅)
90	89	fveq2d 5699	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘𝑤) = (𝑓‘∅))
91		simp-5r 550	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘∅) = (inr‘∅))
92	88, 90, 91	3eqtrd 2275	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (inr‘∅))
93		simplrr 542	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (inl‘∅) = (𝑓‘𝑤))
94		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → 𝑤 = 1o)
95	94	fveq2d 5699	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (𝑓‘𝑤) = (𝑓‘1o))
96		simp-4r 548	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (𝑓‘1o) = (inr‘∅))
97	93, 95, 96	3eqtrd 2275	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (inl‘∅) = (inr‘∅))
98		elpri 3732	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {∅, 1o} → (𝑤 = ∅ ∨ 𝑤 = 1o))
99	98, 74	eleq2s 2333	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 2o → (𝑤 = ∅ ∨ 𝑤 = 1o))
100	99	ad2antrl 494	. . . . . . . . . . . 12 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (𝑤 = ∅ ∨ 𝑤 = 1o))
101	92, 97, 100	mpjaodan 810	. . . . . . . . . . 11 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (inl‘∅) = (inr‘∅))
102	87, 101	rexlimddv 2673	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) = (inr‘∅))
103		djune 7418	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
104	63, 63, 103	mp2an 430	. . . . . . . . . . . 12 ⊢ (inl‘∅) ≠ (inr‘∅)
105	104	neii 2422	. . . . . . . . . . 11 ⊢ ¬ (inl‘∅) = (inr‘∅)
106	105	a1i 9	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ¬ (inl‘∅) = (inr‘∅))
107	102, 106	pm2.65da 671	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → ¬ ∅ ∈ 𝑢)
108	107	olcd 746	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
109	108, 68	sylibr 134	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
110		simplr 533	. . . . . . . . . 10 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ {∅})
111	110, 13	sseqtrrdi 3297	. . . . . . . . 9 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ 1o)
112	111	adantr 276	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑢 ⊆ 1o)
113	112, 77	exmidfodomrlemeldju 7551	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → ((𝑓‘1o) = (inl‘∅) ∨ (𝑓‘1o) = (inr‘∅)))
114	82, 109, 113	mpjaodan 810	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
115	111, 60	exmidfodomrlemeldju 7551	. . . . . 6 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ((𝑓‘∅) = (inl‘∅) ∨ (𝑓‘∅) = (inr‘∅)))
116	69, 114, 115	mpjaodan 810	. . . . 5 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → DECID ∅ ∈ 𝑢)
117	7, 8, 51, 116	exlimdd 1925	. . . 4 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → DECID ∅ ∈ 𝑢)
118	117	ex 115	. . 3 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → (𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
119	118	alrimiv 1927	. 2 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
120		df-exmid 4332	. 2 ⊢ (EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
121	119, 120	sylibr 134	1 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 720  DECID wdc 846  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209   ≠ wne 2420  ∃wrex 2529  Vcvv 2821   ⊆ wss 3220  ∅c0 3520  {csn 3709  {cpr 3710   class class class wbr 4130  EXMIDwem 4331  suc csuc 4510  ωcom 4737  ⟶wf 5373  –onto→wfo 5375  ‘cfv 5377  1_oc1o 6680  2_oc2o 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:  exmidfodomr  7556