exmidsbthrlem - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > exmidsbthrlem		GIF version

Theorem exmidsbthrlem 17041

Description: Lemma for exmidsbthr 17042. (Contributed by Jim Kingdon, 11-Aug-2022.)

**Hypothesis**
Ref	Expression
exmidsbthrlem.s	⊢ 𝑆 = (𝑝 ∈ ℕ_∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))))

**Assertion**
Ref	Expression
exmidsbthrlem	⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID)

Distinct variable groups: 𝑆,𝑖 𝑖,𝑝 𝑥,𝑦 Allowed substitution hints: 𝑆(𝑥,𝑦,𝑝)

Proof of Theorem exmidsbthrlem Dummy variables 𝑎 𝑏 𝑘 𝑧 𝑓 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 109	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦))
2		nninfex 7455	. . . . . . . . . 10 ⊢ ℕ_∞ ∈ V
3		fconstmpt 4820	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) = (𝑖 ∈ ω ↦ ∅)
4		0nninf 17021	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) ∈ ℕ_∞
5	3, 4	eqeltrri 2312	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω ↦ ∅) ∈ ℕ_∞
6	5	fconst6 5590	. . . . . . . . . . . . 13 ⊢ (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞
7	6	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞)
8		ssel 3242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 ∈ {∅}))
9		elsni 3726	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ {∅} → 𝑢 = ∅)
10	8, 9	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 = ∅))
11		ssel 3242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 ∈ {∅}))
12		elsni 3726	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {∅} → 𝑣 = ∅)
13	11, 12	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 = ∅))
14	10, 13	anim12d 335	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ {∅} → ((𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → (𝑢 = ∅ ∧ 𝑣 = ∅)))
15		eqtr3 2258	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = ∅ ∧ 𝑣 = ∅) → 𝑢 = 𝑣)
16	14, 15	syl6 33	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ⊆ {∅} → ((𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → 𝑢 = 𝑣))
17	16	imp 124	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ⊆ {∅} ∧ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) → 𝑢 = 𝑣)
18	17	a1d 22	. . . . . . . . . . . . 13 ⊢ ((𝑧 ⊆ {∅} ∧ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) → (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣))
19	18	ralrimivva 2632	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣))
20		dff13 5968	. . . . . . . . . . . 12 ⊢ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞ ↔ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞ ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣)))
21	7, 19, 20	sylanbrc 421	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞)
22		exmidsbthrlem.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = (𝑝 ∈ ℕ_∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))))
23	22	peano4nninf 17023	. . . . . . . . . . . 12 ⊢ 𝑆:ℕ_∞–1-1→ℕ_∞
24	23	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → 𝑆:ℕ_∞–1-1→ℕ_∞)
25		disj 3573	. . . . . . . . . . . . 13 ⊢ ((ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅ ↔ ∀𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ¬ 𝑎 ∈ ran 𝑆)
26	22	peano3nninf 17024	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅))
27		eqidd 2239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → ∅ = ∅)
28	27	cbvmptv 4225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ω ↦ ∅) = (𝑖 ∈ ω ↦ ∅)
29	28	neeq2i 2436	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅) ↔ (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
30	26, 29	sylib 122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
31	30	neneqd 2441	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ℕ_∞ → ¬ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
32	31	nrex 2642	. . . . . . . . . . . . . . . 16 ⊢ ¬ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅)
33		f1dm 5601	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:ℕ_∞–1-1→ℕ_∞ → dom 𝑆 = ℕ_∞)
34	23, 33	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ dom 𝑆 = ℕ_∞
35		eqcom 2240	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏) ↔ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
36	34, 35	rexeqbii 2563	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏) ↔ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
37	32, 36	mtbir 682	. . . . . . . . . . . . . . 15 ⊢ ¬ ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)
38	22	funmpt2 5414	. . . . . . . . . . . . . . . 16 ⊢ Fun 𝑆
39		elrnrexdm 5841	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑆 → ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)))
40	38, 39	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏))
41	37, 40	mto 672	. . . . . . . . . . . . . 14 ⊢ ¬ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆
42		rnxpss 5217	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ⊆ {(𝑖 ∈ ω ↦ ∅)}
43	42	sseli 3244	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)})
44		elsni 3726	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)} → 𝑎 = (𝑖 ∈ ω ↦ ∅))
45	43, 44	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 = (𝑖 ∈ ω ↦ ∅))
46	45	eleq1d 2307	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → (𝑎 ∈ ran 𝑆 ↔ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆))
47	41, 46	mtbiri 686	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → ¬ 𝑎 ∈ ran 𝑆)
48	25, 47	mprgbir 2608	. . . . . . . . . . . 12 ⊢ (ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅
49	48	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅)
50	21, 24, 49	casef1 7424	. . . . . . . . . 10 ⊢ (𝑧 ⊆ {∅} → case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞)
51		f1domg 7038	. . . . . . . . . 10 ⊢ (ℕ_∞ ∈ V → (case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞ → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
52	2, 50, 51	mpsyl 65	. . . . . . . . 9 ⊢ (𝑧 ⊆ {∅} → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
53	52	adantl 277	. . . . . . . 8 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
54		inrresf1 7396	. . . . . . . . 9 ⊢ (inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞)
55		vex 2824	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
56		djuex 7377	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ V ∧ ℕ_∞ ∈ V) → (𝑧 ⊔ ℕ_∞) ∈ V)
57	55, 2, 56	mp2an 430	. . . . . . . . . 10 ⊢ (𝑧 ⊔ ℕ_∞) ∈ V
58	57	f1dom 7040	. . . . . . . . 9 ⊢ ((inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞) → ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))
59	54, 58	ax-mp 5	. . . . . . . 8 ⊢ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)
60	53, 59	jctir 313	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
61		breq12 4133	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≼ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
62		breq12 4133	. . . . . . . . . . . 12 ⊢ ((𝑦 = ℕ_∞ ∧ 𝑥 = (𝑧 ⊔ ℕ_∞)) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
63	62	ancoms 268	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
64	61, 63	anbi12d 477	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))))
65		breq12 4133	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≈ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞))
66	64, 65	imbi12d 234	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ↔ (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)))
67	66	spc2gv 2916	. . . . . . . 8 ⊢ (((𝑧 ⊔ ℕ_∞) ∈ V ∧ ℕ_∞ ∈ V) → (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)))
68	57, 2, 67	mp2an 430	. . . . . . 7 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞))
69	1, 60, 68	sylc 62	. . . . . 6 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)
70		bren 7024	. . . . . 6 ⊢ ((𝑧 ⊔ ℕ_∞) ≈ ℕ_∞ ↔ ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
71	69, 70	sylib 122	. . . . 5 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
72		nninfomni 17036	. . . . . . . . 9 ⊢ ℕ_∞ ∈ Omni
73	72	a1i 9	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ℕ_∞ ∈ Omni)
74		f1ocnv 5650	. . . . . . . . . 10 ⊢ (𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞ → ^◡𝑓:ℕ_∞–1-1-onto→(𝑧 ⊔ ℕ_∞))
75		f1ofo 5644	. . . . . . . . . 10 ⊢ (^◡𝑓:ℕ_∞–1-1-onto→(𝑧 ⊔ ℕ_∞) → ^◡𝑓:ℕ_∞–onto→(𝑧 ⊔ ℕ_∞))
76	74, 75	syl 14	. . . . . . . . 9 ⊢ (𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞ → ^◡𝑓:ℕ_∞–onto→(𝑧 ⊔ ℕ_∞))
77	76	adantl 277	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ^◡𝑓:ℕ_∞–onto→(𝑧 ⊔ ℕ_∞))
78	73, 77	fodjuomni 7483	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (∃𝑤 𝑤 ∈ 𝑧 ∨ 𝑧 = ∅))
79		sssnm 3877	. . . . . . . . . 10 ⊢ (∃𝑤 𝑤 ∈ 𝑧 → (𝑧 ⊆ {∅} ↔ 𝑧 = {∅}))
80	79	biimpcd 159	. . . . . . . . 9 ⊢ (𝑧 ⊆ {∅} → (∃𝑤 𝑤 ∈ 𝑧 → 𝑧 = {∅}))
81	80	ad2antlr 493	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (∃𝑤 𝑤 ∈ 𝑧 → 𝑧 = {∅}))
82	81	orim1d 799	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ((∃𝑤 𝑤 ∈ 𝑧 ∨ 𝑧 = ∅) → (𝑧 = {∅} ∨ 𝑧 = ∅)))
83	78, 82	mpd 13	. . . . . 6 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (𝑧 = {∅} ∨ 𝑧 = ∅))
84	83	orcomd 741	. . . . 5 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (𝑧 = ∅ ∨ 𝑧 = {∅}))
85	71, 84	exlimddv 1954	. . . 4 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 = ∅ ∨ 𝑧 = {∅}))
86	85	ex 115	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
87	86	alrimiv 1927	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
88		exmid01 4333	. 2 ⊢ (EXMID ↔ ∀𝑧(𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
89	87, 88	sylibr 134	1 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 ∀wal 1400 = wceq 1402 ∃wex 1545 ∈ wcel 2209 ≠ wne 2420 ∀wral 2528 ∃wrex 2529 Vcvv 2821 ∩ cin 3219 ⊆ wss 3220 ∅c0 3520 ifcif 3638 {csn 3708 ∪ cuni 3933 class class class wbr 4128 ↦ cmpt 4190 EXMIDwem 4329 ωcom 4735 × cxp 4770 ^◡ccnv 4771 dom cdm 4772 ran crn 4773 ↾ cres 4774 Fun wfun 5369 ⟶wf 5371 –1-1→wf1 5372 –onto→wfo 5373 –1-1-onto→wf1o 5374 ‘cfv 5375 1_oc1o 6674 ≈ cen 7014 ≼ cdom 7015 ⊔ cdju 7371 inrcinr 7380 casecdjucase 7417 ℕ_∞xnninf 7453 Omnicomni 7468

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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-13 2211 ax-14 2212 ax-ext 2220 ax-coll 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733

This theorem depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-exmid 4330 df-id 4436 df-iord 4509 df-on 4511 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-ov 6082 df-oprab 6083 df-mpo 6084 df-1st 6368 df-2nd 6369 df-1o 6681 df-2o 6682 df-map 6918 df-en 7017 df-dom 7018 df-dju 7372 df-inl 7381 df-inr 7382 df-case 7418 df-nninf 7454 df-omni 7469

This theorem is referenced by: exmidsbthr 17042

W3C validator