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 14773

Description: Lemma for exmidsbthr 14774. (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 7120	. . . . . . . . . 10 ⊢ ℕ_∞ ∈ V
3		fconstmpt 4674	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) = (𝑖 ∈ ω ↦ ∅)
4		0nninf 14756	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) ∈ ℕ_∞
5	3, 4	eqeltrri 2251	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω ↦ ∅) ∈ ℕ_∞
6	5	fconst6 5416	. . . . . . . . . . . . 13 ⊢ (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞
7	6	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞)
8		ssel 3150	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 ∈ {∅}))
9		elsni 3611	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ {∅} → 𝑢 = ∅)
10	8, 9	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 = ∅))
11		ssel 3150	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 ∈ {∅}))
12		elsni 3611	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {∅} → 𝑣 = ∅)
13	11, 12	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 = ∅))
14	10, 13	anim12d 335	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ {∅} → ((𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → (𝑢 = ∅ ∧ 𝑣 = ∅)))
15		eqtr3 2197	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = ∅ ∧ 𝑣 = ∅) → 𝑢 = 𝑣)
16	14, 15	syl6 33	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ⊆ {∅} → ((𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → 𝑢 = 𝑣))
17	16	imp 124	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ⊆ {∅} ∧ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) → 𝑢 = 𝑣)
18	17	a1d 22	. . . . . . . . . . . . 13 ⊢ ((𝑧 ⊆ {∅} ∧ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) → (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣))
19	18	ralrimivva 2559	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣))
20		dff13 5769	. . . . . . . . . . . 12 ⊢ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞ ↔ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞ ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣)))
21	7, 19, 20	sylanbrc 417	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞)
22		exmidsbthrlem.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = (𝑝 ∈ ℕ_∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))))
23	22	peano4nninf 14758	. . . . . . . . . . . 12 ⊢ 𝑆:ℕ_∞–1-1→ℕ_∞
24	23	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → 𝑆:ℕ_∞–1-1→ℕ_∞)
25		disj 3472	. . . . . . . . . . . . 13 ⊢ ((ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅ ↔ ∀𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ¬ 𝑎 ∈ ran 𝑆)
26	22	peano3nninf 14759	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅))
27		eqidd 2178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → ∅ = ∅)
28	27	cbvmptv 4100	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ω ↦ ∅) = (𝑖 ∈ ω ↦ ∅)
29	28	neeq2i 2363	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅) ↔ (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
30	26, 29	sylib 122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
31	30	neneqd 2368	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ℕ_∞ → ¬ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
32	31	nrex 2569	. . . . . . . . . . . . . . . 16 ⊢ ¬ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅)
33		f1dm 5427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:ℕ_∞–1-1→ℕ_∞ → dom 𝑆 = ℕ_∞)
34	23, 33	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ dom 𝑆 = ℕ_∞
35		eqcom 2179	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏) ↔ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
36	34, 35	rexeqbii 2490	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏) ↔ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
37	32, 36	mtbir 671	. . . . . . . . . . . . . . 15 ⊢ ¬ ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)
38	22	funmpt2 5256	. . . . . . . . . . . . . . . 16 ⊢ Fun 𝑆
39		elrnrexdm 5656	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑆 → ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)))
40	38, 39	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏))
41	37, 40	mto 662	. . . . . . . . . . . . . 14 ⊢ ¬ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆
42		rnxpss 5061	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ⊆ {(𝑖 ∈ ω ↦ ∅)}
43	42	sseli 3152	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)})
44		elsni 3611	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)} → 𝑎 = (𝑖 ∈ ω ↦ ∅))
45	43, 44	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 = (𝑖 ∈ ω ↦ ∅))
46	45	eleq1d 2246	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → (𝑎 ∈ ran 𝑆 ↔ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆))
47	41, 46	mtbiri 675	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → ¬ 𝑎 ∈ ran 𝑆)
48	25, 47	mprgbir 2535	. . . . . . . . . . . 12 ⊢ (ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅
49	48	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅)
50	21, 24, 49	casef1 7089	. . . . . . . . . 10 ⊢ (𝑧 ⊆ {∅} → case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞)
51		f1domg 6758	. . . . . . . . . 10 ⊢ (ℕ_∞ ∈ V → (case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞ → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
52	2, 50, 51	mpsyl 65	. . . . . . . . 9 ⊢ (𝑧 ⊆ {∅} → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
53	52	adantl 277	. . . . . . . 8 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
54		inrresf1 7061	. . . . . . . . 9 ⊢ (inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞)
55		vex 2741	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
56		djuex 7042	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ V ∧ ℕ_∞ ∈ V) → (𝑧 ⊔ ℕ_∞) ∈ V)
57	55, 2, 56	mp2an 426	. . . . . . . . . 10 ⊢ (𝑧 ⊔ ℕ_∞) ∈ V
58	57	f1dom 6760	. . . . . . . . 9 ⊢ ((inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞) → ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))
59	54, 58	ax-mp 5	. . . . . . . 8 ⊢ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)
60	53, 59	jctir 313	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
61		breq12 4009	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≼ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
62		breq12 4009	. . . . . . . . . . . 12 ⊢ ((𝑦 = ℕ_∞ ∧ 𝑥 = (𝑧 ⊔ ℕ_∞)) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
63	62	ancoms 268	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
64	61, 63	anbi12d 473	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))))
65		breq12 4009	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≈ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞))
66	64, 65	imbi12d 234	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ↔ (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)))
67	66	spc2gv 2829	. . . . . . . 8 ⊢ (((𝑧 ⊔ ℕ_∞) ∈ V ∧ ℕ_∞ ∈ V) → (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)))
68	57, 2, 67	mp2an 426	. . . . . . 7 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞))
69	1, 60, 68	sylc 62	. . . . . 6 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)
70		bren 6747	. . . . . 6 ⊢ ((𝑧 ⊔ ℕ_∞) ≈ ℕ_∞ ↔ ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
71	69, 70	sylib 122	. . . . 5 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
72		nninfomni 14771	. . . . . . . . 9 ⊢ ℕ_∞ ∈ Omni
73	72	a1i 9	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ℕ_∞ ∈ Omni)
74		f1ocnv 5475	. . . . . . . . . 10 ⊢ (𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞ → ^◡𝑓:ℕ_∞–1-1-onto→(𝑧 ⊔ ℕ_∞))
75		f1ofo 5469	. . . . . . . . . 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 7147	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (∃𝑤 𝑤 ∈ 𝑧 ∨ 𝑧 = ∅))
79		sssnm 3755	. . . . . . . . . 10 ⊢ (∃𝑤 𝑤 ∈ 𝑧 → (𝑧 ⊆ {∅} ↔ 𝑧 = {∅}))
80	79	biimpcd 159	. . . . . . . . 9 ⊢ (𝑧 ⊆ {∅} → (∃𝑤 𝑤 ∈ 𝑧 → 𝑧 = {∅}))
81	80	ad2antlr 489	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (∃𝑤 𝑤 ∈ 𝑧 → 𝑧 = {∅}))
82	81	orim1d 787	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ((∃𝑤 𝑤 ∈ 𝑧 ∨ 𝑧 = ∅) → (𝑧 = {∅} ∨ 𝑧 = ∅)))
83	78, 82	mpd 13	. . . . . 6 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (𝑧 = {∅} ∨ 𝑧 = ∅))
84	83	orcomd 729	. . . . 5 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (𝑧 = ∅ ∨ 𝑧 = {∅}))
85	71, 84	exlimddv 1898	. . . 4 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 = ∅ ∨ 𝑧 = {∅}))
86	85	ex 115	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
87	86	alrimiv 1874	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
88		exmid01 4199	. 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 708 ∀wal 1351 = wceq 1353 ∃wex 1492 ∈ wcel 2148 ≠ wne 2347 ∀wral 2455 ∃wrex 2456 Vcvv 2738 ∩ cin 3129 ⊆ wss 3130 ∅c0 3423 ifcif 3535 {csn 3593 ∪ cuni 3810 class class class wbr 4004 ↦ cmpt 4065 EXMIDwem 4195 ωcom 4590 × cxp 4625 ^◡ccnv 4626 dom cdm 4627 ran crn 4628 ↾ cres 4629 Fun wfun 5211 ⟶wf 5213 –1-1→wf1 5214 –onto→wfo 5215 –1-1-onto→wf1o 5216 ‘cfv 5217 1_oc1o 6410 ≈ cen 6738 ≼ cdom 6739 ⊔ cdju 7036 inrcinr 7045 casecdjucase 7082 ℕ_∞xnninf 7118 Omnicomni 7132

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 4119 ax-sep 4122 ax-nul 4130 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-setind 4537 ax-iinf 4588

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 2740 df-sbc 2964 df-csb 3059 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-nul 3424 df-if 3536 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-iun 3889 df-br 4005 df-opab 4066 df-mpt 4067 df-tr 4103 df-exmid 4196 df-id 4294 df-iord 4367 df-on 4369 df-suc 4372 df-iom 4591 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-f1 5222 df-fo 5223 df-f1o 5224 df-fv 5225 df-ov 5878 df-oprab 5879 df-mpo 5880 df-1st 6141 df-2nd 6142 df-1o 6417 df-2o 6418 df-map 6650 df-en 6741 df-dom 6742 df-dju 7037 df-inl 7046 df-inr 7047 df-case 7083 df-nninf 7119 df-omni 7133

This theorem is referenced by: exmidsbthr 14774

W3C validator