Theorem exmidfodomrlemr 7075

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 1509	. . . . . . . . 9 ⊢ Ⅎ𝑓(∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥)
2		nfe1 1473	. . . . . . . . 9 ⊢ Ⅎ𝑓∃𝑓 𝑓:𝑥–onto→𝑦
3	1, 2	nfim 1552	. . . . . . . 8 ⊢ Ⅎ𝑓((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
4	3	nfal 1556	. . . . . . 7 ⊢ Ⅎ𝑓∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
5	4	nfal 1556	. . . . . 6 ⊢ Ⅎ𝑓∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
6		nfv 1509	. . . . . 6 ⊢ Ⅎ𝑓 𝑢 ⊆ {∅}
7	5, 6	nfan 1545	. . . . 5 ⊢ Ⅎ𝑓(∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅})
8		nfv 1509	. . . . 5 ⊢ Ⅎ𝑓DECID ∅ ∈ 𝑢
9		simpl 108	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦))
10		p0ex 4120	. . . . . . . . . . . 12 ⊢ {∅} ∈ V
11		ssdomg 6680	. . . . . . . . . . . 12 ⊢ ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
12	10, 11	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13		df1o2 6334	. . . . . . . . . . 11 ⊢ 1o = {∅}
14	12, 13	breqtrrdi 3978	. . . . . . . . . 10 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ 1o)
15		1onn 6424	. . . . . . . . . . 11 ⊢ 1o ∈ ω
16		domrefg 6669	. . . . . . . . . . 11 ⊢ (1o ∈ ω → 1o ≼ 1o)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ 1o ≼ 1o
18		djudom 6986	. . . . . . . . . 10 ⊢ ((𝑢 ≼ 1o ∧ 1o ≼ 1o) → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
19	14, 17, 18	sylancl 410	. . . . . . . . 9 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
20		dju1p1e2 7070	. . . . . . . . 9 ⊢ (1o ⊔ 1o) ≈ 2o
21		domentr 6693	. . . . . . . . 9 ⊢ (((𝑢 ⊔ 1o) ≼ (1o ⊔ 1o) ∧ (1o ⊔ 1o) ≈ 2o) → (𝑢 ⊔ 1o) ≼ 2o)
22	19, 20, 21	sylancl 410	. . . . . . . 8 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ 2o)
23	22	adantl 275	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (𝑢 ⊔ 1o) ≼ 2o)
24		0lt1o 6345	. . . . . . . . 9 ⊢ ∅ ∈ 1o
25		djurcl 6945	. . . . . . . . 9 ⊢ (∅ ∈ 1o → (inr‘∅) ∈ (𝑢 ⊔ 1o))
26	24, 25	ax-mp 5	. . . . . . . 8 ⊢ (inr‘∅) ∈ (𝑢 ⊔ 1o)
27		elex2 2705	. . . . . . . 8 ⊢ ((inr‘∅) ∈ (𝑢 ⊔ 1o) → ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o))
28	26, 27	ax-mp 5	. . . . . . 7 ⊢ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)
29	23, 28	jctil 310	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o))
30		vex 2692	. . . . . . . 8 ⊢ 𝑢 ∈ V
31		djuex 6936	. . . . . . . 8 ⊢ ((𝑢 ∈ V ∧ 1o ∈ ω) → (𝑢 ⊔ 1o) ∈ V)
32	30, 15, 31	mp2an 423	. . . . . . 7 ⊢ (𝑢 ⊔ 1o) ∈ V
33		2onn 6425	. . . . . . . 8 ⊢ 2o ∈ ω
34		breq2 3941	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑦 ≼ 𝑥 ↔ 𝑦 ≼ 2o))
35	34	anbi2d 460	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o)))
36		foeq2 5350	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑓:𝑥–onto→𝑦 ↔ 𝑓:2o–onto→𝑦))
37	36	exbidv 1798	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → (∃𝑓 𝑓:𝑥–onto→𝑦 ↔ ∃𝑓 𝑓:2o–onto→𝑦))
38	35, 37	imbi12d 233	. . . . . . . . . 10 ⊢ (𝑥 = 2o → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
39	38	albidv 1797	. . . . . . . . 9 ⊢ (𝑥 = 2o → (∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
40	39	spcgv 2776	. . . . . . . 8 ⊢ (2o ∈ ω → (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
41	33, 40	ax-mp 5	. . . . . . 7 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦))
42		eleq2 2204	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑢 ⊔ 1o)))
43	42	exbidv 1798	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)))
44		breq1 3940	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑦 ≼ 2o ↔ (𝑢 ⊔ 1o) ≼ 2o))
45	43, 44	anbi12d 465	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1o) → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o)))
46		foeq3 5351	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑓:2o–onto→𝑦 ↔ 𝑓:2o–onto→(𝑢 ⊔ 1o)))
47	46	exbidv 1798	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (∃𝑓 𝑓:2o–onto→𝑦 ↔ ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o)))
48	45, 47	imbi12d 233	. . . . . . . 8 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o))))
49	48	spcgv 2776	. . . . . . 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 109	. . . . . . . . . 10 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) = (inl‘∅))
53		fof 5353	. . . . . . . . . . . . 13 ⊢ (𝑓:2o–onto→(𝑢 ⊔ 1o) → 𝑓:2o⟶(𝑢 ⊔ 1o))
54	53	adantl 275	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
55		elelsuc 4339	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ 1o → ∅ ∈ suc 1o)
56	24, 55	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ suc 1o
57		df-2o 6322	. . . . . . . . . . . . . 14 ⊢ 2o = suc 1o
58	56, 57	eleqtrri 2216	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 2o
59	58	a1i 9	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ∅ ∈ 2o)
60	54, 59	ffvelrnd 5564	. . . . . . . . . . 11 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
61	60	adantr 274	. . . . . . . . . 10 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
62	52, 61	eqeltrrd 2218	. . . . . . . . 9 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
63		0ex 4063	. . . . . . . . . 10 ⊢ ∅ ∈ V
64		djulclb 6948	. . . . . . . . . 10 ⊢ (∅ ∈ V → (∅ ∈ 𝑢 ↔ (inl‘∅) ∈ (𝑢 ⊔ 1o)))
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (∅ ∈ 𝑢 ↔ (inl‘∅) ∈ (𝑢 ⊔ 1o))
66	62, 65	sylibr 133	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → ∅ ∈ 𝑢)
67	66	orcd 723	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
68		df-dc 821	. . . . . . 7 ⊢ (DECID ∅ ∈ 𝑢 ↔ (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
69	67, 68	sylibr 133	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inl‘∅)) → DECID ∅ ∈ 𝑢)
70		simpr 109	. . . . . . . . . . 11 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → (𝑓‘1o) = (inl‘∅))
71	54	adantr 274	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
72		1oex 6329	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ V
73	72	prid2 3638	. . . . . . . . . . . . . . 15 ⊢ 1o ∈ {∅, 1o}
74		df2o3 6335	. . . . . . . . . . . . . . 15 ⊢ 2o = {∅, 1o}
75	73, 74	eleqtrri 2216	. . . . . . . . . . . . . 14 ⊢ 1o ∈ 2o
76	75	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 1o ∈ 2o)
77	71, 76	ffvelrnd 5564	. . . . . . . . . . . 12 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → (𝑓‘1o) ∈ (𝑢 ⊔ 1o))
78	77	adantr 274	. . . . . . . . . . 11 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → (𝑓‘1o) ∈ (𝑢 ⊔ 1o))
79	70, 78	eqeltrrd 2218	. . . . . . . . . 10 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
80	79, 65	sylibr 133	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → ∅ ∈ 𝑢)
81	80	orcd 723	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
82	81, 68	sylibr 133	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inl‘∅)) → DECID ∅ ∈ 𝑢)
83		simp-4r 532	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → 𝑓:2o–onto→(𝑢 ⊔ 1o))
84		djulcl 6944	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1o))
85	84	adantl 275	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
86		foelrn 5662	. . . . . . . . . . . 12 ⊢ ((𝑓:2o–onto→(𝑢 ⊔ 1o) ∧ (inl‘∅) ∈ (𝑢 ⊔ 1o)) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓‘𝑤))
87	83, 85, 86	syl2anc 409	. . . . . . . . . . 11 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓‘𝑤))
88		simplrr 526	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (𝑓‘𝑤))
89		simpr 109	. . . . . . . . . . . . . 14 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → 𝑤 = ∅)
90	89	fveq2d 5433	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘𝑤) = (𝑓‘∅))
91		simp-5r 534	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘∅) = (inr‘∅))
92	88, 90, 91	3eqtrd 2177	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (inr‘∅))
93		simplrr 526	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (inl‘∅) = (𝑓‘𝑤))
94		simpr 109	. . . . . . . . . . . . . 14 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → 𝑤 = 1o)
95	94	fveq2d 5433	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (𝑓‘𝑤) = (𝑓‘1o))
96		simp-4r 532	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (𝑓‘1o) = (inr‘∅))
97	93, 95, 96	3eqtrd 2177	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (inl‘∅) = (inr‘∅))
98		elpri 3555	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {∅, 1o} → (𝑤 = ∅ ∨ 𝑤 = 1o))
99	98, 74	eleq2s 2235	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 2o → (𝑤 = ∅ ∨ 𝑤 = 1o))
100	99	ad2antrl 482	. . . . . . . . . . . 12 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (𝑤 = ∅ ∨ 𝑤 = 1o))
101	92, 97, 100	mpjaodan 788	. . . . . . . . . . 11 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (inl‘∅) = (inr‘∅))
102	87, 101	rexlimddv 2557	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) = (inr‘∅))
103		djune 6971	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
104	63, 63, 103	mp2an 423	. . . . . . . . . . . 12 ⊢ (inl‘∅) ≠ (inr‘∅)
105	104	neii 2311	. . . . . . . . . . 11 ⊢ ¬ (inl‘∅) = (inr‘∅)
106	105	a1i 9	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ¬ (inl‘∅) = (inr‘∅))
107	102, 106	pm2.65da 651	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → ¬ ∅ ∈ 𝑢)
108	107	olcd 724	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
109	108, 68	sylibr 133	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1o) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
110		simplr 520	. . . . . . . . . 10 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ {∅})
111	110, 13	sseqtrrdi 3151	. . . . . . . . 9 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ 1o)
112	111	adantr 274	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑢 ⊆ 1o)
113	112, 77	exmidfodomrlemeldju 7072	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → ((𝑓‘1o) = (inl‘∅) ∨ (𝑓‘1o) = (inr‘∅)))
114	82, 109, 113	mpjaodan 788	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
115	111, 60	exmidfodomrlemeldju 7072	. . . . . 6 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ((𝑓‘∅) = (inl‘∅) ∨ (𝑓‘∅) = (inr‘∅)))
116	69, 114, 115	mpjaodan 788	. . . . 5 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → DECID ∅ ∈ 𝑢)
117	7, 8, 51, 116	exlimdd 1845	. . . 4 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → DECID ∅ ∈ 𝑢)
118	117	ex 114	. . 3 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → (𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
119	118	alrimiv 1847	. 2 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
120		df-exmid 4127	. 2 ⊢ (EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
121	119, 120	sylibr 133	1 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820  ∀wal 1330   = wceq 1332  ∃wex 1469   ∈ wcel 1481   ≠ wne 2309  ∃wrex 2418  Vcvv 2689   ⊆ wss 3076  ∅c0 3368  {csn 3532  {cpr 3533   class class class wbr 3937  EXMIDwem 4126  suc csuc 4295  ωcom 4512  ⟶wf 5127  –onto→wfo 5129  ‘cfv 5131  1_oc1o 6314  2_oc2o 6315   ≈ cen 6640   ≼ cdom 6641   ⊔ cdju 6930  inlcinl 6938  inrcinr 6939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4051  ax-sep 4054  ax-nul 4062  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-iinf 4510

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-iun 3823  df-br 3938  df-opab 3998  df-mpt 3999  df-tr 4035  df-exmid 4127  df-id 4223  df-iord 4296  df-on 4298  df-suc 4301  df-iom 4513  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-1st 6046  df-2nd 6047  df-1o 6321  df-2o 6322  df-er 6437  df-en 6643  df-dom 6644  df-dju 6931  df-inl 6940  df-inr 6941  df-case 6977

This theorem is referenced by:  exmidfodomr  7077