P. 487 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48601-48700   *Has distinct variable group(s)

Type	Label	Description
Statement
21.49.9.6  Separated sets
Theorem	sepnsepolem1 48601*	Lemma for sepnsepo 48603. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥 ∈ 𝐽 (𝜑 ∧ ∃𝑦 ∈ 𝐽 (𝜓 ∧ 𝜒)))
Theorem	sepnsepolem2 48602*	Open neighborhood and neighborhood is equivalent regarding disjointness. Lemma for sepnsepo 48603. Proof could be shortened by 1 step using ssdisjdr 48540. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ((nei‘𝐽)‘𝐷)(𝑥 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ 𝐽 (𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)))
Theorem	sepnsepo 48603*	Open neighborhood and neighborhood is equivalent regarding disjointness for both sides. Namely, separatedness by open neighborhoods is equivalent to separatedness by neighborhoods. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝐶)∃𝑦 ∈ ((nei‘𝐽)‘𝐷)(𝑥 ∩ 𝑦) = ∅ ↔ ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)))
Theorem	sepdisj 48604	Separated sets are disjoint. Note that in general separatedness also requires 𝑇 ⊆ ∪ 𝐽 and (𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ as well but they are unnecessary here. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)    ⇒   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)
Theorem	seposep 48605*	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 48603. The relationship between separatedness and closure is also seen in isnrm 23364, isnrm2 23387, isnrm3 23388. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ((𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)))
Theorem	sepcsepo 48606*	If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo 48603 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 48584, adantr 480, and rexlimiva 3153. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	sepfsepc 48607*	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 48608	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 48609*	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.9.7  Separated spaces: T0, T1, T2 (Hausdorff) ...
Theorem	isnrm4 48610*	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 48611*	A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm 23346. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ 𝑗 ∃𝑦 ∈ 𝑗 (𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))}
Theorem	dfnrm3 48612*	A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm 23346. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝑗)‘𝑐)∃𝑦 ∈ ((nei‘𝑗)‘𝑑)(𝑥 ∩ 𝑦) = ∅)}
Theorem	iscnrm3lem1 48613*	Lemma for iscnrm3 48632. Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ((𝐽 ↾t 𝑥) ∈ Top ∧ 𝜑)))
Theorem	iscnrm3lem2 48614*	Lemma for iscnrm3 48632 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 → ((𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸) → 𝜒)))    &   ⊢ (𝜑 → (∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜓)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒))
Theorem	iscnrm3lem3 48615	Lemma for iscnrm3lem4 48616. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓))
Theorem	iscnrm3lem4 48616	Lemma for iscnrm3lem5 48617 and iscnrm3r 48628. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ (𝜂 → (𝜓 → 𝜁))    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	iscnrm3lem5 48617*	Lemma for iscnrm3l 48631. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → ((𝜓 → 𝜃) → 𝜎))    ⇒   ⊢ (𝜏 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝜑 → 𝜒) → (𝜂 → (𝜁 → 𝜎))))
Theorem	iscnrm3lem6 48618*	Lemma for iscnrm3lem7 48619. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑊 𝜓 → 𝜒))
Theorem	iscnrm3lem7 48619*	Lemma for iscnrm3rlem8 48627 and iscnrm3llem2 48630 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝑧 = 𝑍 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝑊 → (𝜃 ↔ 𝜏))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → (𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜒))
Theorem	iscnrm3rlem1 48620	Lemma for iscnrm3rlem2 48621. The hypothesis could be generalized to (𝜑 → (𝑆 ∖ 𝑇) ⊆ 𝑋). (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∖ 𝑇) = (𝑆 ∩ (𝑋 ∖ (𝑆 ∩ 𝑇))))
Theorem	iscnrm3rlem2 48621	Lemma for iscnrm3rlem3 48622. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∖ 𝑇) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ 𝑇)))))
Theorem	iscnrm3rlem3 48622	Lemma for iscnrm3r 48628. 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 48623	Lemma for iscnrm3rlem8 48627. 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 48624	Lemma for iscnrm3rlem6 48625. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ 𝐽)
Theorem	iscnrm3rlem6 48625	Lemma for iscnrm3rlem7 48626. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑂 ⊆ (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))    ⇒   ⊢ (𝜑 → (𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ↔ 𝑂 ∈ 𝐽))
Theorem	iscnrm3rlem7 48626	Lemma for iscnrm3rlem8 48627. 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 48627*	Lemma for iscnrm3r 48628. 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 48628*	Lemma for iscnrm3 48632. 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 48629	Lemma for iscnrm3l 48631. 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 48630*	Lemma for iscnrm3l 48631. 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 44957.) (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍)) ∧ 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) ∧ (𝐶 ∩ 𝐷) = ∅) → (∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) → ∃𝑙 ∈ (𝐽 ↾t 𝑍)∃𝑘 ∈ (𝐽 ↾t 𝑍)(𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅)))
Theorem	iscnrm3l 48631*	Lemma for iscnrm3 48632. 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 48632*	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 48633*	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 48634*	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.10  Preordered sets and directed sets using extensible structures
Theorem	isprsd 48635*	Property of being a preordered set (deduction form). (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐾 ∈ Proset ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
21.49.11  Posets and lattices using extensible structures
21.49.11.1  Posets
Theorem	lubeldm2 48636*	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 48637*	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 48638*	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 48639*	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 48640	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 48641	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 48642	Lemma for lubprdm 48643 and lubpr 48644. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ∧ (𝑈‘𝑆) = 𝑌))
Theorem	lubprdm 48643	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 48644	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 48645	Lemma for glbprdm 48646 and glbpr 48647. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ∧ (𝐺‘𝑆) = 𝑋))
Theorem	glbprdm 48646	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 48647	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 48648*	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 48649*	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 48650*	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 48651*	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 48652	Poset join is idempotent. latjidm 18532 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋)
Theorem	posmidm 48653	Poset meet is idempotent. latmidm 18544 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋)
21.49.11.2  Lattices
Theorem	toslat 48654	A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝐾 ∈ Toset → 𝐾 ∈ Lat)
Theorem	isclatd 48655*	The predicate "is a complete lattice" (deduction form). (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐾))    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝑈)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → 𝐾 ∈ CLat)
21.49.11.3  Subset order structures
Theorem	intubeu 48656*	Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ (𝐶 ∈ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ ∀𝑦 ∈ 𝐵 (𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦)) ↔ 𝐶 = ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}))
Theorem	unilbeu 48657*	Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}))
Theorem	ipolublem 48658*	Lemma for ipolubdm 48659 and ipolub 48660. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧))))
Theorem	ipolubdm 48659*	The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹))
Theorem	ipolub 48660*	The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18484 is in quantified form. mrelatlub 18632 could potentially be shortened using this. See mrelatlubALT 48667. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	ipoglblem 48661*	Lemma for ipoglbdm 48662 and ipoglb 48663. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋))))
Theorem	ipoglbdm 48662*	The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹))
Theorem	ipoglb 48663*	The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18485 is in quantified form. mrelatglb 18630 could potentially be shortened using this. See mrelatglbALT 48668. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇)
Theorem	ipolub0 48664	The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹)
Theorem	ipolub00 48665	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 48666	The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹)
Theorem	mrelatlubALT 48667	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 48668	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 48669	A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat)
Theorem	topclat 48670	A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat)
Theorem	toplatglb0 48671	The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽)
Theorem	toplatlub 48672	Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐽)    &   ⊢ 𝑈 = (lub‘𝐼)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆)
Theorem	toplatglb 48673	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 48674	Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ ∨ = (join‘𝐼)    ⇒   ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵))
Theorem	toplatmeet 48675	Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ ∧ = (meet‘𝐼)    ⇒   ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵))
Theorem	topdlat 48676	A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat)
21.49.12  Categories
21.49.12.1  Categories
Theorem	catprslem 48677*	Lemma for catprs 48678. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))
Theorem	catprs 48678*	A preorder can be extracted from a category. See catprs2 48679 for more details. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	catprs2 48679*	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 48680 and catprsc2 48681 for constructions satisfying the hypothesis "catprs.1". See catprs 48678 for a more primitive version. See prsthinc 48721 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → ≤ = (le‘𝐶))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Proset )
Theorem	catprsc 48680*	A construction of the preorder induced by a category. See catprs2 48679 for details. See also catprsc2 48681 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)})    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅))
Theorem	catprsc2 48681*	An alternate construction of the preorder induced by a category. See catprs2 48679 for details. See also catprsc 48680 for a different construction. The two constructions are different because df-cat 17726 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.)
⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐻𝑦) ≠ ∅})    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅))
Theorem	endmndlem 48682	A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 48751 for converting a monoid to a category. Lemma for bj-endmnd 37284. (Contributed by Zhi Wang, 25-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀))    &   ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (+g‘𝑀))    ⇒   ⊢ (𝜑 → 𝑀 ∈ Mnd)
21.49.12.2  Monomorphisms and epimorphisms
Theorem	idmon 48683	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 48684	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.12.3  Functors
Theorem	funcf2lem 48685*	A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 1-Oct-2024.)
⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦))))
21.49.13  Examples of categories
21.49.13.1  Thin categories
Syntax	cthinc 48686	Extend class notation with the class of thin categories.
class ThinCat
Definition	df-thinc 48687*	Definition of the class of thin categories, or posetal categories, whose hom-sets each contain at most one morphism. Example 3.26(2) of [Adamek] p. 33. "ThinCat" was taken instead of "PosCat" because the latter might mean the category of posets. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ThinCat = {𝑐 ∈ Cat ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)}
Theorem	isthinc 48688*	The predicate "is a thin category". (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)))
Theorem	isthinc2 48689*	A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ≼ 1o))
Theorem	isthinc3 48690*	A thin category is a category in which, given a pair of objects 𝑥 and 𝑦 and any two morphisms 𝑓, 𝑔 from 𝑥 to 𝑦, the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑥𝐻𝑦)𝑓 = 𝑔))
Theorem	thincc 48691	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝐶 ∈ ThinCat → 𝐶 ∈ Cat)
Theorem	thinccd 48692	A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	thincssc 48693	A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ ThinCat ⊆ Cat
Theorem	isthincd2lem1 48694*	Lemma for isthincd2 48705 and thincmo2 48695. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thincmo2 48695	Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑌))    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ ThinCat)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	thincmo 48696*	There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmoALT 48697*	Alternate proof for thincmo 48696. (Contributed by Zhi Wang, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincmod 48698*	At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → ∃*𝑓 𝑓 ∈ (𝑋𝐻𝑌))
Theorem	thincn0eu 48699*	In a thin category, a hom-set being non-empty is equivalent to having a unique element. (Contributed by Zhi Wang, 21-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    ⇒   ⊢ (𝜑 → ((𝑋𝐻𝑌) ≠ ∅ ↔ ∃!𝑓 𝑓 ∈ (𝑋𝐻𝑌)))
Theorem	thincid 48700	In a thin category, a morphism from an object to itself is an identity morphism. (Contributed by Zhi Wang, 24-Sep-2024.)
⊢ (𝜑 → 𝐶 ∈ ThinCat)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑋))    ⇒   ⊢ (𝜑 → 𝐹 = ( 1 ‘𝑋))