exmidfodomrlemr - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > exmidfodomrlemr		GIF version

Theorem exmidfodomrlemr 7203

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 1528	. . . . . . . . 9 ⊢ Ⅎ𝑓(∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥)
2		nfe1 1496	. . . . . . . . 9 ⊢ Ⅎ𝑓∃𝑓 𝑓:𝑥–onto→𝑦
3	1, 2	nfim 1572	. . . . . . . 8 ⊢ Ⅎ𝑓((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
4	3	nfal 1576	. . . . . . 7 ⊢ Ⅎ𝑓∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
5	4	nfal 1576	. . . . . 6 ⊢ Ⅎ𝑓∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
6		nfv 1528	. . . . . 6 ⊢ Ⅎ𝑓 𝑢 ⊆ {∅}
7	5, 6	nfan 1565	. . . . 5 ⊢ Ⅎ𝑓(∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅})
8		nfv 1528	. . . . 5 ⊢ Ⅎ𝑓DECID ∅ ∈ 𝑢
9		simpl 109	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦))
10		p0ex 4190	. . . . . . . . . . . 12 ⊢ {∅} ∈ V
11		ssdomg 6780	. . . . . . . . . . . 12 ⊢ ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
12	10, 11	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13		df1o2 6432	. . . . . . . . . . 11 ⊢ 1_o = {∅}
14	12, 13	breqtrrdi 4047	. . . . . . . . . 10 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ 1_o)
15		1onn 6523	. . . . . . . . . . 11 ⊢ 1_o ∈ ω
16		domrefg 6769	. . . . . . . . . . 11 ⊢ (1_o ∈ ω → 1_o ≼ 1_o)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ 1_o ≼ 1_o
18		djudom 7094	. . . . . . . . . 10 ⊢ ((𝑢 ≼ 1_o ∧ 1_o ≼ 1_o) → (𝑢 ⊔ 1_o) ≼ (1_o ⊔ 1_o))
19	14, 17, 18	sylancl 413	. . . . . . . . 9 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1_o) ≼ (1_o ⊔ 1_o))
20		dju1p1e2 7198	. . . . . . . . 9 ⊢ (1_o ⊔ 1_o) ≈ 2_o
21		domentr 6793	. . . . . . . . 9 ⊢ (((𝑢 ⊔ 1_o) ≼ (1_o ⊔ 1_o) ∧ (1_o ⊔ 1_o) ≈ 2_o) → (𝑢 ⊔ 1_o) ≼ 2_o)
22	19, 20, 21	sylancl 413	. . . . . . . 8 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1_o) ≼ 2_o)
23	22	adantl 277	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (𝑢 ⊔ 1_o) ≼ 2_o)
24		0lt1o 6443	. . . . . . . . 9 ⊢ ∅ ∈ 1_o
25		djurcl 7053	. . . . . . . . 9 ⊢ (∅ ∈ 1_o → (inr‘∅) ∈ (𝑢 ⊔ 1_o))
26	24, 25	ax-mp 5	. . . . . . . 8 ⊢ (inr‘∅) ∈ (𝑢 ⊔ 1_o)
27		elex2 2755	. . . . . . . 8 ⊢ ((inr‘∅) ∈ (𝑢 ⊔ 1_o) → ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1_o))
28	26, 27	ax-mp 5	. . . . . . 7 ⊢ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1_o)
29	23, 28	jctil 312	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1_o) ∧ (𝑢 ⊔ 1_o) ≼ 2_o))
30		vex 2742	. . . . . . . 8 ⊢ 𝑢 ∈ V
31		djuex 7044	. . . . . . . 8 ⊢ ((𝑢 ∈ V ∧ 1_o ∈ ω) → (𝑢 ⊔ 1_o) ∈ V)
32	30, 15, 31	mp2an 426	. . . . . . 7 ⊢ (𝑢 ⊔ 1_o) ∈ V
33		2onn 6524	. . . . . . . 8 ⊢ 2_o ∈ ω
34		breq2 4009	. . . . . . . . . . . 12 ⊢ (𝑥 = 2_o → (𝑦 ≼ 𝑥 ↔ 𝑦 ≼ 2_o))
35	34	anbi2d 464	. . . . . . . . . . 11 ⊢ (𝑥 = 2_o → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2_o)))
36		foeq2 5437	. . . . . . . . . . . 12 ⊢ (𝑥 = 2_o → (𝑓:𝑥–onto→𝑦 ↔ 𝑓:2_o–onto→𝑦))
37	36	exbidv 1825	. . . . . . . . . . 11 ⊢ (𝑥 = 2_o → (∃𝑓 𝑓:𝑥–onto→𝑦 ↔ ∃𝑓 𝑓:2_o–onto→𝑦))
38	35, 37	imbi12d 234	. . . . . . . . . 10 ⊢ (𝑥 = 2_o → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→𝑦)))
39	38	albidv 1824	. . . . . . . . 9 ⊢ (𝑥 = 2_o → (∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→𝑦)))
40	39	spcgv 2826	. . . . . . . 8 ⊢ (2_o ∈ ω → (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→𝑦)))
41	33, 40	ax-mp 5	. . . . . . 7 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→𝑦))
42		eleq2 2241	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ⊔ 1_o) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑢 ⊔ 1_o)))
43	42	exbidv 1825	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1_o) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1_o)))
44		breq1 4008	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1_o) → (𝑦 ≼ 2_o ↔ (𝑢 ⊔ 1_o) ≼ 2_o))
45	43, 44	anbi12d 473	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1_o) → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2_o) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1_o) ∧ (𝑢 ⊔ 1_o) ≼ 2_o)))
46		foeq3 5438	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1_o) → (𝑓:2_o–onto→𝑦 ↔ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)))
47	46	exbidv 1825	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1_o) → (∃𝑓 𝑓:2_o–onto→𝑦 ↔ ∃𝑓 𝑓:2_o–onto→(𝑢 ⊔ 1_o)))
48	45, 47	imbi12d 234	. . . . . . . 8 ⊢ (𝑦 = (𝑢 ⊔ 1_o) → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1_o) ∧ (𝑢 ⊔ 1_o) ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→(𝑢 ⊔ 1_o))))
49	48	spcgv 2826	. . . . . . 7 ⊢ ((𝑢 ⊔ 1_o) ∈ V → (∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1_o) ∧ (𝑢 ⊔ 1_o) ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→(𝑢 ⊔ 1_o))))
50	32, 41, 49	mpsyl 65	. . . . . 6 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1_o) ∧ (𝑢 ⊔ 1_o) ≼ 2_o) → ∃𝑓 𝑓:2_o–onto→(𝑢 ⊔ 1_o)))
51	9, 29, 50	sylc 62	. . . . 5 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → ∃𝑓 𝑓:2_o–onto→(𝑢 ⊔ 1_o))
52		simpr 110	. . . . . . . . . 10 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) = (inl‘∅))
53		fof 5440	. . . . . . . . . . . . 13 ⊢ (𝑓:2_o–onto→(𝑢 ⊔ 1_o) → 𝑓:2_o⟶(𝑢 ⊔ 1_o))
54	53	adantl 277	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) → 𝑓:2_o⟶(𝑢 ⊔ 1_o))
55		elelsuc 4411	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ 1_o → ∅ ∈ suc 1_o)
56	24, 55	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ suc 1_o
57		df-2o 6420	. . . . . . . . . . . . . 14 ⊢ 2_o = suc 1_o
58	56, 57	eleqtrri 2253	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 2_o
59	58	a1i 9	. . . . . . . . . . . 12 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) → ∅ ∈ 2_o)
60	54, 59	ffvelcdmd 5654	. . . . . . . . . . 11 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1_o))
61	60	adantr 276	. . . . . . . . . 10 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inl‘∅)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1_o))
62	52, 61	eqeltrrd 2255	. . . . . . . . 9 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1_o))
63		0ex 4132	. . . . . . . . . 10 ⊢ ∅ ∈ V
64		djulclb 7056	. . . . . . . . . 10 ⊢ (∅ ∈ V → (∅ ∈ 𝑢 ↔ (inl‘∅) ∈ (𝑢 ⊔ 1_o)))
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (∅ ∈ 𝑢 ↔ (inl‘∅) ∈ (𝑢 ⊔ 1_o))
66	62, 65	sylibr 134	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inl‘∅)) → ∅ ∈ 𝑢)
67	66	orcd 733	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
68		df-dc 835	. . . . . . 7 ⊢ (DECID ∅ ∈ 𝑢 ↔ (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
69	67, 68	sylibr 134	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inl‘∅)) → DECID ∅ ∈ 𝑢)
70		simpr 110	. . . . . . . . . . 11 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inl‘∅)) → (𝑓‘1_o) = (inl‘∅))
71	54	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑓:2_o⟶(𝑢 ⊔ 1_o))
72		1oex 6427	. . . . . . . . . . . . . . . 16 ⊢ 1_o ∈ V
73	72	prid2 3701	. . . . . . . . . . . . . . 15 ⊢ 1_o ∈ {∅, 1_o}
74		df2o3 6433	. . . . . . . . . . . . . . 15 ⊢ 2_o = {∅, 1_o}
75	73, 74	eleqtrri 2253	. . . . . . . . . . . . . 14 ⊢ 1_o ∈ 2_o
76	75	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) → 1_o ∈ 2_o)
77	71, 76	ffvelcdmd 5654	. . . . . . . . . . . 12 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) → (𝑓‘1_o) ∈ (𝑢 ⊔ 1_o))
78	77	adantr 276	. . . . . . . . . . 11 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inl‘∅)) → (𝑓‘1_o) ∈ (𝑢 ⊔ 1_o))
79	70, 78	eqeltrrd 2255	. . . . . . . . . 10 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inl‘∅)) → (inl‘∅) ∈ (𝑢 ⊔ 1_o))
80	79, 65	sylibr 134	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inl‘∅)) → ∅ ∈ 𝑢)
81	80	orcd 733	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inl‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
82	81, 68	sylibr 134	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inl‘∅)) → DECID ∅ ∈ 𝑢)
83		simp-4r 542	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → 𝑓:2_o–onto→(𝑢 ⊔ 1_o))
84		djulcl 7052	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1_o))
85	84	adantl 277	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1_o))
86		foelrn 5755	. . . . . . . . . . . 12 ⊢ ((𝑓:2_o–onto→(𝑢 ⊔ 1_o) ∧ (inl‘∅) ∈ (𝑢 ⊔ 1_o)) → ∃𝑤 ∈ 2_o (inl‘∅) = (𝑓‘𝑤))
87	83, 85, 86	syl2anc 411	. . . . . . . . . . 11 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ∃𝑤 ∈ 2_o (inl‘∅) = (𝑓‘𝑤))
88		simplrr 536	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (𝑓‘𝑤))
89		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → 𝑤 = ∅)
90	89	fveq2d 5521	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘𝑤) = (𝑓‘∅))
91		simp-5r 544	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘∅) = (inr‘∅))
92	88, 90, 91	3eqtrd 2214	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (inl‘∅) = (inr‘∅))
93		simplrr 536	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1_o) → (inl‘∅) = (𝑓‘𝑤))
94		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1_o) → 𝑤 = 1_o)
95	94	fveq2d 5521	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1_o) → (𝑓‘𝑤) = (𝑓‘1_o))
96		simp-4r 542	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1_o) → (𝑓‘1_o) = (inr‘∅))
97	93, 95, 96	3eqtrd 2214	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1_o) → (inl‘∅) = (inr‘∅))
98		elpri 3617	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {∅, 1_o} → (𝑤 = ∅ ∨ 𝑤 = 1_o))
99	98, 74	eleq2s 2272	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 2_o → (𝑤 = ∅ ∨ 𝑤 = 1_o))
100	99	ad2antrl 490	. . . . . . . . . . . 12 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) → (𝑤 = ∅ ∨ 𝑤 = 1_o))
101	92, 97, 100	mpjaodan 798	. . . . . . . . . . 11 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2_o ∧ (inl‘∅) = (𝑓‘𝑤))) → (inl‘∅) = (inr‘∅))
102	87, 101	rexlimddv 2599	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) = (inr‘∅))
103		djune 7079	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
104	63, 63, 103	mp2an 426	. . . . . . . . . . . 12 ⊢ (inl‘∅) ≠ (inr‘∅)
105	104	neii 2349	. . . . . . . . . . 11 ⊢ ¬ (inl‘∅) = (inr‘∅)
106	105	a1i 9	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) ∧ ∅ ∈ 𝑢) → ¬ (inl‘∅) = (inr‘∅))
107	102, 106	pm2.65da 661	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) → ¬ ∅ ∈ 𝑢)
108	107	olcd 734	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
109	108, 68	sylibr 134	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) ∧ (𝑓‘1_o) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
110		simplr 528	. . . . . . . . . 10 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) → 𝑢 ⊆ {∅})
111	110, 13	sseqtrrdi 3206	. . . . . . . . 9 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) → 𝑢 ⊆ 1_o)
112	111	adantr 276	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) → 𝑢 ⊆ 1_o)
113	112, 77	exmidfodomrlemeldju 7200	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) → ((𝑓‘1_o) = (inl‘∅) ∨ (𝑓‘1_o) = (inr‘∅)))
114	82, 109, 113	mpjaodan 798	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) ∧ (𝑓‘∅) = (inr‘∅)) → DECID ∅ ∈ 𝑢)
115	111, 60	exmidfodomrlemeldju 7200	. . . . . 6 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) → ((𝑓‘∅) = (inl‘∅) ∨ (𝑓‘∅) = (inr‘∅)))
116	69, 114, 115	mpjaodan 798	. . . . 5 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2_o–onto→(𝑢 ⊔ 1_o)) → DECID ∅ ∈ 𝑢)
117	7, 8, 51, 116	exlimdd 1872	. . . 4 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → DECID ∅ ∈ 𝑢)
118	117	ex 115	. . 3 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → (𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
119	118	alrimiv 1874	. 2 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
120		df-exmid 4197	. 2 ⊢ (EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
121	119, 120	sylibr 134	1 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 708 DECID wdc 834 ∀wal 1351 = wceq 1353 ∃wex 1492 ∈ wcel 2148 ≠ wne 2347 ∃wrex 2456 Vcvv 2739 ⊆ wss 3131 ∅c0 3424 {csn 3594 {cpr 3595 class class class wbr 4005 EXMIDwem 4196 suc csuc 4367 ωcom 4591 ⟶wf 5214 –onto→wfo 5216 ‘cfv 5218 1_oc1o 6412 2_oc2o 6413 ≈ cen 6740 ≼ cdom 6741 ⊔ cdju 7038 inlcinl 7046 inrcinr 7047

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4120 ax-sep 4123 ax-nul 4131 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-iinf 4589

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-reu 2462 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-nul 3425 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-int 3847 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-tr 4104 df-exmid 4197 df-id 4295 df-iord 4368 df-on 4370 df-suc 4373 df-iom 4592 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-f1 5223 df-fo 5224 df-f1o 5225 df-fv 5226 df-1st 6143 df-2nd 6144 df-1o 6419 df-2o 6420 df-er 6537 df-en 6743 df-dom 6744 df-dju 7039 df-inl 7048 df-inr 7049 df-case 7085

This theorem is referenced by: exmidfodomr 7205

W3C validator