P. 501 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 50001-50100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	f1omo 50001*	There is at most one element in the function value of a constant function whose output is 1o. (An artifact of our function value definition.) Proof could be significantly shortened by fvconstdomi 50000 assuming ax-un 7751 (see f1omoALT 50003). (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by SN, 24-Nov-2025.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
Theorem	f1omoOLD 50002*	Obsolete version of f1omo 50001 as of 24-Nov-2025. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
Theorem	f1omoALT 50003*	There is at most one element in the function value of a constant function whose output is 1o. (An artifact of our function value definition.) Use f1omo 50001 without assuming ax-un 7751. (Contributed by Zhi Wang, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 = (𝐴 × {1o}))    ⇒   ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋))
21.51.7  Order sets
21.51.7.1  Real number intervals
Theorem	iccin 50004	Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)[,]if(𝐵 ≤ 𝐷, 𝐵, 𝐷)))
Theorem	iccdisj2 50005	If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 < 𝐶) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = ∅)
Theorem	iccdisj 50006	If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) ∧ 𝐵 < 𝐶) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = ∅)
21.51.8  Extensible structures
21.51.8.1  Basic definitions
Theorem	slotresfo 50007*	The condition of a structure component extractor restricted to a class being a surjection. This combined with fonex 49977 can be used to prove a class being proper. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐸 Fn V    &   ⊢ (𝑘 ∈ 𝐴 → (𝐸‘𝑘) ∈ 𝑉)    &   ⊢ (𝑏 ∈ 𝑉 → 𝐾 ∈ 𝐴)    &   ⊢ (𝑏 ∈ 𝑉 → 𝑏 = (𝐸‘𝐾))    ⇒   ⊢ (𝐸 ↾ 𝐴):𝐴–onto→𝑉
21.51.9  Moore spaces
Theorem	mreuniss 50008	The union of a collection of closed sets is a subset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → ∪ 𝑆 ⊆ 𝑋)
21.51.10  Topology Additional contents for topology.
21.51.10.1  Closure and interior
Theorem	clduni 50009	The union of closed sets is the underlying set of the topology (the union of open sets). (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝐽 ∈ Top → ∪ (Clsd‘𝐽) = ∪ 𝐽)
Theorem	opncldbid 50010*	Conditions on open sets are equivalent to conditions on closed sets. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 = (∪ 𝐽 ∖ 𝑦)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐽 𝜓 ↔ ∀𝑦 ∈ (Clsd‘𝐽)𝜒))
Theorem	opndisj 50011	Two ways of saying that two open sets are disjoint, if 𝐽 is a topology and 𝑋 is an open set. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝑍 = (∪ 𝐽 ∖ 𝑋) → (𝑌 ∈ (𝐽 ∩ 𝒫 𝑍) ↔ (𝑌 ∈ 𝐽 ∧ (𝑋 ∩ 𝑌) = ∅)))
Theorem	clddisj 50012	Two ways of saying that two closed sets are disjoint, if 𝐽 is a topology and 𝑋 is a closed set. An alternative proof is similar to that of opndisj 50011 with elssuni 4898 replaced by the combination of cldss 23347 and eqid 2760. (Contributed by Zhi Wang, 6-Sep-2024.)
⊢ (𝑍 = (∪ 𝐽 ∖ 𝑋) → (𝑌 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑍) ↔ (𝑌 ∈ (Clsd‘𝐽) ∧ (𝑋 ∩ 𝑌) = ∅)))
21.51.10.2  Neighborhoods
Theorem	neircl 50013	Reverse closure of the neighborhood operation. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by Zhi Wang, 16-Sep-2024.)
⊢ (𝑁 ∈ ((nei‘𝐽)‘𝑆) → 𝐽 ∈ Top)
Theorem	opnneilem 50014*	Lemma factoring out common proof steps of opnneil 50018 and opnneirv 50016. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
Theorem	opnneir 50015*	If something is true for an open neighborhood, it must be true for a neighborhood. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) → ∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓))
Theorem	opnneirv 50016*	A variant of opnneir 50015 with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) → ∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝜒))
Theorem	opnneilv 50017*	The converse of opnneir 50015 with different dummy variables. Note that the second hypothesis could be generalized by adding 𝑦 ∈ 𝐽 to the antecedent. See the proof for details. Although 𝐽 ∈ Top might be redundant here (see neircl 50013), it is listed for explicitness. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 → ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
Theorem	opnneil 50018*	A variant of opnneilv 50017. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 → ∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓)))
Theorem	opnneibid 50019*	The equivalence between neighborhood and open neighborhood. See opnneibid2 50020 for different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 ↔ ∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓)))
Theorem	opnneibid2 50020*	The equivalence between neighborhood and open neighborhood. A variant of opnneibid 50019 with two dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 ↔ ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒)))
21.51.10.3  Subspace topologies
Theorem	restcls2lem 50021	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 50022	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 50023	Lemma for restclssep 50024. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑌)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)
Theorem	restclssep 50024	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.51.10.4  Limits and continuity in topological spaces
Theorem	cnneiima 50025	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.51.10.5  Topological definitions using the reals
Theorem	iooii 50026	Open intervals are open sets of II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴(,)𝐵) ∈ II)
Theorem	icccldii 50027	Closed intervals are closed sets of II. Note that iccss 13545, iccordt 23532, and ordtresticc 23541 are proved from ixxss12 13496, ordtcld3 23517, and ordtrest2 23522, respectively. An alternate proof uses restcldi 23491, dfii2 25203, and icccld 25085. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ∈ (Clsd‘II))
Theorem	i0oii 50028	(0[,)𝐴) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (𝐴 ≤ 1 → (0[,)𝐴) ∈ II)
Theorem	io1ii 50029	(𝐴(,]1) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.)
⊢ (0 ≤ 𝐴 → (𝐴(,]1) ∈ II)
21.51.10.6  Separated sets
Theorem	sepnsepolem1 50030*	Lemma for sepnsepo 50032. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥 ∈ 𝐽 (𝜑 ∧ ∃𝑦 ∈ 𝐽 (𝜓 ∧ 𝜒)))
Theorem	sepnsepolem2 50031*	Open neighborhood and neighborhood is equivalent regarding disjointness. Lemma for sepnsepo 50032. Proof could be shortened by 1 step using ssdisjdr 49919. (Contributed by Zhi Wang, 1-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ((nei‘𝐽)‘𝐷)(𝑥 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ 𝐽 (𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)))
Theorem	sepnsepo 50032*	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 50033	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 50034*	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 50032. The relationship between separatedness and closure is also seen in isnrm 23653, isnrm2 23676, isnrm3 23677. (Contributed by Zhi Wang, 7-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ((𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅)))
Theorem	sepcsepo 50035*	If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo 50032 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 50013, adantr 486, and rexlimiva 3155. (Contributed by Zhi Wang, 8-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	sepfsepc 50036*	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 50037	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 50038*	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.51.10.7  Separated spaces: T0, T1, T2 (Hausdorff) ...
Theorem	isnrm4 50039*	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 50040*	A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm 23635. (Contributed by Zhi Wang, 30-Aug-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ 𝑗 ∃𝑦 ∈ 𝑗 (𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))}
Theorem	dfnrm3 50041*	A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm 23635. (Contributed by Zhi Wang, 2-Sep-2024.)
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝑗)‘𝑐)∃𝑦 ∈ ((nei‘𝑗)‘𝑑)(𝑥 ∩ 𝑦) = ∅)}
Theorem	iscnrm3lem1 50042*	Lemma for iscnrm3 50060. Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ((𝐽 ↾t 𝑥) ∈ Top ∧ 𝜑)))
Theorem	iscnrm3lem2 50043*	Lemma for iscnrm3 50060 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 → ((𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸) → 𝜒)))    &   ⊢ (𝜑 → (∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜓)))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒))
Theorem	iscnrm3lem4 50044	Lemma for iscnrm3lem5 50045 and iscnrm3r 50056. (Contributed by Zhi Wang, 4-Sep-2024.)
⊢ (𝜂 → (𝜓 → 𝜁))    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	iscnrm3lem5 50045*	Lemma for iscnrm3l 50059. (Contributed by Zhi Wang, 3-Sep-2024.)
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊))    &   ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → ((𝜓 → 𝜃) → 𝜎))    ⇒   ⊢ (𝜏 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝜑 → 𝜒) → (𝜂 → (𝜁 → 𝜎))))
Theorem	iscnrm3lem6 50046*	Lemma for iscnrm3lem7 50047. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑊 𝜓 → 𝜒))
Theorem	iscnrm3lem7 50047*	Lemma for iscnrm3rlem8 50055 and iscnrm3llem2 50058 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝑧 = 𝑍 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝑊 → (𝜃 ↔ 𝜏))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → (𝑍 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝜏))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜒))
Theorem	iscnrm3rlem1 50048	Lemma for iscnrm3rlem2 50049. The hypothesis could be generalized to (𝜑 → (𝑆 ∖ 𝑇) ⊆ 𝑋). (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∖ 𝑇) = (𝑆 ∩ (𝑋 ∖ (𝑆 ∩ 𝑇))))
Theorem	iscnrm3rlem2 50049	Lemma for iscnrm3rlem3 50050. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∖ 𝑇) ∈ (Clsd‘(𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ 𝑇)))))
Theorem	iscnrm3rlem3 50050	Lemma for iscnrm3r 50056. 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 50051	Lemma for iscnrm3rlem8 50055. 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 50052	Lemma for iscnrm3rlem6 50053. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ 𝐽)
Theorem	iscnrm3rlem6 50053	Lemma for iscnrm3rlem7 50054. (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽)    &   ⊢ (𝜑 → 𝑂 ⊆ (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))    ⇒   ⊢ (𝜑 → (𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ↔ 𝑂 ∈ 𝐽))
Theorem	iscnrm3rlem7 50054	Lemma for iscnrm3rlem8 50055. 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 50055*	Lemma for iscnrm3r 50056. 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 50056*	Lemma for iscnrm3 50060. 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 50057	Lemma for iscnrm3l 50059. 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 50058*	Lemma for iscnrm3l 50059. 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 46072.) (Contributed by Zhi Wang, 5-Sep-2024.)
⊢ ((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽 ∧ 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍)) ∧ 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) ∧ (𝐶 ∩ 𝐷) = ∅) → (∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) → ∃𝑙 ∈ (𝐽 ↾t 𝑍)∃𝑘 ∈ (𝐽 ↾t 𝑍)(𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅)))
Theorem	iscnrm3l 50059*	Lemma for iscnrm3 50060. 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 50060*	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 50061*	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 50062*	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.51.11  Preordered sets and directed sets using extensible structures
Theorem	isprsd 50063*	Property of being a preordered set (deduction form). (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐾 ∈ Proset ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
21.51.12  Posets and lattices using extensible structures
21.51.12.1  Posets
Theorem	lubeldm2 50064*	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 50065*	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 50066*	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 50067*	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 50068	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 50069	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 50070	Lemma for lubprdm 50071 and lubpr 50072. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ∧ (𝑈‘𝑆) = 𝑌))
Theorem	lubprdm 50071	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 50072	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 50073	Lemma for glbprdm 50074 and glbpr 50075. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌})    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ∧ (𝐺‘𝑆) = 𝑋))
Theorem	glbprdm 50074	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 50075	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 50076*	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 50077*	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 50078*	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 50079*	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 50080	Poset join is idempotent. latjidm 18636 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋)
Theorem	posmidm 50081	Poset meet is idempotent. latmidm 18648 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋)
Theorem	resiposbas 50082	Construct a poset (resipos 50083) for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐾))
Theorem	resipos 50083	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 50084*	There exists a poset for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Poset 𝐵 = (Base‘𝑘))
Theorem	exbasprs 50085*	There exists a preordered set for any base set. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Proset 𝐵 = (Base‘𝑘))
Theorem	basresposfo 50086	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 50087	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 50088	The class of posets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ Poset ∉ V
Theorem	prsnex 50089	The class of preordered sets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.)
⊢ Proset ∉ V
21.51.12.2  Lattices
Theorem	toslat 50090	A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024.)
⊢ (𝐾 ∈ Toset → 𝐾 ∈ Lat)
Theorem	isclatd 50091*	The predicate "is a complete lattice" (deduction form). (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐾))    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝑈)    &   ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → 𝐾 ∈ CLat)
21.51.12.3  Subset order structures
Theorem	intubeu 50092*	Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ (𝐶 ∈ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ ∀𝑦 ∈ 𝐵 (𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦)) ↔ 𝐶 = ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}))
Theorem	unilbeu 50093*	Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}))
Theorem	ipolublem 50094*	Lemma for ipolubdm 50095 and ipolub 50096. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧))))
Theorem	ipolubdm 50095*	The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹))
Theorem	ipolub 50096*	The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18586 is in quantified form. mrelatlub 18736 could potentially be shortened using this. See mrelatlubALT 50103. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	ipoglblem 50097*	Lemma for ipoglbdm 50098 and ipoglb 50099. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋))))
Theorem	ipoglbdm 50098*	The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹))
Theorem	ipoglb 50099*	The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18587 is in quantified form. mrelatglb 18734 could potentially be shortened using this. See mrelatglbALT 50104. (Contributed by Zhi Wang, 29-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐼))    &   ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆})    &   ⊢ (𝜑 → 𝑇 ∈ 𝐹)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇)
Theorem	ipolub0 50100	The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐼))    &   ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹)