Theorem exmidfodomrlemr 7236

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 1539	. . . . . . . . 9 ⊢ Ⅎ𝑓(∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥)
2		nfe1 1507	. . . . . . . . 9 ⊢ Ⅎ𝑓∃𝑓 𝑓:𝑥–onto→𝑦
3	1, 2	nfim 1583	. . . . . . . 8 ⊢ Ⅎ𝑓((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
4	3	nfal 1587	. . . . . . 7 ⊢ Ⅎ𝑓∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
5	4	nfal 1587	. . . . . 6 ⊢ Ⅎ𝑓∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
6		nfv 1539	. . . . . 6 ⊢ Ⅎ𝑓 𝑢 ⊆ {∅}
7	5, 6	nfan 1576	. . . . 5 ⊢ Ⅎ𝑓(∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅})
8		nfv 1539	. . . . 5 ⊢ Ⅎ𝑓DECID ∅ ∈ 𝑢
9		simpl 109	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦))
10		p0ex 4209	. . . . . . . . . . . 12 ⊢ {∅} ∈ V
11		ssdomg 6808	. . . . . . . . . . . 12 ⊢ ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
12	10, 11	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13		df1o2 6458	. . . . . . . . . . 11 ⊢ 1o = {∅}
14	12, 13	breqtrrdi 4063	. . . . . . . . . 10 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ 1o)
15		1onn 6549	. . . . . . . . . . 11 ⊢ 1o ∈ ω
16		domrefg 6797	. . . . . . . . . . 11 ⊢ (1o ∈ ω → 1o ≼ 1o)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ 1o ≼ 1o
18		djudom 7126	. . . . . . . . . 10 ⊢ ((𝑢 ≼ 1o ∧ 1o ≼ 1o) → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
19	14, 17, 18	sylancl 413	. . . . . . . . 9 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
20		dju1p1e2 7231	. . . . . . . . 9 ⊢ (1o ⊔ 1o) ≈ 2o
21		domentr 6821	. . . . . . . . 9 ⊢ (((𝑢 ⊔ 1o) ≼ (1o ⊔ 1o) ∧ (1o ⊔ 1o) ≈ 2o) → (𝑢 ⊔ 1o) ≼ 2o)
22	19, 20, 21	sylancl 413	. . . . . . . 8 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ 2o)
23	22	adantl 277	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (𝑢 ⊔ 1o) ≼ 2o)
24		0lt1o 6469	. . . . . . . . 9 ⊢ ∅ ∈ 1o
25		djurcl 7085	. . . . . . . . 9 ⊢ (∅ ∈ 1o → (inr‘∅) ∈ (𝑢 ⊔ 1o))
26	24, 25	ax-mp 5	. . . . . . . 8 ⊢ (inr‘∅) ∈ (𝑢 ⊔ 1o)
27		elex2 2768	. . . . . . . 8 ⊢ ((inr‘∅) ∈ (𝑢 ⊔ 1o) → ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o))
28	26, 27	ax-mp 5	. . . . . . 7 ⊢ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)
29	23, 28	jctil 312	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o))
30		vex 2755	. . . . . . . 8 ⊢ 𝑢 ∈ V
31		djuex 7076	. . . . . . . 8 ⊢ ((𝑢 ∈ V ∧ 1o ∈ ω) → (𝑢 ⊔ 1o) ∈ V)
32	30, 15, 31	mp2an 426	. . . . . . 7 ⊢ (𝑢 ⊔ 1o) ∈ V
33		2onn 6550	. . . . . . . 8 ⊢ 2o ∈ ω
34		breq2 4025	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑦 ≼ 𝑥 ↔ 𝑦 ≼ 2o))
35	34	anbi2d 464	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o)))
36		foeq2 5457	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑓:𝑥–onto→𝑦 ↔ 𝑓:2o–onto→𝑦))
37	36	exbidv 1836	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → (∃𝑓 𝑓:𝑥–onto→𝑦 ↔ ∃𝑓 𝑓:2o–onto→𝑦))
38	35, 37	imbi12d 234	. . . . . . . . . 10 ⊢ (𝑥 = 2o → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
39	38	albidv 1835	. . . . . . . . 9 ⊢ (𝑥 = 2o → (∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
40	39	spcgv 2839	. . . . . . . 8 ⊢ (2o ∈ ω → (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
41	33, 40	ax-mp 5	. . . . . . 7 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦))
42		eleq2 2253	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑢 ⊔ 1o)))
43	42	exbidv 1836	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)))
44		breq1 4024	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑦 ≼ 2o ↔ (𝑢 ⊔ 1o) ≼ 2o))
45	43, 44	anbi12d 473	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1o) → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o)))
46		foeq3 5458	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑓:2o–onto→𝑦 ↔ 𝑓:2o–onto→(𝑢 ⊔ 1o)))
47	46	exbidv 1836	. . . . . . . . 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 2839	. . . . . . 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 5460	. . . . . . . . . . . . 13 ⊢ (𝑓:2o–onto→(𝑢 ⊔ 1o) → 𝑓:2o⟶(𝑢 ⊔ 1o))
54	53	adantl 277	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
55		elelsuc 4430	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ 1o → ∅ ∈ suc 1o)
56	24, 55	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ suc 1o
57		df-2o 6446	. . . . . . . . . . . . . 14 ⊢ 2o = suc 1o
58	56, 57	eleqtrri 2265	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 2o
59	58	a1i 9	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ∅ ∈ 2o)
60	54, 59	ffvelcdmd 5676	. . . . . . . . . . 11 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
61	60	adantr 276	. . . . . . . . . 10 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
62	52, 61	eqeltrrd 2267	. . . . . . . . 9 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
63		0ex 4148	. . . . . . . . . 10 ⊢ ∅ ∈ V
64		djulclb 7088	. . . . . . . . . 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 734	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
68		df-dc 836	. . . . . . 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 6453	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ V
73	72	prid2 3717	. . . . . . . . . . . . . . 15 ⊢ 1o ∈ {∅, 1o}
74		df2o3 6459	. . . . . . . . . . . . . . 15 ⊢ 2o = {∅, 1o}
75	73, 74	eleqtrri 2265	. . . . . . . . . . . . . 14 ⊢ 1o ∈ 2o
76	75	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 1o ∈ 2o)
77	71, 76	ffvelcdmd 5676	. . . . . . . . . . . 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 2267	. . . . . . . . . 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 734	. . . . . . . 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 542	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → 𝑓:2o–onto→(𝑢 ⊔ 1o))
84		djulcl 7084	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1o))
85	84	adantl 277	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
86		foelrn 5777	. . . . . . . . . . . 12 ⊢ ((𝑓:2o–onto→(𝑢 ⊔ 1o) ∧ (inl‘∅) ∈ (𝑢 ⊔ 1o)) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓‘𝑤))
87	83, 85, 86	syl2anc 411	. . . . . . . . . . 11 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓‘𝑤))
88		simplrr 536	. . . . . . . . . . . . 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 5541	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘𝑤) = (𝑓‘∅))
91		simp-5r 544	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘∅) = (inr‘∅))
92	88, 90, 91	3eqtrd 2226	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (inr‘∅))
93		simplrr 536	. . . . . . . . . . . . 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 5541	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (𝑓‘𝑤) = (𝑓‘1o))
96		simp-4r 542	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (𝑓‘1o) = (inr‘∅))
97	93, 95, 96	3eqtrd 2226	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (inl‘∅) = (inr‘∅))
98		elpri 3633	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {∅, 1o} → (𝑤 = ∅ ∨ 𝑤 = 1o))
99	98, 74	eleq2s 2284	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 2o → (𝑤 = ∅ ∨ 𝑤 = 1o))
100	99	ad2antrl 490	. . . . . . . . . . . 12 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (𝑤 = ∅ ∨ 𝑤 = 1o))
101	92, 97, 100	mpjaodan 799	. . . . . . . . . . 11 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (inl‘∅) = (inr‘∅))
102	87, 101	rexlimddv 2612	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) = (inr‘∅))
103		djune 7111	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
104	63, 63, 103	mp2an 426	. . . . . . . . . . . 12 ⊢ (inl‘∅) ≠ (inr‘∅)
105	104	neii 2362	. . . . . . . . . . 11 ⊢ ¬ (inl‘∅) = (inr‘∅)
106	105	a1i 9	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ¬ (inl‘∅) = (inr‘∅))
107	102, 106	pm2.65da 662	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → ¬ ∅ ∈ 𝑢)
108	107	olcd 735	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
109	108, 68	sylibr 134	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
110		simplr 528	. . . . . . . . . 10 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ {∅})
111	110, 13	sseqtrrdi 3219	. . . . . . . . 9 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ 1o)
112	111	adantr 276	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑢 ⊆ 1o)
113	112, 77	exmidfodomrlemeldju 7233	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → ((𝑓‘1o) = (inl‘∅) ∨ (𝑓‘1o) = (inr‘∅)))
114	82, 109, 113	mpjaodan 799	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
115	111, 60	exmidfodomrlemeldju 7233	. . . . . 6 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ((𝑓‘∅) = (inl‘∅) ∨ (𝑓‘∅) = (inr‘∅)))
116	69, 114, 115	mpjaodan 799	. . . . 5 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → DECID ∅ ∈ 𝑢)
117	7, 8, 51, 116	exlimdd 1883	. . . 4 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → DECID ∅ ∈ 𝑢)
118	117	ex 115	. . 3 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → (𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
119	118	alrimiv 1885	. 2 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
120		df-exmid 4216	. 2 ⊢ (EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
121	119, 120	sylibr 134	1 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  DECID wdc 835  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2160   ≠ wne 2360  ∃wrex 2469  Vcvv 2752   ⊆ wss 3144  ∅c0 3437  {csn 3610  {cpr 3611   class class class wbr 4021  EXMIDwem 4215  suc csuc 4386  ωcom 4610  ⟶wf 5234  –onto→wfo 5236  ‘cfv 5238  1_oc1o 6438  2_oc2o 6439   ≈ cen 6768   ≼ cdom 6769   ⊔ cdju 7070  inlcinl 7078  inrcinr 7079

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 2162  ax-14 2163  ax-ext 2171  ax-coll 4136  ax-sep 4139  ax-nul 4147  ax-pow 4195  ax-pr 4230  ax-un 4454  ax-setind 4557  ax-iinf 4608

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 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-int 3863  df-iun 3906  df-br 4022  df-opab 4083  df-mpt 4084  df-tr 4120  df-exmid 4216  df-id 4314  df-iord 4387  df-on 4389  df-suc 4392  df-iom 4611  df-xp 4653  df-rel 4654  df-cnv 4655  df-co 4656  df-dm 4657  df-rn 4658  df-res 4659  df-ima 4660  df-iota 5199  df-fun 5240  df-fn 5241  df-f 5242  df-f1 5243  df-fo 5244  df-f1o 5245  df-fv 5246  df-1st 6169  df-2nd 6170  df-1o 6445  df-2o 6446  df-er 6563  df-en 6771  df-dom 6772  df-dju 7071  df-inl 7080  df-inr 7081  df-case 7117

This theorem is referenced by:  exmidfodomr  7238