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 15666

Description: Lemma for exmidsbthr 15667. (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 7187	. . . . . . . . . 10 ⊢ ℕ_∞ ∈ V
3		fconstmpt 4710	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) = (𝑖 ∈ ω ↦ ∅)
4		0nninf 15648	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) ∈ ℕ_∞
5	3, 4	eqeltrri 2270	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω ↦ ∅) ∈ ℕ_∞
6	5	fconst6 5457	. . . . . . . . . . . . 13 ⊢ (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞
7	6	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞)
8		ssel 3177	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 ∈ {∅}))
9		elsni 3640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ {∅} → 𝑢 = ∅)
10	8, 9	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 = ∅))
11		ssel 3177	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 ∈ {∅}))
12		elsni 3640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {∅} → 𝑣 = ∅)
13	11, 12	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 = ∅))
14	10, 13	anim12d 335	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ {∅} → ((𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → (𝑢 = ∅ ∧ 𝑣 = ∅)))
15		eqtr3 2216	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = ∅ ∧ 𝑣 = ∅) → 𝑢 = 𝑣)
16	14, 15	syl6 33	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ⊆ {∅} → ((𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → 𝑢 = 𝑣))
17	16	imp 124	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ⊆ {∅} ∧ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) → 𝑢 = 𝑣)
18	17	a1d 22	. . . . . . . . . . . . 13 ⊢ ((𝑧 ⊆ {∅} ∧ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) → (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣))
19	18	ralrimivva 2579	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣))
20		dff13 5815	. . . . . . . . . . . 12 ⊢ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞ ↔ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞ ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣)))
21	7, 19, 20	sylanbrc 417	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞)
22		exmidsbthrlem.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = (𝑝 ∈ ℕ_∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))))
23	22	peano4nninf 15650	. . . . . . . . . . . 12 ⊢ 𝑆:ℕ_∞–1-1→ℕ_∞
24	23	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → 𝑆:ℕ_∞–1-1→ℕ_∞)
25		disj 3499	. . . . . . . . . . . . 13 ⊢ ((ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅ ↔ ∀𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ¬ 𝑎 ∈ ran 𝑆)
26	22	peano3nninf 15651	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅))
27		eqidd 2197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → ∅ = ∅)
28	27	cbvmptv 4129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ω ↦ ∅) = (𝑖 ∈ ω ↦ ∅)
29	28	neeq2i 2383	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅) ↔ (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
30	26, 29	sylib 122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
31	30	neneqd 2388	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ℕ_∞ → ¬ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
32	31	nrex 2589	. . . . . . . . . . . . . . . 16 ⊢ ¬ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅)
33		f1dm 5468	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:ℕ_∞–1-1→ℕ_∞ → dom 𝑆 = ℕ_∞)
34	23, 33	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ dom 𝑆 = ℕ_∞
35		eqcom 2198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏) ↔ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
36	34, 35	rexeqbii 2510	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏) ↔ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
37	32, 36	mtbir 672	. . . . . . . . . . . . . . 15 ⊢ ¬ ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)
38	22	funmpt2 5297	. . . . . . . . . . . . . . . 16 ⊢ Fun 𝑆
39		elrnrexdm 5701	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑆 → ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)))
40	38, 39	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏))
41	37, 40	mto 663	. . . . . . . . . . . . . 14 ⊢ ¬ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆
42		rnxpss 5101	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ⊆ {(𝑖 ∈ ω ↦ ∅)}
43	42	sseli 3179	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)})
44		elsni 3640	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)} → 𝑎 = (𝑖 ∈ ω ↦ ∅))
45	43, 44	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 = (𝑖 ∈ ω ↦ ∅))
46	45	eleq1d 2265	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → (𝑎 ∈ ran 𝑆 ↔ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆))
47	41, 46	mtbiri 676	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → ¬ 𝑎 ∈ ran 𝑆)
48	25, 47	mprgbir 2555	. . . . . . . . . . . 12 ⊢ (ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅
49	48	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅)
50	21, 24, 49	casef1 7156	. . . . . . . . . 10 ⊢ (𝑧 ⊆ {∅} → case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞)
51		f1domg 6817	. . . . . . . . . 10 ⊢ (ℕ_∞ ∈ V → (case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞ → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
52	2, 50, 51	mpsyl 65	. . . . . . . . 9 ⊢ (𝑧 ⊆ {∅} → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
53	52	adantl 277	. . . . . . . 8 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
54		inrresf1 7128	. . . . . . . . 9 ⊢ (inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞)
55		vex 2766	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
56		djuex 7109	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ V ∧ ℕ_∞ ∈ V) → (𝑧 ⊔ ℕ_∞) ∈ V)
57	55, 2, 56	mp2an 426	. . . . . . . . . 10 ⊢ (𝑧 ⊔ ℕ_∞) ∈ V
58	57	f1dom 6819	. . . . . . . . 9 ⊢ ((inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞) → ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))
59	54, 58	ax-mp 5	. . . . . . . 8 ⊢ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)
60	53, 59	jctir 313	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
61		breq12 4038	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≼ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
62		breq12 4038	. . . . . . . . . . . 12 ⊢ ((𝑦 = ℕ_∞ ∧ 𝑥 = (𝑧 ⊔ ℕ_∞)) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
63	62	ancoms 268	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
64	61, 63	anbi12d 473	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))))
65		breq12 4038	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≈ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞))
66	64, 65	imbi12d 234	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ↔ (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)))
67	66	spc2gv 2855	. . . . . . . 8 ⊢ (((𝑧 ⊔ ℕ_∞) ∈ V ∧ ℕ_∞ ∈ V) → (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)))
68	57, 2, 67	mp2an 426	. . . . . . 7 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞))
69	1, 60, 68	sylc 62	. . . . . 6 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)
70		bren 6806	. . . . . 6 ⊢ ((𝑧 ⊔ ℕ_∞) ≈ ℕ_∞ ↔ ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
71	69, 70	sylib 122	. . . . 5 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
72		nninfomni 15663	. . . . . . . . 9 ⊢ ℕ_∞ ∈ Omni
73	72	a1i 9	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ℕ_∞ ∈ Omni)
74		f1ocnv 5517	. . . . . . . . . 10 ⊢ (𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞ → ^◡𝑓:ℕ_∞–1-1-onto→(𝑧 ⊔ ℕ_∞))
75		f1ofo 5511	. . . . . . . . . 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 7215	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (∃𝑤 𝑤 ∈ 𝑧 ∨ 𝑧 = ∅))
79		sssnm 3784	. . . . . . . . . 10 ⊢ (∃𝑤 𝑤 ∈ 𝑧 → (𝑧 ⊆ {∅} ↔ 𝑧 = {∅}))
80	79	biimpcd 159	. . . . . . . . 9 ⊢ (𝑧 ⊆ {∅} → (∃𝑤 𝑤 ∈ 𝑧 → 𝑧 = {∅}))
81	80	ad2antlr 489	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (∃𝑤 𝑤 ∈ 𝑧 → 𝑧 = {∅}))
82	81	orim1d 788	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ((∃𝑤 𝑤 ∈ 𝑧 ∨ 𝑧 = ∅) → (𝑧 = {∅} ∨ 𝑧 = ∅)))
83	78, 82	mpd 13	. . . . . 6 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (𝑧 = {∅} ∨ 𝑧 = ∅))
84	83	orcomd 730	. . . . 5 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (𝑧 = ∅ ∨ 𝑧 = {∅}))
85	71, 84	exlimddv 1913	. . . 4 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 = ∅ ∨ 𝑧 = {∅}))
86	85	ex 115	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
87	86	alrimiv 1888	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
88		exmid01 4231	. 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 709 ∀wal 1362 = wceq 1364 ∃wex 1506 ∈ wcel 2167 ≠ wne 2367 ∀wral 2475 ∃wrex 2476 Vcvv 2763 ∩ cin 3156 ⊆ wss 3157 ∅c0 3450 ifcif 3561 {csn 3622 ∪ cuni 3839 class class class wbr 4033 ↦ cmpt 4094 EXMIDwem 4227 ωcom 4626 × cxp 4661 ^◡ccnv 4662 dom cdm 4663 ran crn 4664 ↾ cres 4665 Fun wfun 5252 ⟶wf 5254 –1-1→wf1 5255 –onto→wfo 5256 –1-1-onto→wf1o 5257 ‘cfv 5258 1_oc1o 6467 ≈ cen 6797 ≼ cdom 6798 ⊔ cdju 7103 inrcinr 7112 casecdjucase 7149 ℕ_∞xnninf 7185 Omnicomni 7200

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

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-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-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-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-1o 6474 df-2o 6475 df-map 6709 df-en 6800 df-dom 6801 df-dju 7104 df-inl 7113 df-inr 7114 df-case 7150 df-nninf 7186 df-omni 7201

This theorem is referenced by: exmidsbthr 15667

W3C validator