Home | Metamath
Proof Explorer Theorem List (p. 458 of 461) | < 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: | Metamath Proof Explorer
(1-28865) |
Hilbert Space Explorer
(28866-30388) |
Users' Mathboxes
(30389-46009) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itsclinecirc0b 45701 | The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space. (Contributed by AV, 2-May-2023.) (Revised by AV, 14-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) & ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → ((𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)) ↔ (𝑍 ∈ 𝑃 ∧ (((𝑍‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑍‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) | ||
Theorem | itsclinecirc0in 45702 | The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space, expressed as intersection. (Contributed by AV, 7-May-2023.) (Revised by AV, 14-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) & ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}}) | ||
Theorem | itsclquadb 45703* | Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 22-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → (∃𝑥 ∈ ℝ (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) | ||
Theorem | itsclquadeu 45704* | Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 23-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝑇 = -(2 · (𝐵 · 𝐶)) & ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → (∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑥) + (𝐵 · 𝑌)) = 𝐶) ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0)) | ||
Theorem | 2itscplem1 45705 | Lemma 1 for 2itscp 45708. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) ⇒ ⊢ (𝜑 → ((((𝐸↑2) · (𝐵↑2)) + ((𝐷↑2) · (𝐴↑2))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) = (((𝐷 · 𝐴) − (𝐸 · 𝐵))↑2)) | ||
Theorem | 2itscplem2 45706 | Lemma 2 for 2itscp 45708. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) ⇒ ⊢ (𝜑 → (𝐶↑2) = ((((𝐷↑2) · (𝐵↑2)) + (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵)))) + ((𝐸↑2) · (𝐴↑2)))) | ||
Theorem | 2itscplem3 45707 | Lemma D for 2itscp 45708. (Contributed by AV, 4-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2)) & ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (𝜑 → 𝑆 = ((((𝐸↑2) · ((𝑅↑2) − (𝐴↑2))) + ((𝐷↑2) · ((𝑅↑2) − (𝐵↑2)))) − (2 · ((𝐷 · 𝐴) · (𝐸 · 𝐵))))) | ||
Theorem | 2itscp 45708 | A condition for a quadratic equation with real coefficients (for the intersection points of a line with a circle) to have (exactly) two different real solutions. (Contributed by AV, 5-Mar-2023.) (Revised by AV, 16-May-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2)) & ⊢ (𝜑 → (𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋)) & ⊢ 𝑄 = ((𝐸↑2) + (𝐷↑2)) & ⊢ 𝑆 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) ⇒ ⊢ (𝜑 → 0 < 𝑆) | ||
Theorem | itscnhlinecirc02plem1 45709 | Lemma 1 for itscnhlinecirc02p 45712. (Contributed by AV, 6-Mar-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2)) & ⊢ (𝜑 → 𝐵 ≠ 𝑌) ⇒ ⊢ (𝜑 → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02plem2 45710 | Lemma 2 for itscnhlinecirc02p 45712. (Contributed by AV, 10-Mar-2023.) |
⊢ 𝐷 = (𝑋 − 𝐴) & ⊢ 𝐸 = (𝐵 − 𝑌) & ⊢ 𝐶 = ((𝐵 · 𝑋) − (𝐴 · 𝑌)) ⇒ ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) ∧ 𝐵 ≠ 𝑌) ∧ (𝑅 ∈ ℝ ∧ ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2))) → 0 < ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02plem3 45711 | Lemma 3 for itscnhlinecirc02p 45712. (Contributed by AV, 10-Mar-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → 0 < ((-(2 · (((𝑌‘1) − (𝑋‘1)) · (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))↑2) − (4 · (((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) · (𝑅↑2))))))) | ||
Theorem | itscnhlinecirc02p 45712* | Intersection of a nonhorizontal line with a circle: A nonhorizontal line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 28-Jan-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐷 = (dist‘𝐸) & ⊢ 𝑍 = {〈1, 𝑥〉, 〈2, 𝑦〉} ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑠 ∈ 𝒫 ℝ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)))) | ||
Theorem | inlinecirc02plem 45713* | Lemma for inlinecirc02p 45714. (Contributed by AV, 7-May-2023.) (Revised by AV, 15-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) & ⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) & ⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) & ⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) & ⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 < 𝐷)) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ((( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)) | ||
Theorem | inlinecirc02p 45714 | Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 9-May-2023.) (Revised by AV, 16-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) ∈ (Pairsproper‘𝑃)) | ||
Theorem | inlinecirc02preu 45715* | Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points, expressed with restricted uniqueness (and without the definition of proper pairs). (Contributed by AV, 16-May-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝐸 = (ℝ^‘𝐼) & ⊢ 𝑃 = (ℝ ↑m 𝐼) & ⊢ 𝑆 = (Sphere‘𝐸) & ⊢ 0 = (𝐼 × {0}) & ⊢ 𝐿 = (LineM‘𝐸) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑝 ∈ 𝒫 𝑃((♯‘𝑝) = 2 ∧ 𝑝 = (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)))) | ||
Theorem | pm4.71da 45716 | Deduction converting a biconditional to a biconditional with conjunction. Variant of pm4.71d 565. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | logic1 45717 | Distribution of implication over biconditional with replacement (deduction form). (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜏))) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | logic1a 45718 | Variant of logic1 45717. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝜓) → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | logic2 45719 | Variant of logic1 45717. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | pm5.32dav 45720 | Distribution of implication over biconditional (deduction form). Variant of pm5.32da 582. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓))) | ||
Theorem | pm5.32dra 45721 | Reverse distribution of implication over biconditional (deduction form). (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | ||
Theorem | exp12bd 45722 | The import-export theorem (impexp 454) for biconditionals (deduction form). (Contributed by Zhi Wang, 3-Sep-2024.) |
⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜏 ∧ 𝜂) → 𝜁))) ⇒ ⊢ (𝜑 → ((𝜓 → (𝜒 → 𝜃)) ↔ (𝜏 → (𝜂 → 𝜁)))) | ||
Theorem | monepilem 45723 | Common lemmas for proving monomorphisms, epimorphisms, and potentially others. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | dtrucor3 45724* | An example of how ax-5 1917 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5247 in the ZF set theory. axc16nf 2264 and euae 2663 demonstrate that the violation of dtru 5247 leads to a model with only one object assuming its existence (ax-6 1975). The conclusion is also provable in the empty model ( see emptyal 1915). See also nf5 2287 and nf5i 2150 for the relation between unconditional ax-5 1917 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 & ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦) ⇒ ⊢ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | ralbidb 45725* | Formula-building rule for restricted universal quantifier and additional condition (deduction form). See ralbidc 45726 for a more generalized form. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃))) | ||
Theorem | ralbidc 45726* | Formula-building rule for restricted universal quantifier and additional condition (deduction form). A variant of ralbidb 45725. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥 ∈ 𝐵 (𝜓 → 𝜃))) | ||
Theorem | r19.41dv 45727* | A complex deduction form of r19.41v 3252. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) | ||
Theorem | rextru 45728 | Two ways of expressing "at least one" element. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ⊤) | ||
Theorem | rmotru 45729 | Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof shortened by BJ, 23-Sep-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑥 ∈ 𝐴 ⊤) | ||
Theorem | reutru 45730 | Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤) | ||
Theorem | reutruALT 45731 | Alternate proof for reutru 45730. (Contributed by Zhi Wang, 23-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 ∈ 𝐴 ⊤) | ||
Theorem | ssdisjd 45732 | Subset preserves disjointness. Deduction form of ssdisj 4359. (Contributed by Zhi Wang, 7-Sep-2024.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝐵 ∩ 𝐶) = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | ssdisjdr 45733 | Subset preserves disjointness. Deduction form of ssdisj 4359. Alternatively this could be proved with ineqcom 4103 in tandem with ssdisjd 45732. (Contributed by Zhi Wang, 7-Sep-2024.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → (𝐶 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐶 ∩ 𝐴) = ∅) | ||
Theorem | disjdifb 45734 | Relative complement is anticommutative regarding intersection. (Contributed by Zhi Wang, 5-Sep-2024.) |
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅ | ||
Theorem | predisj 45735 | Preimages of disjoint sets are disjoint. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑆 ⊆ (◡𝐹 “ 𝐴)) & ⊢ (𝜑 → 𝑇 ⊆ (◡𝐹 “ 𝐵)) ⇒ ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) | ||
Theorem | vsn 45736 | The singleton of the universal class is the empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ {V} = ∅ | ||
Theorem | mosn 45737* | "At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝐴 = {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴) | ||
Theorem | mo0 45738* | "At most one" element in an empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝐴 = ∅ → ∃*𝑥 𝑥 ∈ 𝐴) | ||
Theorem | mosssn 45739* | "At most one" element in a subclass of a singleton. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (𝐴 ⊆ {𝐵} → ∃*𝑥 𝑥 ∈ 𝐴) | ||
Theorem | mo0sn 45740* | Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑦 𝐴 = {𝑦})) | ||
Theorem | mosssn2 45741* | Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝐴 ⊆ {𝑦}) | ||
Theorem | mof0 45742 | There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ ∃*𝑓 𝑓:𝐴⟶∅ | ||
Theorem | mof02 45743* | A variant of mof0 45742. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝐵 = ∅ → ∃*𝑓 𝑓:𝐴⟶𝐵) | ||
Theorem | mof0ALT 45744* | Alternate proof for mof0 45742 with stronger requirements on distinct variables. Uses mo4 2567. (Contributed by Zhi Wang, 19-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃*𝑓 𝑓:𝐴⟶∅ | ||
Theorem | eufsnlem 45745* | There is exactly one function into a singleton. For a simpler hypothesis, see eufsn 45746 assuming ax-rep 5164, or eufsn2 45747 assuming ax-pow 5242 and ax-un 7491. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝐴 × {𝐵}) ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵}) | ||
Theorem | eufsn 45746* | There is exactly one function into a singleton, assuming ax-rep 5164. See eufsn2 45747 for different axiom requirements. If existence is not needed, use mofsn 45748 or mofsn2 45749 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵}) | ||
Theorem | eufsn2 45747* | There is exactly one function into a singleton, assuming ax-pow 5242 and ax-un 7491. Variant of eufsn 45746. If existence is not needed, use mofsn 45748 or mofsn2 45749 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓:𝐴⟶{𝐵}) | ||
Theorem | mofsn 45748* | There is at most one function into a singleton, with fewer axioms than eufsn 45746 and eufsn2 45747. See also mofsn2 45749. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝐵 ∈ 𝑉 → ∃*𝑓 𝑓:𝐴⟶{𝐵}) | ||
Theorem | mofsn2 45749* | There is at most one function into a singleton. An unconditional variant of mofsn 45748, i.e., the singleton could be empty if 𝑌 is a proper class. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝐵 = {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵) | ||
Theorem | mofsssn 45750* | There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024.) |
⊢ (𝐵 ⊆ {𝑌} → ∃*𝑓 𝑓:𝐴⟶𝐵) | ||
Theorem | mofmo 45751* | There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐵 → ∃*𝑓 𝑓:𝐴⟶𝐵) | ||
Theorem | elfvne0 45752 | 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 | fvconstr 45753 | Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌})) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) = 𝑌)) | ||
Theorem | fvconstrn0 45754 | Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 20-Sep-2024.) |
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌})) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐵) ≠ ∅)) | ||
Theorem | fvconstr2 45755 | Two ways of expressing 𝐴𝑅𝐵. (Contributed by Zhi Wang, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹 = (𝑅 × {𝑌})) & ⊢ (𝜑 → 𝑋 ∈ (𝐴𝐹𝐵)) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐵) | ||
Theorem | fvconst0ci 45756 | 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 45757 | 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 45758* | 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 45757 assuming ax-un 7491 (see f1omoALT 45759). (Contributed by Zhi Wang, 19-Sep-2024.) |
⊢ (𝜑 → 𝐹 = (𝐴 × {1o})) ⇒ ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋)) | ||
Theorem | f1omoALT 45759* | 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 45758 without assuming ax-un 7491. (Contributed by Zhi Wang, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐹 = (𝐴 × {1o})) ⇒ ⊢ (𝜑 → ∃*𝑦 𝑦 ∈ (𝐹‘𝑋)) | ||
Theorem | iccin 45760 | Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)[,]if(𝐵 ≤ 𝐷, 𝐵, 𝐷))) | ||
Theorem | iccdisj2 45761 | 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 45762 | 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.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) ∧ 𝐵 < 𝐶) → ((𝐴[,]𝐵) ∩ (𝐶[,]𝐷)) = ∅) | ||
Additional contents for topology. | ||
Theorem | clduni 45763 | 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 45764* | Conditions on open sets are equivalent to conditions on closed sets. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑥 = (∪ 𝐽 ∖ 𝑦)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐽 𝜓 ↔ ∀𝑦 ∈ (Clsd‘𝐽)𝜒)) | ||
Theorem | opndisj 45765 | 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 45766 | 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 45765 with elssuni 4838 replaced by the combination of cldss 21792 and eqid 2739. (Contributed by Zhi Wang, 6-Sep-2024.) |
⊢ (𝑍 = (∪ 𝐽 ∖ 𝑋) → (𝑌 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑍) ↔ (𝑌 ∈ (Clsd‘𝐽) ∧ (𝑋 ∩ 𝑌) = ∅))) | ||
Theorem | neircl 45767 | 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 45768* | Lemma factoring out common proof steps of opnneil 45772 and opnneirv 45770. (Contributed by Zhi Wang, 31-Aug-2024.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒))) | ||
Theorem | opnneir 45769* | 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 45770* | A variant of opnneir 45769 with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓) → ∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝜒)) | ||
Theorem | opnneilv 45771* | The converse of opnneir 45769 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 45767), it is listed for explicitness. (Contributed by Zhi Wang, 31-Aug-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 → ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒))) | ||
Theorem | opnneil 45772* | A variant of opnneilv 45771. (Contributed by Zhi Wang, 31-Aug-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 → ∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓))) | ||
Theorem | opnneieqv 45773* | The equivalence between neighborhood and open neighborhood. See opnneieqvv 45774 for different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 ↔ ∃𝑥 ∈ 𝐽 (𝑆 ⊆ 𝑥 ∧ 𝜓))) | ||
Theorem | opnneieqvv 45774* | The equivalence between neighborhood and open neighborhood. A variant of opnneieqv 45773 with two dummy variables. (Contributed by Zhi Wang, 31-Aug-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑥) → (𝜓 → 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ ((nei‘𝐽)‘𝑆)𝜓 ↔ ∃𝑦 ∈ 𝐽 (𝑆 ⊆ 𝑦 ∧ 𝜒))) | ||
Theorem | restcls2lem 45775 | 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 45776 | 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 45777 | Lemma for restclssep 45778. (Contributed by Zhi Wang, 2-Sep-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑋 = ∪ 𝐽) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝐾 = (𝐽 ↾t 𝑌)) & ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐾)) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) & ⊢ (𝜑 → 𝑇 ⊆ 𝑌) ⇒ ⊢ (𝜑 → (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅) | ||
Theorem | restclssep 45778 | 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 45779 | 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 45780 | Open intervals are open sets of II. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴(,)𝐵) ∈ II) | ||
Theorem | icccldii 45781 | Closed intervals are closed sets of II. Note that iccss 12901, iccordt 21977, and ordtresticc 21986 are proved from ixxss12 12853, ordtcld3 21962, and ordtrest2 21967, respectively. An alternate proof uses restcldi 21936, dfii2 23646, and icccld 23531. (Contributed by Zhi Wang, 8-Sep-2024.) |
⊢ ((0 ≤ 𝐴 ∧ 𝐵 ≤ 1) → (𝐴[,]𝐵) ∈ (Clsd‘II)) | ||
Theorem | i0oii 45782 | (0[,)𝐴) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ (𝐴 ≤ 1 → (0[,)𝐴) ∈ II) | ||
Theorem | io1ii 45783 | (𝐴(,]1) is open in II. (Contributed by Zhi Wang, 9-Sep-2024.) |
⊢ (0 ≤ 𝐴 → (𝐴(,]1) ∈ II) | ||
Theorem | sepnsepolem1 45784* | Lemma for sepnsepo 45786. (Contributed by Zhi Wang, 1-Sep-2024.) |
⊢ (∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥 ∈ 𝐽 (𝜑 ∧ ∃𝑦 ∈ 𝐽 (𝜓 ∧ 𝜒))) | ||
Theorem | sepnsepolem2 45785* | Open neighborhood and neighborhood is equivalent regarding disjointness. Lemma for sepnsepo 45786. Proof could be shortened by 1 step using ssdisjdr 45733. (Contributed by Zhi Wang, 1-Sep-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ((nei‘𝐽)‘𝐷)(𝑥 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ 𝐽 (𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))) | ||
Theorem | sepnsepo 45786* | 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 45787 | 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 45788* | 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 45786. The relationship between separatedness and closure is also seen in isnrm 22098, isnrm2 22121, isnrm3 22122. (Contributed by Zhi Wang, 7-Sep-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) ⇒ ⊢ (𝜑 → ((𝑆 ⊆ ∪ 𝐽 ∧ 𝑇 ⊆ ∪ 𝐽) ∧ ((𝑆 ∩ ((cls‘𝐽)‘𝑇)) = ∅ ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑇) = ∅))) | ||
Theorem | sepcsepo 45789* | If two sets are separated by closed neighborhoods, then they are separated by (open) neighborhoods. See sepnsepo 45786 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 45767, adantr 484, and rexlimiva 3192. (Contributed by Zhi Wang, 8-Sep-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅)) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑆 ⊆ 𝑛 ∧ 𝑇 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) | ||
Theorem | sepfsepc 45790* | 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 45791 | 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 45792* | 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 45793* | 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 45794* | A topological space is normal if any disjoint closed sets can be separated by open neighborhoods. An alternate definition of df-nrm 22080. (Contributed by Zhi Wang, 30-Aug-2024.) |
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ 𝑗 ∃𝑦 ∈ 𝑗 (𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))} | ||
Theorem | dfnrm3 45795* | A topological space is normal if any disjoint closed sets can be separated by neighborhoods. An alternate definition of df-nrm 22080. (Contributed by Zhi Wang, 2-Sep-2024.) |
⊢ Nrm = {𝑗 ∈ Top ∣ ∀𝑐 ∈ (Clsd‘𝑗)∀𝑑 ∈ (Clsd‘𝑗)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ ((nei‘𝑗)‘𝑐)∃𝑦 ∈ ((nei‘𝑗)‘𝑑)(𝑥 ∩ 𝑦) = ∅)} | ||
Theorem | iscnrm3lem1 45796* | Lemma for iscnrm3 45815. Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024.) |
⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ((𝐽 ↾t 𝑥) ∈ Top ∧ 𝜑))) | ||
Theorem | iscnrm3lem2 45797* | Lemma for iscnrm3 45815 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024.) |
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 → ((𝑤 ∈ 𝐷 ∧ 𝑣 ∈ 𝐸) → 𝜒))) & ⊢ (𝜑 → (∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜓))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑤 ∈ 𝐷 ∀𝑣 ∈ 𝐸 𝜒)) | ||
Theorem | iscnrm3lem3 45798 | Lemma for iscnrm3lem4 45799. (Contributed by Zhi Wang, 4-Sep-2024.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓)) | ||
Theorem | iscnrm3lem4 45799 | Lemma for iscnrm3lem5 45800 and iscnrm3r 45811. (Contributed by Zhi Wang, 4-Sep-2024.) |
⊢ (𝜂 → (𝜓 → 𝜁)) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜁 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | iscnrm3lem5 45800* | Lemma for iscnrm3l 45814. (Contributed by Zhi Wang, 3-Sep-2024.) |
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑇) → (𝜒 ↔ 𝜃)) & ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊)) & ⊢ ((𝜏 ∧ 𝜂 ∧ 𝜁) → ((𝜓 → 𝜃) → 𝜎)) ⇒ ⊢ (𝜏 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 (𝜑 → 𝜒) → (𝜂 → (𝜁 → 𝜎)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |