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 15582

Description: Lemma for exmidsbthr 15583. (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 7182	. . . . . . . . . 10 ⊢ ℕ_∞ ∈ V
3		fconstmpt 4707	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) = (𝑖 ∈ ω ↦ ∅)
4		0nninf 15564	. . . . . . . . . . . . . . 15 ⊢ (ω × {∅}) ∈ ℕ_∞
5	3, 4	eqeltrri 2267	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω ↦ ∅) ∈ ℕ_∞
6	5	fconst6 5454	. . . . . . . . . . . . 13 ⊢ (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞
7	6	a1i 9	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞)
8		ssel 3174	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 ∈ {∅}))
9		elsni 3637	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ {∅} → 𝑢 = ∅)
10	8, 9	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑢 ∈ 𝑧 → 𝑢 = ∅))
11		ssel 3174	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 ∈ {∅}))
12		elsni 3637	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {∅} → 𝑣 = ∅)
13	11, 12	syl6 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ {∅} → (𝑣 ∈ 𝑧 → 𝑣 = ∅))
14	10, 13	anim12d 335	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ {∅} → ((𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → (𝑢 = ∅ ∧ 𝑣 = ∅)))
15		eqtr3 2213	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = ∅ ∧ 𝑣 = ∅) → 𝑢 = 𝑣)
16	14, 15	syl6 33	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ⊆ {∅} → ((𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧) → 𝑢 = 𝑣))
17	16	imp 124	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ⊆ {∅} ∧ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) → 𝑢 = 𝑣)
18	17	a1d 22	. . . . . . . . . . . . 13 ⊢ ((𝑧 ⊆ {∅} ∧ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) → (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣))
19	18	ralrimivva 2576	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {∅} → ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣))
20		dff13 5812	. . . . . . . . . . . 12 ⊢ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞ ↔ ((𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧⟶ℕ_∞ ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑢) = ((𝑧 × {(𝑖 ∈ ω ↦ ∅)})‘𝑣) → 𝑢 = 𝑣)))
21	7, 19, 20	sylanbrc 417	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (𝑧 × {(𝑖 ∈ ω ↦ ∅)}):𝑧–1-1→ℕ_∞)
22		exmidsbthrlem.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = (𝑝 ∈ ℕ_∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_o, (𝑝‘∪ 𝑖))))
23	22	peano4nninf 15566	. . . . . . . . . . . 12 ⊢ 𝑆:ℕ_∞–1-1→ℕ_∞
24	23	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → 𝑆:ℕ_∞–1-1→ℕ_∞)
25		disj 3496	. . . . . . . . . . . . 13 ⊢ ((ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅ ↔ ∀𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ¬ 𝑎 ∈ ran 𝑆)
26	22	peano3nninf 15567	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅))
27		eqidd 2194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → ∅ = ∅)
28	27	cbvmptv 4126	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ω ↦ ∅) = (𝑖 ∈ ω ↦ ∅)
29	28	neeq2i 2380	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆‘𝑏) ≠ (𝑘 ∈ ω ↦ ∅) ↔ (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
30	26, 29	sylib 122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℕ_∞ → (𝑆‘𝑏) ≠ (𝑖 ∈ ω ↦ ∅))
31	30	neneqd 2385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ ℕ_∞ → ¬ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
32	31	nrex 2586	. . . . . . . . . . . . . . . 16 ⊢ ¬ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅)
33		f1dm 5465	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:ℕ_∞–1-1→ℕ_∞ → dom 𝑆 = ℕ_∞)
34	23, 33	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ dom 𝑆 = ℕ_∞
35		eqcom 2195	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏) ↔ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
36	34, 35	rexeqbii 2507	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏) ↔ ∃𝑏 ∈ ℕ_∞ (𝑆‘𝑏) = (𝑖 ∈ ω ↦ ∅))
37	32, 36	mtbir 672	. . . . . . . . . . . . . . 15 ⊢ ¬ ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)
38	22	funmpt2 5294	. . . . . . . . . . . . . . . 16 ⊢ Fun 𝑆
39		elrnrexdm 5698	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑆 → ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏)))
40	38, 39	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆 → ∃𝑏 ∈ dom 𝑆(𝑖 ∈ ω ↦ ∅) = (𝑆‘𝑏))
41	37, 40	mto 663	. . . . . . . . . . . . . 14 ⊢ ¬ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆
42		rnxpss 5098	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ⊆ {(𝑖 ∈ ω ↦ ∅)}
43	42	sseli 3176	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)})
44		elsni 3637	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {(𝑖 ∈ ω ↦ ∅)} → 𝑎 = (𝑖 ∈ ω ↦ ∅))
45	43, 44	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → 𝑎 = (𝑖 ∈ ω ↦ ∅))
46	45	eleq1d 2262	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → (𝑎 ∈ ran 𝑆 ↔ (𝑖 ∈ ω ↦ ∅) ∈ ran 𝑆))
47	41, 46	mtbiri 676	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) → ¬ 𝑎 ∈ ran 𝑆)
48	25, 47	mprgbir 2552	. . . . . . . . . . . 12 ⊢ (ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅
49	48	a1i 9	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ {∅} → (ran (𝑧 × {(𝑖 ∈ ω ↦ ∅)}) ∩ ran 𝑆) = ∅)
50	21, 24, 49	casef1 7151	. . . . . . . . . 10 ⊢ (𝑧 ⊆ {∅} → case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞)
51		f1domg 6814	. . . . . . . . . 10 ⊢ (ℕ_∞ ∈ V → (case((𝑧 × {(𝑖 ∈ ω ↦ ∅)}), 𝑆):(𝑧 ⊔ ℕ_∞)–1-1→ℕ_∞ → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
52	2, 50, 51	mpsyl 65	. . . . . . . . 9 ⊢ (𝑧 ⊆ {∅} → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
53	52	adantl 277	. . . . . . . 8 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞)
54		inrresf1 7123	. . . . . . . . 9 ⊢ (inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞)
55		vex 2763	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
56		djuex 7104	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ V ∧ ℕ_∞ ∈ V) → (𝑧 ⊔ ℕ_∞) ∈ V)
57	55, 2, 56	mp2an 426	. . . . . . . . . 10 ⊢ (𝑧 ⊔ ℕ_∞) ∈ V
58	57	f1dom 6816	. . . . . . . . 9 ⊢ ((inr ↾ ℕ_∞):ℕ_∞–1-1→(𝑧 ⊔ ℕ_∞) → ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))
59	54, 58	ax-mp 5	. . . . . . . 8 ⊢ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)
60	53, 59	jctir 313	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
61		breq12 4035	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≼ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≼ ℕ_∞))
62		breq12 4035	. . . . . . . . . . . 12 ⊢ ((𝑦 = ℕ_∞ ∧ 𝑥 = (𝑧 ⊔ ℕ_∞)) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
63	62	ancoms 268	. . . . . . . . . . 11 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑦 ≼ 𝑥 ↔ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)))
64	61, 63	anbi12d 473	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ ((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞))))
65		breq12 4035	. . . . . . . . . 10 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (𝑥 ≈ 𝑦 ↔ (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞))
66	64, 65	imbi12d 234	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ⊔ ℕ_∞) ∧ 𝑦 = ℕ_∞) → (((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ↔ (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)))
67	66	spc2gv 2852	. . . . . . . 8 ⊢ (((𝑧 ⊔ ℕ_∞) ∈ V ∧ ℕ_∞ ∈ V) → (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)))
68	57, 2, 67	mp2an 426	. . . . . . 7 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (((𝑧 ⊔ ℕ_∞) ≼ ℕ_∞ ∧ ℕ_∞ ≼ (𝑧 ⊔ ℕ_∞)) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞))
69	1, 60, 68	sylc 62	. . . . . 6 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 ⊔ ℕ_∞) ≈ ℕ_∞)
70		bren 6803	. . . . . 6 ⊢ ((𝑧 ⊔ ℕ_∞) ≈ ℕ_∞ ↔ ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
71	69, 70	sylib 122	. . . . 5 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → ∃𝑓 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞)
72		nninfomni 15579	. . . . . . . . 9 ⊢ ℕ_∞ ∈ Omni
73	72	a1i 9	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → ℕ_∞ ∈ Omni)
74		f1ocnv 5514	. . . . . . . . . 10 ⊢ (𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞ → ^◡𝑓:ℕ_∞–1-1-onto→(𝑧 ⊔ ℕ_∞))
75		f1ofo 5508	. . . . . . . . . 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 7210	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) ∧ 𝑓:(𝑧 ⊔ ℕ_∞)–1-1-onto→ℕ_∞) → (∃𝑤 𝑤 ∈ 𝑧 ∨ 𝑧 = ∅))
79		sssnm 3781	. . . . . . . . . 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 1910	. . . 4 ⊢ ((∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) ∧ 𝑧 ⊆ {∅}) → (𝑧 = ∅ ∨ 𝑧 = {∅}))
86	85	ex 115	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → (𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
87	86	alrimiv 1885	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → (𝑧 = ∅ ∨ 𝑧 = {∅})))
88		exmid01 4228	. 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 1503 ∈ wcel 2164 ≠ wne 2364 ∀wral 2472 ∃wrex 2473 Vcvv 2760 ∩ cin 3153 ⊆ wss 3154 ∅c0 3447 ifcif 3558 {csn 3619 ∪ cuni 3836 class class class wbr 4030 ↦ cmpt 4091 EXMIDwem 4224 ωcom 4623 × cxp 4658 ^◡ccnv 4659 dom cdm 4660 ran crn 4661 ↾ cres 4662 Fun wfun 5249 ⟶wf 5251 –1-1→wf1 5252 –onto→wfo 5253 –1-1-onto→wf1o 5254 ‘cfv 5255 1_oc1o 6464 ≈ cen 6794 ≼ cdom 6795 ⊔ cdju 7098 inrcinr 7107 casecdjucase 7144 ℕ_∞xnninf 7180 Omnicomni 7195

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4145 ax-sep 4148 ax-nul 4156 ax-pow 4204 ax-pr 4239 ax-un 4465 ax-setind 4570 ax-iinf 4621

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 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-ral 2477 df-rex 2478 df-reu 2479 df-rab 2481 df-v 2762 df-sbc 2987 df-csb 3082 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-nul 3448 df-if 3559 df-pw 3604 df-sn 3625 df-pr 3626 df-op 3628 df-uni 3837 df-int 3872 df-iun 3915 df-br 4031 df-opab 4092 df-mpt 4093 df-tr 4129 df-exmid 4225 df-id 4325 df-iord 4398 df-on 4400 df-suc 4403 df-iom 4624 df-xp 4666 df-rel 4667 df-cnv 4668 df-co 4669 df-dm 4670 df-rn 4671 df-res 4672 df-ima 4673 df-iota 5216 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-ov 5922 df-oprab 5923 df-mpo 5924 df-1st 6195 df-2nd 6196 df-1o 6471 df-2o 6472 df-map 6706 df-en 6797 df-dom 6798 df-dju 7099 df-inl 7108 df-inr 7109 df-case 7145 df-nninf 7181 df-omni 7196

This theorem is referenced by: exmidsbthr 15583

W3C validator