Theorem exmidfodomrlemr 7262

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 4217	. . . . . . . . . . . 12 ⊢ {∅} ∈ V
11		ssdomg 6832	. . . . . . . . . . . 12 ⊢ ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
12	10, 11	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13		df1o2 6482	. . . . . . . . . . 11 ⊢ 1o = {∅}
14	12, 13	breqtrrdi 4071	. . . . . . . . . 10 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ 1o)
15		1onn 6573	. . . . . . . . . . 11 ⊢ 1o ∈ ω
16		domrefg 6821	. . . . . . . . . . 11 ⊢ (1o ∈ ω → 1o ≼ 1o)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ 1o ≼ 1o
18		djudom 7152	. . . . . . . . . 10 ⊢ ((𝑢 ≼ 1o ∧ 1o ≼ 1o) → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
19	14, 17, 18	sylancl 413	. . . . . . . . 9 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
20		dju1p1e2 7257	. . . . . . . . 9 ⊢ (1o ⊔ 1o) ≈ 2o
21		domentr 6845	. . . . . . . . 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 6493	. . . . . . . . 9 ⊢ ∅ ∈ 1o
25		djurcl 7111	. . . . . . . . 9 ⊢ (∅ ∈ 1o → (inr‘∅) ∈ (𝑢 ⊔ 1o))
26	24, 25	ax-mp 5	. . . . . . . 8 ⊢ (inr‘∅) ∈ (𝑢 ⊔ 1o)
27		elex2 2776	. . . . . . . 8 ⊢ ((inr‘∅) ∈ (𝑢 ⊔ 1o) → ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o))
28	26, 27	ax-mp 5	. . . . . . 7 ⊢ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)
29	23, 28	jctil 312	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o))
30		vex 2763	. . . . . . . 8 ⊢ 𝑢 ∈ V
31		djuex 7102	. . . . . . . 8 ⊢ ((𝑢 ∈ V ∧ 1o ∈ ω) → (𝑢 ⊔ 1o) ∈ V)
32	30, 15, 31	mp2an 426	. . . . . . 7 ⊢ (𝑢 ⊔ 1o) ∈ V
33		2onn 6574	. . . . . . . 8 ⊢ 2o ∈ ω
34		breq2 4033	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑦 ≼ 𝑥 ↔ 𝑦 ≼ 2o))
35	34	anbi2d 464	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o)))
36		foeq2 5473	. . . . . . . . . . . 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 2847	. . . . . . . 8 ⊢ (2o ∈ ω → (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
41	33, 40	ax-mp 5	. . . . . . 7 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦))
42		eleq2 2257	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑢 ⊔ 1o)))
43	42	exbidv 1836	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)))
44		breq1 4032	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑦 ≼ 2o ↔ (𝑢 ⊔ 1o) ≼ 2o))
45	43, 44	anbi12d 473	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1o) → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o)))
46		foeq3 5474	. . . . . . . . . 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 2847	. . . . . . 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 5476	. . . . . . . . . . . . 13 ⊢ (𝑓:2o–onto→(𝑢 ⊔ 1o) → 𝑓:2o⟶(𝑢 ⊔ 1o))
54	53	adantl 277	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
55		elelsuc 4440	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ 1o → ∅ ∈ suc 1o)
56	24, 55	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ suc 1o
57		df-2o 6470	. . . . . . . . . . . . . 14 ⊢ 2o = suc 1o
58	56, 57	eleqtrri 2269	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 2o
59	58	a1i 9	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ∅ ∈ 2o)
60	54, 59	ffvelcdmd 5694	. . . . . . . . . . 11 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
61	60	adantr 276	. . . . . . . . . 10 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
62	52, 61	eqeltrrd 2271	. . . . . . . . 9 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
63		0ex 4156	. . . . . . . . . 10 ⊢ ∅ ∈ V
64		djulclb 7114	. . . . . . . . . 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 6477	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ V
73	72	prid2 3725	. . . . . . . . . . . . . . 15 ⊢ 1o ∈ {∅, 1o}
74		df2o3 6483	. . . . . . . . . . . . . . 15 ⊢ 2o = {∅, 1o}
75	73, 74	eleqtrri 2269	. . . . . . . . . . . . . 14 ⊢ 1o ∈ 2o
76	75	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 1o ∈ 2o)
77	71, 76	ffvelcdmd 5694	. . . . . . . . . . . 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 2271	. . . . . . . . . 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 7110	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1o))
85	84	adantl 277	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
86		foelrn 5795	. . . . . . . . . . . 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 5558	. . . . . . . . . . . . 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 2230	. . . . . . . . . . . 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 5558	. . . . . . . . . . . . 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 2230	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (inl‘∅) = (inr‘∅))
98		elpri 3641	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {∅, 1o} → (𝑤 = ∅ ∨ 𝑤 = 1o))
99	98, 74	eleq2s 2288	. . . . . . . . . . . . 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 2616	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) = (inr‘∅))
103		djune 7137	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
104	63, 63, 103	mp2an 426	. . . . . . . . . . . 12 ⊢ (inl‘∅) ≠ (inr‘∅)
105	104	neii 2366	. . . . . . . . . . 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 3228	. . . . . . . . 9 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ 1o)
112	111	adantr 276	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑢 ⊆ 1o)
113	112, 77	exmidfodomrlemeldju 7259	. . . . . . 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 7259	. . . . . 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 4224	. 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 2164   ≠ wne 2364  ∃wrex 2473  Vcvv 2760   ⊆ wss 3153  ∅c0 3446  {csn 3618  {cpr 3619   class class class wbr 4029  EXMIDwem 4223  suc csuc 4396  ωcom 4622  ⟶wf 5250  –onto→wfo 5252  ‘cfv 5254  1_oc1o 6462  2_oc2o 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:  exmidfodomr  7264