Theorem exmidunben 12643

Description: If any unbounded set of positive integers is equinumerous to ℕ, then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.)

Assertion

Ref	Expression
exmidunben	⊢ ((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) → EXMID)

Distinct variable group:   𝑚,𝑛,𝑥

Proof of Theorem exmidunben

Dummy variables 𝑓 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2766	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
2	1	enref 6824	. . . . . . . . . 10 ⊢ 𝑦 ≈ 𝑦
3		2z 9354	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
4		uzennn 10528	. . . . . . . . . . 11 ⊢ (2 ∈ ℤ → (ℤ≥‘2) ≈ ℕ)
5	3, 4	ax-mp 5	. . . . . . . . . 10 ⊢ (ℤ≥‘2) ≈ ℕ
6		djuen 7278	. . . . . . . . . 10 ⊢ ((𝑦 ≈ 𝑦 ∧ (ℤ≥‘2) ≈ ℕ) → (𝑦 ⊔ (ℤ≥‘2)) ≈ (𝑦 ⊔ ℕ))
7	2, 5, 6	mp2an 426	. . . . . . . . 9 ⊢ (𝑦 ⊔ (ℤ≥‘2)) ≈ (𝑦 ⊔ ℕ)
8	7	ensymi 6841	. . . . . . . 8 ⊢ (𝑦 ⊔ ℕ) ≈ (𝑦 ⊔ (ℤ≥‘2))
9		zex 9335	. . . . . . . . . . 11 ⊢ ℤ ∈ V
10		uzssz 9621	. . . . . . . . . . 11 ⊢ (ℤ≥‘2) ⊆ ℤ
11	9, 10	ssexi 4171	. . . . . . . . . 10 ⊢ (ℤ≥‘2) ∈ V
12		1re 8025	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
13	12	ltnri 8119	. . . . . . . . . . . . . 14 ⊢ ¬ 1 < 1
14		simplr 528	. . . . . . . . . . . . . . . . 17 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑧 ∈ 𝑦) → 𝑦 ⊆ {1})
15		simpr 110	. . . . . . . . . . . . . . . . 17 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝑦)
16	14, 15	sseldd 3184	. . . . . . . . . . . . . . . 16 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ {1})
17		elsni 3640	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {1} → 𝑧 = 1)
18	16, 17	syl 14	. . . . . . . . . . . . . . 15 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑧 ∈ 𝑦) → 𝑧 = 1)
19	18	breq2d 4045	. . . . . . . . . . . . . 14 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑧 ∈ 𝑦) → (1 < 𝑧 ↔ 1 < 1))
20	13, 19	mtbiri 676	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑧 ∈ 𝑦) → ¬ 1 < 𝑧)
21		eluz2gt1 9676	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (ℤ≥‘2) → 1 < 𝑧)
22	20, 21	nsyl 629	. . . . . . . . . . . 12 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑧 ∈ 𝑦) → ¬ 𝑧 ∈ (ℤ≥‘2))
23	22	ralrimiva 2570	. . . . . . . . . . 11 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → ∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ (ℤ≥‘2))
24		disj 3499	. . . . . . . . . . 11 ⊢ ((𝑦 ∩ (ℤ≥‘2)) = ∅ ↔ ∀𝑧 ∈ 𝑦 ¬ 𝑧 ∈ (ℤ≥‘2))
25	23, 24	sylibr 134	. . . . . . . . . 10 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (𝑦 ∩ (ℤ≥‘2)) = ∅)
26		endjudisj 7277	. . . . . . . . . 10 ⊢ ((𝑦 ∈ V ∧ (ℤ≥‘2) ∈ V ∧ (𝑦 ∩ (ℤ≥‘2)) = ∅) → (𝑦 ⊔ (ℤ≥‘2)) ≈ (𝑦 ∪ (ℤ≥‘2)))
27	1, 11, 25, 26	mp3an12i 1352	. . . . . . . . 9 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (𝑦 ⊔ (ℤ≥‘2)) ≈ (𝑦 ∪ (ℤ≥‘2)))
28		simpr 110	. . . . . . . . . . . 12 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → 𝑦 ⊆ {1})
29		1nn 9001	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
30		snssi 3766	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
31	29, 30	ax-mp 5	. . . . . . . . . . . 12 ⊢ {1} ⊆ ℕ
32	28, 31	sstrdi 3195	. . . . . . . . . . 11 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → 𝑦 ⊆ ℕ)
33		2nn 9152	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
34		uznnssnn 9651	. . . . . . . . . . . 12 ⊢ (2 ∈ ℕ → (ℤ≥‘2) ⊆ ℕ)
35	33, 34	mp1i 10	. . . . . . . . . . 11 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (ℤ≥‘2) ⊆ ℕ)
36	32, 35	unssd 3339	. . . . . . . . . 10 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (𝑦 ∪ (ℤ≥‘2)) ⊆ ℕ)
37		nfv 1542	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑚 𝑥 ⊆ ℕ
38		nfra1 2528	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑚∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛
39	37, 38	nfan 1579	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑚(𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛)
40		nfv 1542	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑚 𝑥 ≈ ℕ
41	39, 40	nfim 1586	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑚((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ)
42	41	nfal 1590	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑚∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ)
43		nfv 1542	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑚ω ∈ Omni
44	42, 43	nfan 1579	. . . . . . . . . . . 12 ⊢ Ⅎ𝑚(∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni)
45		nfv 1542	. . . . . . . . . . . 12 ⊢ Ⅎ𝑚 𝑦 ⊆ {1}
46	44, 45	nfan 1579	. . . . . . . . . . 11 ⊢ Ⅎ𝑚((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1})
47		simpr 110	. . . . . . . . . . . . . . . . 17 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
48	47	peano2nnd 9005	. . . . . . . . . . . . . . . 16 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ)
49	48	nnzd 9447	. . . . . . . . . . . . . . 15 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℤ)
50		0p1e1 9104	. . . . . . . . . . . . . . . . 17 ⊢ (0 + 1) = 1
51		0red 8027	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 0 ∈ ℝ)
52		nnre 8997	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
53		1red 8041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 1 ∈ ℝ)
54		nngt0 9015	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 0 < 𝑚)
55	51, 52, 53, 54	ltadd1dd 8583	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ → (0 + 1) < (𝑚 + 1))
56	50, 55	eqbrtrrid 4069	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → 1 < (𝑚 + 1))
57	56	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → 1 < (𝑚 + 1))
58		eluz2b1 9675	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘2) ↔ ((𝑚 + 1) ∈ ℤ ∧ 1 < (𝑚 + 1)))
59	49, 57, 58	sylanbrc 417	. . . . . . . . . . . . . 14 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ (ℤ≥‘2))
60		elun2 3331	. . . . . . . . . . . . . 14 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘2) → (𝑚 + 1) ∈ (𝑦 ∪ (ℤ≥‘2)))
61	59, 60	syl 14	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ (𝑦 ∪ (ℤ≥‘2)))
62	47	nnred 9003	. . . . . . . . . . . . . 14 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
63	62	ltp1d 8957	. . . . . . . . . . . . 13 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → 𝑚 < (𝑚 + 1))
64		breq2 4037	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑚 + 1) → (𝑚 < 𝑛 ↔ 𝑚 < (𝑚 + 1)))
65	64	rspcev 2868	. . . . . . . . . . . . 13 ⊢ (((𝑚 + 1) ∈ (𝑦 ∪ (ℤ≥‘2)) ∧ 𝑚 < (𝑚 + 1)) → ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛)
66	61, 63, 65	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑚 ∈ ℕ) → ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛)
67	66	ex 115	. . . . . . . . . . 11 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (𝑚 ∈ ℕ → ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛))
68	46, 67	ralrimi 2568	. . . . . . . . . 10 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛)
69	1, 11	unex 4476	. . . . . . . . . . . 12 ⊢ (𝑦 ∪ (ℤ≥‘2)) ∈ V
70		sseq1 3206	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2)) → (𝑥 ⊆ ℕ ↔ (𝑦 ∪ (ℤ≥‘2)) ⊆ ℕ))
71		rexeq 2694	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2)) → (∃𝑛 ∈ 𝑥 𝑚 < 𝑛 ↔ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛))
72	71	ralbidv 2497	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2)) → (∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛 ↔ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛))
73	70, 72	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2)) → ((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) ↔ ((𝑦 ∪ (ℤ≥‘2)) ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛)))
74		breq1 4036	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2)) → (𝑥 ≈ ℕ ↔ (𝑦 ∪ (ℤ≥‘2)) ≈ ℕ))
75	73, 74	imbi12d 234	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 ∪ (ℤ≥‘2)) → (((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ↔ (((𝑦 ∪ (ℤ≥‘2)) ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛) → (𝑦 ∪ (ℤ≥‘2)) ≈ ℕ)))
76	69, 75	spcv 2858	. . . . . . . . . . 11 ⊢ (∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) → (((𝑦 ∪ (ℤ≥‘2)) ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛) → (𝑦 ∪ (ℤ≥‘2)) ≈ ℕ))
77	76	ad2antrr 488	. . . . . . . . . 10 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (((𝑦 ∪ (ℤ≥‘2)) ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ (𝑦 ∪ (ℤ≥‘2))𝑚 < 𝑛) → (𝑦 ∪ (ℤ≥‘2)) ≈ ℕ))
78	36, 68, 77	mp2and 433	. . . . . . . . 9 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (𝑦 ∪ (ℤ≥‘2)) ≈ ℕ)
79		entr 6843	. . . . . . . . 9 ⊢ (((𝑦 ⊔ (ℤ≥‘2)) ≈ (𝑦 ∪ (ℤ≥‘2)) ∧ (𝑦 ∪ (ℤ≥‘2)) ≈ ℕ) → (𝑦 ⊔ (ℤ≥‘2)) ≈ ℕ)
80	27, 78, 79	syl2anc 411	. . . . . . . 8 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (𝑦 ⊔ (ℤ≥‘2)) ≈ ℕ)
81		entr 6843	. . . . . . . 8 ⊢ (((𝑦 ⊔ ℕ) ≈ (𝑦 ⊔ (ℤ≥‘2)) ∧ (𝑦 ⊔ (ℤ≥‘2)) ≈ ℕ) → (𝑦 ⊔ ℕ) ≈ ℕ)
82	8, 80, 81	sylancr 414	. . . . . . 7 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (𝑦 ⊔ ℕ) ≈ ℕ)
83	82	ensymd 6842	. . . . . 6 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → ℕ ≈ (𝑦 ⊔ ℕ))
84		bren 6806	. . . . . 6 ⊢ (ℕ ≈ (𝑦 ⊔ ℕ) ↔ ∃𝑓 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ))
85	83, 84	sylib 122	. . . . 5 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → ∃𝑓 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ))
86		simpllr 534	. . . . . . . . 9 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → ω ∈ Omni)
87		nnenom 10526	. . . . . . . . . 10 ⊢ ℕ ≈ ω
88		enomni 7205	. . . . . . . . . 10 ⊢ (ℕ ≈ ω → (ℕ ∈ Omni ↔ ω ∈ Omni))
89	87, 88	ax-mp 5	. . . . . . . . 9 ⊢ (ℕ ∈ Omni ↔ ω ∈ Omni)
90	86, 89	sylibr 134	. . . . . . . 8 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → ℕ ∈ Omni)
91		f1ofo 5511	. . . . . . . . 9 ⊢ (𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ) → 𝑓:ℕ–onto→(𝑦 ⊔ ℕ))
92	91	adantl 277	. . . . . . . 8 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → 𝑓:ℕ–onto→(𝑦 ⊔ ℕ))
93	90, 92	fodjuomni 7215	. . . . . . 7 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → (∃𝑤 𝑤 ∈ 𝑦 ∨ 𝑦 = ∅))
94	93	orcomd 730	. . . . . 6 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → (𝑦 = ∅ ∨ ∃𝑤 𝑤 ∈ 𝑦))
95		simplr 528	. . . . . . . 8 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → 𝑦 ⊆ {1})
96		sssnm 3784	. . . . . . . 8 ⊢ (∃𝑤 𝑤 ∈ 𝑦 → (𝑦 ⊆ {1} ↔ 𝑦 = {1}))
97	95, 96	syl5ibcom 155	. . . . . . 7 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → (∃𝑤 𝑤 ∈ 𝑦 → 𝑦 = {1}))
98	97	orim2d 789	. . . . . 6 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → ((𝑦 = ∅ ∨ ∃𝑤 𝑤 ∈ 𝑦) → (𝑦 = ∅ ∨ 𝑦 = {1})))
99	94, 98	mpd 13	. . . . 5 ⊢ ((((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) ∧ 𝑓:ℕ–1-1-onto→(𝑦 ⊔ ℕ)) → (𝑦 = ∅ ∨ 𝑦 = {1}))
100	85, 99	exlimddv 1913	. . . 4 ⊢ (((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) ∧ 𝑦 ⊆ {1}) → (𝑦 = ∅ ∨ 𝑦 = {1}))
101	100	ex 115	. . 3 ⊢ ((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) → (𝑦 ⊆ {1} → (𝑦 = ∅ ∨ 𝑦 = {1})))
102	101	alrimiv 1888	. 2 ⊢ ((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) → ∀𝑦(𝑦 ⊆ {1} → (𝑦 = ∅ ∨ 𝑦 = {1})))
103		exmidsssnc 4236	. . 3 ⊢ (1 ∈ ℕ → (EXMID ↔ ∀𝑦(𝑦 ⊆ {1} → (𝑦 = ∅ ∨ 𝑦 = {1}))))
104	29, 103	ax-mp 5	. 2 ⊢ (EXMID ↔ ∀𝑦(𝑦 ⊆ {1} → (𝑦 = ∅ ∨ 𝑦 = {1})))
105	102, 104	sylibr 134	1 ⊢ ((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) → EXMID)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  ∀wal 1362   = wceq 1364  ∃wex 1506   ∈ wcel 2167  ∀wral 2475  ∃wrex 2476  Vcvv 2763   ∪ cun 3155   ∩ cin 3156   ⊆ wss 3157  ∅c0 3450  {csn 3622   class class class wbr 4033  EXMIDwem 4227  ωcom 4626  –onto→wfo 5256  –1-1-onto→wf1o 5257  ‘cfv 5258  (class class class)co 5922   ≈ cen 6797   ⊔ cdju 7103  Omnicomni 7200  0cc0 7879  1c1 7880   + caddc 7882   < clt 8061  ℕcn 8990  2c2 9041  ℤcz 9326  ℤ_≥cuz 9601

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-addcom 7979  ax-addass 7981  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-0id 7987  ax-rnegex 7988  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-ltadd 7995

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 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-exmid 4228  df-id 4328  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-recs 6363  df-frec 6449  df-1o 6474  df-2o 6475  df-er 6592  df-map 6709  df-en 6800  df-dju 7104  df-inl 7113  df-inr 7114  df-omni 7201  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-inn 8991  df-2 9049  df-n0 9250  df-z 9327  df-uz 9602

This theorem is referenced by: (None)