P. 495 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49401-49500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	seposep 49401*	If two sets are separated by (open) neighborhoods, then they are separated subsets of the underlying set. Note that separatedness by open neighborhoods is equivalent to separatedness by neighborhoods. See sepnsepo 49399. The relationship between separatedness and closure is also seen in isnrm 23300, isnrm2 23323, isnrm3 23324. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ((𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)))
Theorem	sepcsepo 49402*	If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo 49399 for the equivalence between separatedness by open neighborhoods and separatedness by neighborhoods. Although 𝐽 ∈ Top might be redundant here, it is listed for explicitness. 𝐽 ∈ Top can be obtained from neircl 49380, adantr 480, and rexlimiva 3130. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	sepfsepc 49403*	If two sets are separated by a continuous function, then they are separated by closed neighborhoods. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1})))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	seppsepf 49404	If two sets are precisely separated by a continuous function, then they are separated by the continuous function. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 = (◡𝑓 “ {0}) ∧ 𝑇 = (◡𝑓 “ {1})))    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1})))
Theorem	seppcld 49405*	If two sets are precisely separated by a continuous function, then they are closed. An alternate proof involves II ∈ Fre. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 = (◡𝑓 “ {0}) ∧ 𝑇 = (◡𝑓 “ {1})))    ⇒   ⊢ (𝜑 → (𝑆 ∈ (Clsd‘𝐽) ∧ 𝑇 ∈ (Clsd‘𝐽)))
21.49.10.7  Separated spaces: T0, T1, T2 (Hausdorff) ...
Theorem	isnrm4 49406*	A topological space is normal iff any two disjoint closed sets are separated by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑑 ∈ (Clsd‘𝐽)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝐽)‘𝑐)∃𝑦 ∈ ((nei‘𝐽)‘𝑑)(𝑥 ∩ 𝑦) = ∅)))
Theorem	dfnrm2 49407*	A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm 23282. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ 𝑗 ∃𝑦 ∈ 𝑗 (𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))}
Theorem	dfnrm3 49408*	A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm 23282. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝑗)‘𝑐)∃𝑦 ∈ ((nei‘𝑗)‘𝑑)(𝑥 ∩ 𝑦) = ∅)}
Theorem	iscnrm3lem1 49409*	Lemma for iscnrm3 49427. Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ((𝐽 ↾t 𝑥) ∈ Top ∧ 𝜑)))
Theorem	iscnrm3lem2 49410*	Lemma for iscnrm3 49427 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 → ((𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸) → 𝜒)))    &   ⊢ (𝜑 → (∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜓)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒))
Theorem	iscnrm3lem4 49411	Lemma for iscnrm3lem5 49412 and iscnrm3r 49423. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ (𝜂 → (𝜓 → 𝜁))    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	iscnrm3lem5 49412*	Lemma for iscnrm3l 49426. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → ((𝜓 → 𝜃) → 𝜎))    ⇒   ⊢ (𝜏 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝜑 → 𝜒) → (𝜂 → (𝜁 → 𝜎))))
Theorem	iscnrm3lem6 49413*	Lemma for iscnrm3lem7 49414. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑊 𝜓 → 𝜒))
Theorem	iscnrm3lem7 49414*	Lemma for iscnrm3rlem8 49422 and iscnrm3llem2 49425 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝑧 = 𝑍 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝑊 → (𝜃 ↔ 𝜏))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → (𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜒))
Theorem	iscnrm3rlem1 49415	Lemma for iscnrm3rlem2 49416. The hypothesis could be generalized to (𝜑 → (𝑆 ∖ 𝑇) ⊆ 𝑋). (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∖ 𝑇) = (𝑆 ∩ (𝑋 ∖ (𝑆 ∩ 𝑇))))
Theorem	iscnrm3rlem2 49416	Lemma for iscnrm3rlem3 49417. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∖ 𝑇) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ 𝑇)))))
Theorem	iscnrm3rlem3 49417	Lemma for iscnrm3r 49423. The designed subspace is a subset of the original set; the two sets are closed sets in the subspace. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽)) → ((∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ 𝒫 ∪ 𝐽 ∧ (((cls‘𝐽)‘𝑆) ∖ ((cls‘𝐽)‘𝑇)) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) ∧ (((cls‘𝐽)‘𝑇) ∖ ((cls‘𝐽)‘𝑆)) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))))))
Theorem	iscnrm3rlem4 49418	Lemma for iscnrm3rlem8 49422. Given two disjoint subsets 𝑆 and 𝑇 of the underlying set of a topology 𝐽, if 𝑁 is a superset of (((cls‘𝐽)‘𝑆) ∖ 𝑇), then it is a superset of 𝑆. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∖ 𝑇) ⊆ 𝑁)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝑁)
Theorem	iscnrm3rlem5 49419	Lemma for iscnrm3rlem6 49420. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ 𝐽)
Theorem	iscnrm3rlem6 49420	Lemma for iscnrm3rlem7 49421. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑂 ⊆ (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))    ⇒   ⊢ (𝜑 → (𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ↔ 𝑂 ∈ 𝐽))
Theorem	iscnrm3rlem7 49421	Lemma for iscnrm3rlem8 49422. Open neighborhoods in the subspace topology are open neighborhoods in the original topology given that the subspace is an open set in the original topology. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))))    ⇒   ⊢ (𝜑 → 𝑂 ∈ 𝐽)
Theorem	iscnrm3rlem8 49422*	Lemma for iscnrm3r 49423. Disjoint open neighborhoods in the subspace topology are disjoint open neighborhoods in the original topology given that the subspace is an open set in the original topology. Therefore, given any two sets separated in the original topology and separated by open neighborhoods in the subspace topology, they must be separated by open neighborhoods in the original topology. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)) → (∃𝑙 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))∃𝑘 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))((((cls‘𝐽)‘𝑆) ∖ ((cls‘𝐽)‘𝑇)) ⊆ 𝑙 ∧ (((cls‘𝐽)‘𝑇) ∖ ((cls‘𝐽)‘𝑆)) ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))
Theorem	iscnrm3r 49423*	Lemma for iscnrm3 49427. If all subspaces of a topology are normal, i.e., two disjoint closed sets can be separated by open neighborhoods, then in the original topology two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑧 ∈ 𝒫 ∪ 𝐽∀𝑐 ∈ (Clsd‘(𝐽 ↾t 𝑧))∀𝑑 ∈ (Clsd‘(𝐽 ↾t 𝑧))((𝑐 ∩ 𝑑) = ∅ → ∃𝑙 ∈ (𝐽 ↾t 𝑧)∃𝑘 ∈ (𝐽 ↾t 𝑧)(𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅)) → ((𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽) → (((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))))
Theorem	iscnrm3llem1 49424	Lemma for iscnrm3l 49426. Closed sets in the subspace are subsets of the underlying set of the original topology. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍)) ∧ 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) ∧ (𝐶 ∩ 𝐷) = ∅) → (𝐶 ∈ 𝒫 ∪ 𝐽 ∧ 𝐷 ∈ 𝒫 ∪ 𝐽))
Theorem	iscnrm3llem2 49425*	Lemma for iscnrm3l 49426. If there exist disjoint open neighborhoods in the original topology for two disjoint closed sets in a subspace, then they can be separated by open neighborhoods in the subspace topology. (Could shorten proof with ssin0 45486.) (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍)) ∧ 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) ∧ (𝐶 ∩ 𝐷) = ∅) → (∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) → ∃𝑙 ∈ (𝐽 ↾t 𝑍)∃𝑘 ∈ (𝐽 ↾t 𝑍)(𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅)))
Theorem	iscnrm3l 49426*	Lemma for iscnrm3 49427. Given a topology 𝐽, if two separated sets can be separated by open neighborhoods, then all subspaces of the topology 𝐽 are normal, i.e., two disjoint closed sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑠 ∈ 𝒫 ∪ 𝐽∀𝑡 ∈ 𝒫 ∪ 𝐽(((𝑠 ∩ ((cls‘𝐽)‘𝑡)) = ∅ ∧ (((cls‘𝐽)‘𝑠) ∩ 𝑡) = ∅) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ((𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍)) ∧ 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) → ((𝐶 ∩ 𝐷) = ∅ → ∃𝑙 ∈ (𝐽 ↾t 𝑍)∃𝑘 ∈ (𝐽 ↾t 𝑍)(𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅)))))
Theorem	iscnrm3 49427*	A completely normal topology is a topology in which two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝐽 ∈ CNrm ↔ (𝐽 ∈ Top ∧ ∀𝑠 ∈ 𝒫 ∪ 𝐽∀𝑡 ∈ 𝒫 ∪ 𝐽(((𝑠 ∩ ((cls‘𝐽)‘𝑡)) = ∅ ∧ (((cls‘𝐽)‘𝑠) ∩ 𝑡) = ∅) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
Theorem	iscnrm3v 49428*	A topology is completely normal iff two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 10-Sep-2024.)
⊢ (𝐽 ∈ Top → (𝐽 ∈ CNrm ↔ ∀𝑠 ∈ 𝒫 ∪ 𝐽∀𝑡 ∈ 𝒫 ∪ 𝐽(((𝑠 ∩ ((cls‘𝐽)‘𝑡)) = ∅ ∧ (((cls‘𝐽)‘𝑠) ∩ 𝑡) = ∅) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
Theorem	iscnrm4 49429*	A completely normal topology is a topology in which two separated sets can be separated by neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝐽 ∈ CNrm ↔ (𝐽 ∈ Top ∧ ∀𝑠 ∈ 𝒫 ∪ 𝐽∀𝑡 ∈ 𝒫 ∪ 𝐽(((𝑠 ∩ ((cls‘𝐽)‘𝑡)) = ∅ ∧ (((cls‘𝐽)‘𝑠) ∩ 𝑡) = ∅) → ∃𝑛 ∈ ((nei‘𝐽)‘𝑠)∃𝑚 ∈ ((nei‘𝐽)‘𝑡)(𝑛 ∩ 𝑚) = ∅)))
21.49.11  Preordered sets and directed sets using extensible structures
Theorem	isprsd 49430*	Property of being a preordered set (deduction form). (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐾 ∈ Proset ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
21.49.12  Posets and lattices using extensible structures
21.49.12.1  Posets
Theorem	lubeldm2 49431*	Member of the domain of the least upper bound function of a poset. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)))
Theorem	glbeldm2 49432*	Member of the domain of the greatest lower bound function of a poset. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)))
Theorem	lubeldm2d 49433*	Member of the domain of the least upper bound function of a poset. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧))))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)))
Theorem	glbeldm2d 49434*	Member of the domain of the greatest lower bound function of a poset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥))))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓)))
Theorem	lubsscl 49435	If a subset of 𝑆 contains the LUB of 𝑆, then the two sets have the same LUB. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    &   ⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝑇)    ⇒   ⊢ (𝜑 → (𝑇 ∈ dom 𝑈 ∧ (𝑈‘𝑇) = (𝑈‘𝑆)))
Theorem	glbsscl 49436	If a subset of 𝑆 contains the GLB of 𝑆, then the two sets have the same GLB. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    &   ⊢ (𝜑 → (𝐺‘𝑆) ∈ 𝑇)    ⇒   ⊢ (𝜑 → (𝑇 ∈ dom 𝐺 ∧ (𝐺‘𝑇) = (𝐺‘𝑆)))
Theorem	lubprlem 49437	Lemma for lubprdm 49438 and lubpr 49439. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ∧ (𝑈‘𝑆) = 𝑌))
Theorem	lubprdm 49438	The set of two comparable elements in a poset has LUB. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)
Theorem	lubpr 49439	The LUB of the set of two comparable elements in a poset is the greater one of the two. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑌)
Theorem	glbprlem 49440	Lemma for glbprdm 49441 and glbpr 49442. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ∧ (𝐺‘𝑆) = 𝑋))
Theorem	glbprdm 49441	The set of two comparable elements in a poset has GLB. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)
Theorem	glbpr 49442	The GLB of the set of two comparable elements in a poset is the less one of the two. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝑋)
Theorem	joindm2 49443*	The join of any two elements always exists iff all unordered pairs have LUB. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝜑 → (dom ∨ = (𝐵 × 𝐵) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 {𝑥, 𝑦} ∈ dom 𝑈))
Theorem	joindm3 49444*	The join of any two elements always exists iff all unordered pairs have LUB (expanded version). (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝜑 → (dom ∨ = (𝐵 × 𝐵) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃!𝑧 ∈ 𝐵 ((𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧) ∧ ∀𝑤 ∈ 𝐵 ((𝑥 ≤ 𝑤 ∧ 𝑦 ≤ 𝑤) → 𝑧 ≤ 𝑤))))
Theorem	meetdm2 49445*	The meet of any two elements always exists iff all unordered pairs have GLB. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝜑 → (dom ∧ = (𝐵 × 𝐵) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 {𝑥, 𝑦} ∈ dom 𝐺))
Theorem	meetdm3 49446*	The meet of any two elements always exists iff all unordered pairs have GLB (expanded version). (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝜑 → (dom ∧ = (𝐵 × 𝐵) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃!𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑥 ∧ 𝑧 ≤ 𝑦) ∧ ∀𝑤 ∈ 𝐵 ((𝑤 ≤ 𝑥 ∧ 𝑤 ≤ 𝑦) → 𝑤 ≤ 𝑧))))
Theorem	posjidm 49447	Poset join is idempotent. latjidm 18428 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋)
Theorem	posmidm 49448	Poset meet is idempotent. latmidm 18440 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋)
Theorem	resiposbas 49449	Construct a poset (resipos 49450) for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐾))
Theorem	resipos 49450	A set equipped with an order where no distinct elements are comparable is a poset. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐾 ∈ Poset)
Theorem	exbaspos 49451*	There exists a poset for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Poset 𝐵 = (Base‘𝑘))
Theorem	exbasprs 49452*	There exists a preordered set for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Proset 𝐵 = (Base‘𝑘))
Theorem	basresposfo 49453	The base function restricted to the class of posets maps the class of posets onto the universal class. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (Base ↾ Poset):Poset–onto→V
Theorem	basresprsfo 49454	The base function restricted to the class of preordered sets maps the class of preordered sets onto the universal class. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (Base ↾ Proset ): Proset –onto→V
Theorem	posnex 49455	The class of posets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ Poset ∉ V
Theorem	prsnex 49456	The class of preordered sets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ Proset ∉ V
21.49.12.2  Lattices
Theorem	toslat 49457	A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝐾 ∈ Toset → 𝐾 ∈ Lat)
Theorem	isclatd 49458*	The predicate "is a complete lattice" (deduction form). (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐾))    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝑈)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → 𝐾 ∈ CLat)
21.49.12.3  Subset order structures
Theorem	intubeu 49459*	Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ (𝐶 ∈ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ ∀𝑦 ∈ 𝐵 (𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦)) ↔ 𝐶 = ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}))
Theorem	unilbeu 49460*	Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}))
Theorem	ipolublem 49461*	Lemma for ipolubdm 49462 and ipolub 49463. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧))))
Theorem	ipolubdm 49462*	The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹))
Theorem	ipolub 49463*	The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18378 is in quantified form. mrelatlub 18528 could potentially be shortened using this. See mrelatlubALT 49470. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	ipoglblem 49464*	Lemma for ipoglbdm 49465 and ipoglb 49466. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋))))
Theorem	ipoglbdm 49465*	The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹))
Theorem	ipoglb 49466*	The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18379 is in quantified form. mrelatglb 18526 could potentially be shortened using this. See mrelatglbALT 49471. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇)
Theorem	ipolub0 49467	The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹)
Theorem	ipolub00 49468	The LUB of the empty set is the empty set if it is contained. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → ∅ ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑈‘∅) = ∅)
Theorem	ipoglb0 49469	The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹)
Theorem	mrelatlubALT 49470	Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Zhi Wang, 29-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐹 = (mrCls‘𝐶)    &   ⊢ 𝐿 = (lub‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶) → (𝐿‘𝑈) = (𝐹‘∪ 𝑈))
Theorem	mrelatglbALT 49471	Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Zhi Wang, 29-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈)
Theorem	mreclat 49472	A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat)
Theorem	topclat 49473	A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat)
Theorem	toplatglb0 49474	The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽)
Theorem	toplatlub 49475	Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐽)    &   ⊢ 𝑈 = (lub‘𝐼)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆)
Theorem	toplatglb 49476	Greatest lower bounds in a topology are realized by the interior of the intersection. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐽)    &   ⊢ 𝐺 = (glb‘𝐼)    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = ((int‘𝐽)‘∩ 𝑆))
Theorem	toplatjoin 49477	Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ ∨ = (join‘𝐼)    ⇒   ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵))
Theorem	toplatmeet 49478	Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ ∧ = (meet‘𝐼)    ⇒   ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵))
Theorem	topdlat 49479	A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat)
21.49.13  Rings
21.49.13.1  Multiplicative Group
Theorem	elmgpcntrd 49480*	The center of a ring. (Contributed by Zhi Wang, 11-Sep-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑍 = (Cntr‘𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑋))    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑍)
21.49.14  Associative algebras
21.49.14.1  Definition and basic properties
Theorem	asclelbasALT 49481	Alternate proof of asclelbas 21863. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊))
Theorem	asclcntr 49482	The algebra scalar lifting function maps into the center of the algebra. Equivalently, a lifted scalar is a center of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ 𝑀 = (mulGrp‘𝑊)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Cntr‘𝑀))
Theorem	asclcom 49483	Scalars are commutative after being lifted. However, the scalars themselves are not necessarily commutative if the algebra is not a faithful module. For example, Let 𝐹 be the 2 by 2 upper triangular matrix algebra over a commutative ring 𝑊. It is provable that 𝐹 is in general non-commutative. Define scalar multiplication 𝐶 · 𝑋 as multipying the top-left entry, which is a "vector" element of 𝑊, of the "scalar" 𝐶, which is now an upper triangular matrix, with the "vector" 𝑋 ∈ (Base‘𝑊). Equivalently, the algebra scalar lifting function is not necessarily injective unless the algebra is faithful. Therefore, all "scalar injection" was renamed. Alternate proof involves assa2ass 21843, assa2ass2 21844, and asclval 21859, by setting 𝑋 and 𝑌 the multiplicative identity of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ ∗ = (.r‘𝐹)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴‘(𝐶 ∗ 𝐷)) = (𝐴‘(𝐷 ∗ 𝐶)))
21.49.15  Categories
21.49.15.1  Categories
Theorem	homf0 49484	The base is empty iff the functionalized Hom-set operation is empty. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ ((Base‘𝐶) = ∅ ↔ (Homf ‘𝐶) = ∅)
Theorem	catprslem 49485*	Lemma for catprs 49486. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))
Theorem	catprs 49486*	A preorder can be extracted from a category. See catprs2 49487 for more details. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	catprs2 49487*	A category equipped with the induced preorder, where an object 𝑥 is defined to be "less than or equal to" 𝑦 iff there is a morphism from 𝑥 to 𝑦, is a preordered set, or a proset. The category might not be thin. See catprsc 49488 and catprsc2 49489 for constructions satisfying the hypothesis "catprs.1". See catprs 49486 for a more primitive version. See prsthinc 49939 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	catprsc 49488*	A construction of the preorder induced by a category. See catprs2 49487 for details. See also catprsc2 49489 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)})    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅))
Theorem	catprsc2 49489*	An alternate construction of the preorder induced by a category. See catprs2 49487 for details. See also catprsc 49488 for a different construction. The two constructions are different because df-cat 17634 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐻𝑦) ≠ ∅})    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅))
Theorem	endmndlem 49490	A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 50053 for converting a monoid to a category. Lemma for bj-endmnd 37632. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀))    &   ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (+g‘𝑀))    ⇒   ⊢ (𝜑 → 𝑀 ∈ Mnd)
21.49.15.2  Opposite category
Theorem	oppccatb 49491	An opposite category is a category. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝑂 ∈ Cat))
Theorem	oppcmndclem 49492	Lemma for oppcmndc 49494. Everything is true for two distinct elements in a singleton or an empty set (since it is impossible). Note that if this theorem and oppcendc 49493 are in ¬ 𝑥 = 𝑦 form, then both proofs should be one step shorter. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ (𝜑 → 𝐵 = {𝐴})    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≠ 𝑌 → 𝜓))
Theorem	oppcendc 49493*	The opposite category of a category whose morphisms are all endomorphisms has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅))    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂))
Theorem	oppcmndc 49494	The opposite category of a category whose base set is a singleton or an empty set has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ (𝜑 → 𝐵 = {𝑋})    ⇒   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂))
21.49.15.3  Monomorphisms and epimorphisms
Theorem	idmon 49495	An identity arrow, or an identity morphism, is a monomorphism. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑀 = (Mono‘𝐶)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝑀𝑋))
Theorem	idepi 49496	An identity arrow, or an identity morphism, is an epimorphism. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝐸 = (Epi‘𝐶)    ⇒   ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐸𝑋))
21.49.15.4  Sections, inverses, isomorphisms
Theorem	sectrcl 49497	Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	sectrcl2 49498	Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑆 = (Sect‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
Theorem	invrcl 49499	Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	invrcl2 49500	Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.)
⊢ 𝑁 = (Inv‘𝐶)    &   ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))