![]() |
Metamath
Proof Explorer Theorem List (p. 479 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssdisjd 47801 | Subset preserves disjointness. Deduction form of ssdisj 4455. (Contributed by Zhi Wang, 7-Sep-2024.) |
β’ (π β π΄ β π΅) & β’ (π β (π΅ β© πΆ) = β ) β β’ (π β (π΄ β© πΆ) = β ) | ||
Theorem | ssdisjdr 47802 | Subset preserves disjointness. Deduction form of ssdisj 4455. Alternatively this could be proved with ineqcom 4198 in tandem with ssdisjd 47801. (Contributed by Zhi Wang, 7-Sep-2024.) |
β’ (π β π΄ β π΅) & β’ (π β (πΆ β© π΅) = β ) β β’ (π β (πΆ β© π΄) = β ) | ||
Theorem | disjdifb 47803 | Relative complement is anticommutative regarding intersection. (Contributed by Zhi Wang, 5-Sep-2024.) |
β’ ((π΄ β π΅) β© (π΅ β π΄)) = β | ||
Theorem | predisj 47804 | Preimages of disjoint sets are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.) |
β’ (π β Fun πΉ) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β π β (β‘πΉ β π΄)) & β’ (π β π β (β‘πΉ β π΅)) β β’ (π β (π β© π) = β ) | ||
Theorem | vsn 47805 | The singleton of the universal class is the empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ {V} = β | ||
Theorem | mosn 47806* | "At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (π΄ = {π΅} β β*π₯ π₯ β π΄) | ||
Theorem | mo0 47807* | "At most one" element in an empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (π΄ = β β β*π₯ π₯ β π΄) | ||
Theorem | mosssn 47808* | "At most one" element in a subclass of a singleton. (Contributed by Zhi Wang, 23-Sep-2024.) |
β’ (π΄ β {π΅} β β*π₯ π₯ β π΄) | ||
Theorem | mo0sn 47809* | Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (β*π₯ π₯ β π΄ β (π΄ = β β¨ βπ¦ π΄ = {π¦})) | ||
Theorem | mosssn2 47810* | Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024.) |
β’ (β*π₯ π₯ β π΄ β βπ¦ π΄ β {π¦}) | ||
Theorem | unilbss 47811* | Superclass of the greatest lower bound. A dual statement of ssintub 4964. (Contributed by Zhi Wang, 29-Sep-2024.) |
β’ βͺ {π₯ β π΅ β£ π₯ β π΄} β π΄ | ||
Theorem | inpw 47812* | Two ways of expressing a collection of subsets as seen in df-ntr 22911, unimax 4942, and others (Contributed by Zhi Wang, 27-Sep-2024.) |
β’ (π΅ β π β (π΄ β© π« π΅) = {π₯ β π΄ β£ π₯ β π΅}) | ||
Theorem | mof0 47813 | There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ β*π π:π΄βΆβ | ||
Theorem | mof02 47814* | A variant of mof0 47813. (Contributed by Zhi Wang, 20-Sep-2024.) |
β’ (π΅ = β β β*π π:π΄βΆπ΅) | ||
Theorem | mof0ALT 47815* | Alternate proof for mof0 47813 with stronger requirements on distinct variables. Uses mo4 2555. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β*π π:π΄βΆβ | ||
Theorem | eufsnlem 47816* | There is exactly one function into a singleton. For a simpler hypothesis, see eufsn 47817 assuming ax-rep 5279, or eufsn2 47818 assuming ax-pow 5359 and ax-un 7734. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (π β π΅ β π) & β’ (π β (π΄ Γ {π΅}) β π) β β’ (π β β!π π:π΄βΆ{π΅}) | ||
Theorem | eufsn 47817* | There is exactly one function into a singleton, assuming ax-rep 5279. See eufsn2 47818 for different axiom requirements. If existence is not needed, use mofsn 47819 or mofsn2 47820 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (π β π΅ β π) & β’ (π β π΄ β π) β β’ (π β β!π π:π΄βΆ{π΅}) | ||
Theorem | eufsn2 47818* | There is exactly one function into a singleton, assuming ax-pow 5359 and ax-un 7734. Variant of eufsn 47817. If existence is not needed, use mofsn 47819 or mofsn2 47820 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (π β π΅ β π) & β’ (π β π΄ β π) β β’ (π β β!π π:π΄βΆ{π΅}) | ||
Theorem | mofsn 47819* | There is at most one function into a singleton, with fewer axioms than eufsn 47817 and eufsn2 47818. See also mofsn2 47820. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (π΅ β π β β*π π:π΄βΆ{π΅}) | ||
Theorem | mofsn2 47820* | There is at most one function into a singleton. An unconditional variant of mofsn 47819, i.e., the singleton could be empty if π is a proper class. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (π΅ = {π} β β*π π:π΄βΆπ΅) | ||
Theorem | mofsssn 47821* | There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024.) |
β’ (π΅ β {π} β β*π π:π΄βΆπ΅) | ||
Theorem | mofmo 47822* | There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (β*π₯ π₯ β π΅ β β*π π:π΄βΆπ΅) | ||
Theorem | mofeu 47823* | The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024.) |
β’ πΊ = (π΄ Γ π΅) & β’ (π β (π΅ = β β π΄ = β )) & β’ (π β β*π₯ π₯ β π΅) β β’ (π β (πΉ:π΄βΆπ΅ β πΉ = πΊ)) | ||
Theorem | elfvne0 47824 | If a function value has a member, then the function is not an empty set (An artifact of our function value definition.) (Contributed by Zhi Wang, 16-Sep-2024.) |
β’ (π΄ β (πΉβπ΅) β πΉ β β ) | ||
Theorem | fdomne0 47825 | A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024.) |
β’ ((πΉ:πβΆπ β§ π β β ) β (πΉ β β β§ π β β )) | ||
Theorem | f1sn2g 47826 | A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.) |
β’ ((π΄ β π β§ πΉ:{π΄}βΆπ΅) β πΉ:{π΄}β1-1βπ΅) | ||
Theorem | f102g 47827 | A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.) |
β’ ((π΄ = β β§ πΉ:π΄βΆπ΅) β πΉ:π΄β1-1βπ΅) | ||
Theorem | f1mo 47828* | A function that maps a set with at most one element to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024.) |
β’ ((β*π₯ π₯ β π΄ β§ πΉ:π΄βΆπ΅) β πΉ:π΄β1-1βπ΅) | ||
Theorem | f002 47829 | A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024.) |
β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (π΅ = β β π΄ = β )) | ||
Theorem | map0cor 47830* | A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β ((π΅ = β β π΄ = β ) β βπ π:π΄βΆπ΅)) | ||
Theorem | fvconstr 47831 | Two ways of expressing π΄π π΅. (Contributed by Zhi Wang, 18-Sep-2024.) |
β’ (π β πΉ = (π Γ {π})) & β’ (π β π β π) & β’ (π β π β β ) β β’ (π β (π΄π π΅ β (π΄πΉπ΅) = π)) | ||
Theorem | fvconstrn0 47832 | Two ways of expressing π΄π π΅. (Contributed by Zhi Wang, 20-Sep-2024.) |
β’ (π β πΉ = (π Γ {π})) & β’ (π β π β π) & β’ (π β π β β ) β β’ (π β (π΄π π΅ β (π΄πΉπ΅) β β )) | ||
Theorem | fvconstr2 47833 | Two ways of expressing π΄π π΅. (Contributed by Zhi Wang, 18-Sep-2024.) |
β’ (π β πΉ = (π Γ {π})) & β’ (π β π β (π΄πΉπ΅)) β β’ (π β π΄π π΅) | ||
Theorem | fvconst0ci 47834 | A constant function's value is either the constant or the empty set. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024.) |
β’ π΅ β V & β’ π = ((π΄ Γ {π΅})βπ) β β’ (π = β β¨ π = π΅) | ||
Theorem | fvconstdomi 47835 | A constant function's value is dominated by the constant. (An artifact of our function value definition.) (Contributed by Zhi Wang, 18-Sep-2024.) |
β’ π΅ β V β β’ ((π΄ Γ {π΅})βπ) βΌ π΅ | ||
Theorem | f1omo 47836* | 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 47835 assuming ax-un 7734 (see f1omoALT 47837). (Contributed by Zhi Wang, 19-Sep-2024.) |
β’ (π β πΉ = (π΄ Γ {1o})) β β’ (π β β*π¦ π¦ β (πΉβπ)) | ||
Theorem | f1omoALT 47837* | 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 47836 without assuming ax-un 7734. (Contributed by Zhi Wang, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β πΉ = (π΄ Γ {1o})) β β’ (π β β*π¦ π¦ β (πΉβπ)) | ||
Theorem | iccin 47838 | Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β ((π΄[,]π΅) β© (πΆ[,]π·)) = (if(π΄ β€ πΆ, πΆ, π΄)[,]if(π΅ β€ π·, π΅, π·))) | ||
Theorem | iccdisj2 47839 | 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 47840 | 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 | mreuniss 47841 | The union of a collection of closed sets is a subset. (Contributed by Zhi Wang, 29-Sep-2024.) |
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β βͺ π β π) | ||
Additional contents for topology. | ||
Theorem | clduni 47842 | 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 | opncldeqv 47843* | Conditions on open sets are equivalent to conditions on closed sets. (Contributed by Zhi Wang, 30-Aug-2024.) |
β’ (π β π½ β Top) & β’ ((π β§ π₯ = (βͺ π½ β π¦)) β (π β π)) β β’ (π β (βπ₯ β π½ π β βπ¦ β (Clsdβπ½)π)) | ||
Theorem | opndisj 47844 | 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 47845 | 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 47844 with elssuni 4935 replaced by the combination of cldss 22920 and eqid 2727. (Contributed by Zhi Wang, 6-Sep-2024.) |
β’ (π = (βͺ π½ β π) β (π β ((Clsdβπ½) β© π« π) β (π β (Clsdβπ½) β§ (π β© π) = β ))) | ||
Theorem | neircl 47846 | 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 47847* | Lemma factoring out common proof steps of opnneil 47851 and opnneirv 47849. (Contributed by Zhi Wang, 31-Aug-2024.) |
β’ ((π β§ π₯ = π¦) β (π β π)) β β’ (π β (βπ₯ β π½ (π β π₯ β§ π) β βπ¦ β π½ (π β π¦ β§ π))) | ||
Theorem | opnneir 47848* | 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 47849* | A variant of opnneir 47848 with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.) |
β’ (π β π½ β Top) & β’ ((π β§ π₯ = π¦) β (π β π)) β β’ (π β (βπ₯ β π½ (π β π₯ β§ π) β βπ¦ β ((neiβπ½)βπ)π)) | ||
Theorem | opnneilv 47850* | The converse of opnneir 47848 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 47846), it is listed for explicitness. (Contributed by Zhi Wang, 31-Aug-2024.) |
β’ (π β π½ β Top) & β’ ((π β§ π¦ β π₯) β (π β π)) β β’ (π β (βπ₯ β ((neiβπ½)βπ)π β βπ¦ β π½ (π β π¦ β§ π))) | ||
Theorem | opnneil 47851* | A variant of opnneilv 47850. (Contributed by Zhi Wang, 31-Aug-2024.) |
β’ (π β π½ β Top) & β’ ((π β§ π¦ β π₯) β (π β π)) & β’ ((π β§ π₯ = π¦) β (π β π)) β β’ (π β (βπ₯ β ((neiβπ½)βπ)π β βπ₯ β π½ (π β π₯ β§ π))) | ||
Theorem | opnneieqv 47852* | The equivalence between neighborhood and open neighborhood. See opnneieqvv 47853 for different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.) |
β’ (π β π½ β Top) & β’ ((π β§ π¦ β π₯) β (π β π)) & β’ ((π β§ π₯ = π¦) β (π β π)) β β’ (π β (βπ₯ β ((neiβπ½)βπ)π β βπ₯ β π½ (π β π₯ β§ π))) | ||
Theorem | opnneieqvv 47853* | The equivalence between neighborhood and open neighborhood. A variant of opnneieqv 47852 with two dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.) |
β’ (π β π½ β Top) & β’ ((π β§ π¦ β π₯) β (π β π)) & β’ ((π β§ π₯ = π¦) β (π β π)) β β’ (π β (βπ₯ β ((neiβπ½)βπ)π β βπ¦ β π½ (π β π¦ β§ π))) | ||
Theorem | restcls2lem 47854 | 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 47855 | 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 47856 | Lemma for restclssep 47857. (Contributed by Zhi Wang, 2-Sep-2024.) |
β’ (π β π½ β Top) & β’ (π β π = βͺ π½) & β’ (π β π β π) & β’ (π β πΎ = (π½ βΎt π)) & β’ (π β π β (ClsdβπΎ)) & β’ (π β (π β© π) = β ) & β’ (π β π β π) β β’ (π β (((clsβπ½)βπ) β© π) = β ) | ||
Theorem | restclssep 47857 | 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βπ½)βπ) β© π) = β )) | ||
Theorem | cnneiima 47858 | 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βπ½)βπ)) | ||
Theorem | iooii 47859 | Open intervals are open sets of II. (Contributed by Zhi Wang, 9-Sep-2024.) |
β’ ((0 β€ π΄ β§ π΅ β€ 1) β (π΄(,)π΅) β II) | ||
Theorem | icccldii 47860 | Closed intervals are closed sets of II. Note that iccss 13416, iccordt 23105, and ordtresticc 23114 are proved from ixxss12 13368, ordtcld3 23090, and ordtrest2 23095, respectively. An alternate proof uses restcldi 23064, dfii2 24789, and icccld 24670. (Contributed by Zhi Wang, 8-Sep-2024.) |
β’ ((0 β€ π΄ β§ π΅ β€ 1) β (π΄[,]π΅) β (ClsdβII)) | ||
Theorem | i0oii 47861 | (0[,)π΄) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.) |
β’ (π΄ β€ 1 β (0[,)π΄) β II) | ||
Theorem | io1ii 47862 | (π΄(,]1) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.) |
β’ (0 β€ π΄ β (π΄(,]1) β II) | ||
Theorem | sepnsepolem1 47863* | Lemma for sepnsepo 47865. (Contributed by Zhi Wang, 1-Sep-2024.) |
β’ (βπ₯ β π½ βπ¦ β π½ (π β§ π β§ π) β βπ₯ β π½ (π β§ βπ¦ β π½ (π β§ π))) | ||
Theorem | sepnsepolem2 47864* | Open neighborhood and neighborhood is equivalent regarding disjointness. Lemma for sepnsepo 47865. Proof could be shortened by 1 step using ssdisjdr 47802. (Contributed by Zhi Wang, 1-Sep-2024.) |
β’ (π β π½ β Top) β β’ (π β (βπ¦ β ((neiβπ½)βπ·)(π₯ β© π¦) = β β βπ¦ β π½ (π· β π¦ β§ (π₯ β© π¦) = β ))) | ||
Theorem | sepnsepo 47865* | 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 47866 | 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 47867* | 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 47865. The relationship between separatedness and closure is also seen in isnrm 23226, isnrm2 23249, isnrm3 23250. (Contributed by Zhi Wang, 7-Sep-2024.) |
β’ (π β π½ β Top) & β’ (π β βπ β π½ βπ β π½ (π β π β§ π β π β§ (π β© π) = β )) β β’ (π β ((π β βͺ π½ β§ π β βͺ π½) β§ ((π β© ((clsβπ½)βπ)) = β β§ (((clsβπ½)βπ) β© π) = β ))) | ||
Theorem | sepcsepo 47868* | If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo 47865 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 47846, adantr 480, and rexlimiva 3142. (Contributed by Zhi Wang, 8-Sep-2024.) |
β’ (π β π½ β Top) & β’ (π β βπ β ((neiβπ½)βπ)βπ β ((neiβπ½)βπ)(π β (Clsdβπ½) β§ π β (Clsdβπ½) β§ (π β© π) = β )) β β’ (π β βπ β π½ βπ β π½ (π β π β§ π β π β§ (π β© π) = β )) | ||
Theorem | sepfsepc 47869* | 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 47870 | 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 47871* | 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βπ½))) | ||
Theorem | isnrm4 47872* | 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 47873* | A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm 23208. (Contributed by Zhi Wang, 30-Aug-2024.) |
β’ Nrm = {π β Top β£ βπ β (Clsdβπ)βπ β (Clsdβπ)((π β© π) = β β βπ₯ β π βπ¦ β π (π β π₯ β§ π β π¦ β§ (π₯ β© π¦) = β ))} | ||
Theorem | dfnrm3 47874* | A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm 23208. (Contributed by Zhi Wang, 2-Sep-2024.) |
β’ Nrm = {π β Top β£ βπ β (Clsdβπ)βπ β (Clsdβπ)((π β© π) = β β βπ₯ β ((neiβπ)βπ)βπ¦ β ((neiβπ)βπ)(π₯ β© π¦) = β )} | ||
Theorem | iscnrm3lem1 47875* | Lemma for iscnrm3 47894. Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024.) |
β’ (π½ β Top β (βπ₯ β π΄ π β βπ₯ β π΄ ((π½ βΎt π₯) β Top β§ π))) | ||
Theorem | iscnrm3lem2 47876* | Lemma for iscnrm3 47894 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024.) |
β’ (π β (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π β ((π€ β π· β§ π£ β πΈ) β π))) & β’ (π β (βπ€ β π· βπ£ β πΈ π β ((π₯ β π΄ β§ π¦ β π΅ β§ π§ β πΆ) β π))) β β’ (π β (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π β βπ€ β π· βπ£ β πΈ π)) | ||
Theorem | iscnrm3lem3 47877 | Lemma for iscnrm3lem4 47878. (Contributed by Zhi Wang, 4-Sep-2024.) |
β’ (((π β§ π) β§ (π β§ π)) β ((π β§ π β§ π) β§ π)) | ||
Theorem | iscnrm3lem4 47878 | Lemma for iscnrm3lem5 47879 and iscnrm3r 47890. (Contributed by Zhi Wang, 4-Sep-2024.) |
β’ (π β (π β π)) & β’ ((π β§ π β§ π) β π) & β’ ((π β§ π β§ π) β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | iscnrm3lem5 47879* | Lemma for iscnrm3l 47893. (Contributed by Zhi Wang, 3-Sep-2024.) |
β’ ((π₯ = π β§ π¦ = π) β (π β π)) & β’ ((π₯ = π β§ π¦ = π) β (π β π)) & β’ ((π β§ π β§ π) β (π β π β§ π β π)) & β’ ((π β§ π β§ π) β ((π β π) β π)) β β’ (π β (βπ₯ β π βπ¦ β π (π β π) β (π β (π β π)))) | ||
Theorem | iscnrm3lem6 47880* | Lemma for iscnrm3lem7 47881. (Contributed by Zhi Wang, 5-Sep-2024.) |
β’ ((π β§ (π₯ β π β§ π¦ β π) β§ π) β π) β β’ (π β (βπ₯ β π βπ¦ β π π β π)) | ||
Theorem | iscnrm3lem7 47881* | Lemma for iscnrm3rlem8 47889 and iscnrm3llem2 47892 involving restricted existential quantifications. (Contributed by Zhi Wang, 5-Sep-2024.) |
β’ (π§ = π β (π β π)) & β’ (π€ = π β (π β π)) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΅) β§ π) β (π β πΆ β§ π β π· β§ π)) β β’ (π β (βπ₯ β π΄ βπ¦ β π΅ π β βπ§ β πΆ βπ€ β π· π)) | ||
Theorem | iscnrm3rlem1 47882 | Lemma for iscnrm3rlem2 47883. The hypothesis could be generalized to (π β (π β π) β π). (Contributed by Zhi Wang, 5-Sep-2024.) |
β’ (π β π β π) β β’ (π β (π β π) = (π β© (π β (π β© π)))) | ||
Theorem | iscnrm3rlem2 47883 | Lemma for iscnrm3rlem3 47884. (Contributed by Zhi Wang, 5-Sep-2024.) |
β’ (π β π½ β Top) & β’ (π β π β βͺ π½) β β’ (π β (((clsβπ½)βπ) β π) β (Clsdβ(π½ βΎt (βͺ π½ β (((clsβπ½)βπ) β© π))))) | ||
Theorem | iscnrm3rlem3 47884 | Lemma for iscnrm3r 47890. 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 47885 | Lemma for iscnrm3rlem8 47889. 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 47886 | Lemma for iscnrm3rlem6 47887. (Contributed by Zhi Wang, 5-Sep-2024.) |
β’ (π β π½ β Top) & β’ (π β π β βͺ π½) & β’ (π β π β βͺ π½) β β’ (π β (βͺ π½ β (((clsβπ½)βπ) β© ((clsβπ½)βπ))) β π½) | ||
Theorem | iscnrm3rlem6 47887 | Lemma for iscnrm3rlem7 47888. (Contributed by Zhi Wang, 5-Sep-2024.) |
β’ (π β π½ β Top) & β’ (π β π β βͺ π½) & β’ (π β π β βͺ π½) & β’ (π β π β (βͺ π½ β (((clsβπ½)βπ) β© ((clsβπ½)βπ)))) β β’ (π β (π β (π½ βΎt (βͺ π½ β (((clsβπ½)βπ) β© ((clsβπ½)βπ)))) β π β π½)) | ||
Theorem | iscnrm3rlem7 47888 | Lemma for iscnrm3rlem8 47889. 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 47889* | Lemma for iscnrm3r 47890. 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 47890* | Lemma for iscnrm3 47894. 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 47891 | Lemma for iscnrm3l 47893. 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 47892* | Lemma for iscnrm3l 47893. 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 44342.) (Contributed by Zhi Wang, 5-Sep-2024.) |
β’ ((π½ β Top β§ (π β π« βͺ π½ β§ πΆ β (Clsdβ(π½ βΎt π)) β§ π· β (Clsdβ(π½ βΎt π))) β§ (πΆ β© π·) = β ) β (βπ β π½ βπ β π½ (πΆ β π β§ π· β π β§ (π β© π) = β ) β βπ β (π½ βΎt π)βπ β (π½ βΎt π)(πΆ β π β§ π· β π β§ (π β© π) = β ))) | ||
Theorem | iscnrm3l 47893* | Lemma for iscnrm3 47894. 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 47894* | 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 47895* | 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 47896* | 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βπ½)βπ‘)(π β© π) = β ))) | ||
Theorem | isprsd 47897* | Property of being a preordered set (deduction form). (Contributed by Zhi Wang, 18-Sep-2024.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β β€ = (leβπΎ)) & β’ (π β πΎ β π) β β’ (π β (πΎ β Proset β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) | ||
Theorem | lubeldm2 47898* | 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 47899* | 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 47900* | 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 π β (π β π΅ β§ βπ₯ β π΅ π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |