P. 490 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48901-49000   *Has distinct variable group(s)

Type	Label	Description
Statement
21.49.10.3  Subspace topologies
Theorem	restcls2lem 48901	A closed set in a subspace topology is a subset of the subspace. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝑌)
Theorem	restcls2 48902	A closed set in a subspace topology is the closure in the original topology intersecting with the subspace. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    ⇒   ⊢ (𝜑 → 𝑆 = (((cls‘𝐽)‘𝑆) ∩ 𝑌))
Theorem	restclsseplem 48903	Lemma for restclssep 48904. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)
Theorem	restclssep 48904	Two disjoint closed sets in a subspace topology are separated in the original topology. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐾))    ⇒   ⊢ (𝜑 → ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅))
21.49.10.4  Limits and continuity in topological spaces
Theorem	cnneiima 48905	Given a continuous function, the preimage of a neighborhood is a neighborhood. To be precise, the preimage of a neighborhood of a subset 𝑇 of the codomain of a continuous function is a neighborhood of any subset of the preimage of 𝑇. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑁 ∈ ((nei‘𝐾)‘𝑇))    &   ⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ 𝑇))    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝑁) ∈ ((nei‘𝐽)‘𝑆))
21.49.10.5  Topological definitions using the reals
Theorem	iooii 48906	Open intervals are open sets of II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴(,)𝐵) ∈ II)
Theorem	icccldii 48907	Closed intervals are closed sets of II. Note that iccss 13375, iccordt 23101, and ordtresticc 23110 are proved from ixxss12 13326, ordtcld3 23086, and ordtrest2 23091, respectively. An alternate proof uses restcldi 23060, dfii2 24775, and icccld 24654. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ∈ (Clsd‘II))
Theorem	i0oii 48908	(0[,)𝐴) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝐴 ≤ 1 → (0[,)𝐴) ∈ II)
Theorem	io1ii 48909	(𝐴(,]1) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (0 ≤ 𝐴 → (𝐴(,]1) ∈ II)
21.49.10.6  Separated sets
Theorem	sepnsepolem1 48910*	Lemma for sepnsepo 48912. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥 ∈ 𝐽 (𝜑 ∧ ∃𝑦 ∈ 𝐽 (𝜓 ∧ 𝜒)))
Theorem	sepnsepolem2 48911*	Open neighborhood and neighborhood is equivalent regarding disjointness. Lemma for sepnsepo 48912. Proof could be shortened by 1 step using ssdisjdr 48797. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ((nei‘𝐽)‘𝐷)(𝑥 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ 𝐽 (𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)))
Theorem	sepnsepo 48912*	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 48913	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 48914*	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 48912. The relationship between separatedness and closure is also seen in isnrm 23222, isnrm2 23245, isnrm3 23246. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ((𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)))
Theorem	sepcsepo 48915*	If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo 48912 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 48893, adantr 480, and rexlimiva 3126. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	sepfsepc 48916*	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 48917	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 48918*	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 48919*	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 48920*	A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm 23204. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ 𝑗 ∃𝑦 ∈ 𝑗 (𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))}
Theorem	dfnrm3 48921*	A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm 23204. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝑗)‘𝑐)∃𝑦 ∈ ((nei‘𝑗)‘𝑑)(𝑥 ∩ 𝑦) = ∅)}
Theorem	iscnrm3lem1 48922*	Lemma for iscnrm3 48940. Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ((𝐽 ↾t 𝑥) ∈ Top ∧ 𝜑)))
Theorem	iscnrm3lem2 48923*	Lemma for iscnrm3 48940 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 → ((𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸) → 𝜒)))    &   ⊢ (𝜑 → (∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜓)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒))
Theorem	iscnrm3lem4 48924	Lemma for iscnrm3lem5 48925 and iscnrm3r 48936. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ (𝜂 → (𝜓 → 𝜁))    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	iscnrm3lem5 48925*	Lemma for iscnrm3l 48939. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → ((𝜓 → 𝜃) → 𝜎))    ⇒   ⊢ (𝜏 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝜑 → 𝜒) → (𝜂 → (𝜁 → 𝜎))))
Theorem	iscnrm3lem6 48926*	Lemma for iscnrm3lem7 48927. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑊 𝜓 → 𝜒))
Theorem	iscnrm3lem7 48927*	Lemma for iscnrm3rlem8 48935 and iscnrm3llem2 48938 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝑧 = 𝑍 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝑊 → (𝜃 ↔ 𝜏))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → (𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜒))
Theorem	iscnrm3rlem1 48928	Lemma for iscnrm3rlem2 48929. The hypothesis could be generalized to (𝜑 → (𝑆 ∖ 𝑇) ⊆ 𝑋). (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∖ 𝑇) = (𝑆 ∩ (𝑋 ∖ (𝑆 ∩ 𝑇))))
Theorem	iscnrm3rlem2 48929	Lemma for iscnrm3rlem3 48930. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∖ 𝑇) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ 𝑇)))))
Theorem	iscnrm3rlem3 48930	Lemma for iscnrm3r 48936. 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 48931	Lemma for iscnrm3rlem8 48935. 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 48932	Lemma for iscnrm3rlem6 48933. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ 𝐽)
Theorem	iscnrm3rlem6 48933	Lemma for iscnrm3rlem7 48934. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑂 ⊆ (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))    ⇒   ⊢ (𝜑 → (𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ↔ 𝑂 ∈ 𝐽))
Theorem	iscnrm3rlem7 48934	Lemma for iscnrm3rlem8 48935. 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 48935*	Lemma for iscnrm3r 48936. 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 48936*	Lemma for iscnrm3 48940. 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 48937	Lemma for iscnrm3l 48939. 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 48938*	Lemma for iscnrm3l 48939. 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 45049.) (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍)) ∧ 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) ∧ (𝐶 ∩ 𝐷) = ∅) → (∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) → ∃𝑙 ∈ (𝐽 ↾t 𝑍)∃𝑘 ∈ (𝐽 ↾t 𝑍)(𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅)))
Theorem	iscnrm3l 48939*	Lemma for iscnrm3 48940. 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 48940*	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 48941*	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 48942*	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 48943*	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 48944*	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 48945*	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 48946*	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 48947*	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 48948	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 48949	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 48950	Lemma for lubprdm 48951 and lubpr 48952. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ∧ (𝑈‘𝑆) = 𝑌))
Theorem	lubprdm 48951	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 48952	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 48953	Lemma for glbprdm 48954 and glbpr 48955. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ∧ (𝐺‘𝑆) = 𝑋))
Theorem	glbprdm 48954	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 48955	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 48956*	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 48957*	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 48958*	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 48959*	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 48960	Poset join is idempotent. latjidm 18421 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋)
Theorem	posmidm 48961	Poset meet is idempotent. latmidm 18433 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋)
Theorem	resiposbas 48962	Construct a poset (resipos 48963) for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐾))
Theorem	resipos 48963	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 48964*	There exists a poset for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Poset 𝐵 = (Base‘𝑘))
Theorem	exbasprs 48965*	There exists a preordered set for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Proset 𝐵 = (Base‘𝑘))
Theorem	basresposfo 48966	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 48967	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 48968	The class of posets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ Poset ∉ V
Theorem	prsnex 48969	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 48970	A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝐾 ∈ Toset → 𝐾 ∈ Lat)
Theorem	isclatd 48971*	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 48972*	Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ (𝐶 ∈ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ ∀𝑦 ∈ 𝐵 (𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦)) ↔ 𝐶 = ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}))
Theorem	unilbeu 48973*	Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}))
Theorem	ipolublem 48974*	Lemma for ipolubdm 48975 and ipolub 48976. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧))))
Theorem	ipolubdm 48975*	The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹))
Theorem	ipolub 48976*	The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18373 is in quantified form. mrelatlub 18521 could potentially be shortened using this. See mrelatlubALT 48983. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	ipoglblem 48977*	Lemma for ipoglbdm 48978 and ipoglb 48979. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋))))
Theorem	ipoglbdm 48978*	The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹))
Theorem	ipoglb 48979*	The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18374 is in quantified form. mrelatglb 18519 could potentially be shortened using this. See mrelatglbALT 48984. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇)
Theorem	ipolub0 48980	The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹)
Theorem	ipolub00 48981	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 48982	The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹)
Theorem	mrelatlubALT 48983	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 48984	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 48985	A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐶)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat)
Theorem	topclat 48986	A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    ⇒   ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat)
Theorem	toplatglb0 48987	The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽)
Theorem	toplatlub 48988	Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐽)    &   ⊢ 𝑈 = (lub‘𝐼)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆)
Theorem	toplatglb 48989	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 48990	Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ ∨ = (join‘𝐼)    ⇒   ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵))
Theorem	toplatmeet 48991	Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐽)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ ∧ = (meet‘𝐼)    ⇒   ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵))
Theorem	topdlat 48992	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 48993*	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	asclelbas 48994	Lifted scalars are in the base set of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof shortened by Thierry Arnoux, 22-Sep-2025.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊))
Theorem	asclelbasALT 48995	Alternate proof of asclelbas 48994. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊))
Theorem	asclcntr 48996	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 48997	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 21772, assa2ass2 21773, and asclval 21789, 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 48998	The base is empty iff the functionalized Hom-set operation is empty. (Contributed by Zhi Wang, 23-Oct-2025.)
⊢ ((Base‘𝐶) = ∅ ↔ (Homf ‘𝐶) = ∅)
Theorem	catprslem 48999*	Lemma for catprs 49000. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅))
Theorem	catprs 49000*	A preorder can be extracted from a category. See catprs2 49001 for more details. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))