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 17238

Description: Lemma for exmidsbthr 17239. (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 7462	. . . . . . . . . 10 ⊢ ℕ_∞ ∈ V
3		fconstmpt 4822	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) = (𝑖 ∈ ω ↦ ∅)
4		0nninf 17218	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) ∈ ℕ_∞
5	3, 4	eqeltrri 2312	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω ↦ ∅) ∈ ℕ_∞
6	5	fconst6 5592	. . . . . . . . . . . . 13 ⊢ (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞
7	6	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞)
8		ssel 3242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 ∈ {∅}))
9		elsni 3727	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ {∅} → 𝑢 = ∅)
10	8, 9	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 = ∅))
11		ssel 3242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 ∈ {∅}))
12		elsni 3727	. . . . . . . . . . . . . . . . . 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 5974	. . . . . . . . . . . 12 ⊢ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞ ↔ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞ ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣)))
21	7, 19, 20	sylanbrc 421	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞)
22		exmidsbthrlem.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = (𝑝 ∈ ℕ_∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))))
23	22	peano4nninf 17220	. . . . . . . . . . . 12 ⊢ 𝑆:ℕ_∞–1-1→ℕ_∞
24	23	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → 𝑆:ℕ_∞–1-1→ℕ_∞)
25		disj 3573	. . . . . . . . . . . . 13 ⊢ ((ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅ ↔ ∀𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ¬ 𝑎 ∈ ran 𝑆)
26	22	peano3nninf 17221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅))
27		eqidd 2239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → ∅ = ∅)
28	27	cbvmptv 4227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ω ↦ ∅) = (𝑖 ∈ ω ↦ ∅)
29	28	neeq2i 2436	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅) ↔ (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
30	26, 29	sylib 122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
31	30	neneqd 2441	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ℕ_∞ → ¬ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
32	31	nrex 2642	. . . . . . . . . . . . . . . 16 ⊢ ¬ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅)
33		f1dm 5603	. . . . . . . . . . . . . . . . . 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 5416	. . . . . . . . . . . . . . . 16 ⊢ Fun 𝑆
39		elrnrexdm 5847	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑆 → ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)))
40	38, 39	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏))
41	37, 40	mto 672	. . . . . . . . . . . . . 14 ⊢ ¬ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆
42		rnxpss 5219	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ⊆ {(𝑖 ∈ ω ↦ ∅)}
43	42	sseli 3244	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)})
44		elsni 3727	. . . . . . . . . . . . . . . 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 7431	. . . . . . . . . 10 ⊢ (𝑧 ⊆ {∅} → case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞)
51		f1domg 7044	. . . . . . . . . 10 ⊢ (ℕ_∞ ∈ V → (case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞ → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
52	2, 50, 51	mpsyl 65	. . . . . . . . 9 ⊢ (𝑧 ⊆ {∅} → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
53	52	adantl 277	. . . . . . . 8 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
54		inrresf1 7403	. . . . . . . . 9 ⊢ (inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞)
55		vex 2824	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
56		djuex 7384	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ V ∧ ℕ_∞ ∈ V) → (𝑧 ⊔ ℕ_∞) ∈ V)
57	55, 2, 56	mp2an 430	. . . . . . . . . 10 ⊢ (𝑧 ⊔ ℕ_∞) ∈ V
58	57	f1dom 7046	. . . . . . . . 9 ⊢ ((inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞) → ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))
59	54, 58	ax-mp 5	. . . . . . . 8 ⊢ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)
60	53, 59	jctir 313	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
61		breq12 4135	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≼ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
62		breq12 4135	. . . . . . . . . . . 12 ⊢ ((𝑦 = ℕ_∞ ∧ 𝑥 = (𝑧 ⊔ ℕ_∞)) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
63	62	ancoms 268	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
64	61, 63	anbi12d 477	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))))
65		breq12 4135	. . . . . . . . . 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 7030	. . . . . 6 ⊢ ((𝑧 ⊔ ℕ_∞) ≈ ℕ_∞ ↔ ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
71	69, 70	sylib 122	. . . . 5 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
72		nninfomni 17233	. . . . . . . . 9 ⊢ ℕ_∞ ∈ Omni
73	72	a1i 9	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ℕ_∞ ∈ Omni)
74		f1ocnv 5652	. . . . . . . . . 10 ⊢ (𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞ → ^◡𝑓:ℕ_∞–1-1-onto→(𝑧 ⊔ ℕ_∞))
75		f1ofo 5646	. . . . . . . . . 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 7490	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (∃𝑤 𝑤 ∈ 𝑧 ∨ 𝑧 = ∅))
79		sssnm 3879	. . . . . . . . . 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 4335	. 2 ⊢ (EXMID ↔ ∀𝑧(𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
89	87, 88	sylibr 134	1 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID)

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ 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 3709 ∪ cuni 3935 class class class wbr 4130 ↦ cmpt 4192 EXMIDwem 4331 ωcom 4737 × cxp 4772 ^◡ccnv 4773 dom cdm 4774 ran crn 4775 ↾ cres 4776 Fun wfun 5371 ⟶wf 5373 –1-1→wf1 5374 –onto→wfo 5375 –1-1-onto→wf1o 5376 ‘cfv 5377 1_oc1o 6680 ≈ cen 7020 ≼ cdom 7021 ⊔ cdju 7378 inrcinr 7387 casecdjucase 7424 ℕ_∞xnninf 7460 Omnicomni 7475

This proof depends on 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 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735

This proof 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 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-exmid 4332 df-id 4438 df-iord 4511 df-on 4513 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-1o 6687 df-2o 6688 df-map 6924 df-en 7023 df-dom 7024 df-dju 7379 df-inl 7388 df-inr 7389 df-case 7425 df-nninf 7461 df-omni 7476

This theorem is used by: exmidsbthr 17239

W3C validator