HomeTheorem List (p. 489 of 492)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 489 of 492) | < 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-30963) |
Hilbert Space Explorer
(30964-32486) |
Users' Mathboxes
(32487-49161) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | glbeldm2d 48801* | 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 48802 | 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 48803 | 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 48804 | Lemma for lubprdm 48805 and lubpr 48806. (Contributed by Zhi Wang, 26-Sep-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌}) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ∧ (𝑈‘𝑆) = 𝑌)) | ||
| Theorem | lubprdm 48805 | 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 48806 | 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 48807 | Lemma for glbprdm 48808 and glbpr 48809. (Contributed by Zhi Wang, 26-Sep-2024.) |
| ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑆 = {𝑋, 𝑌}) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ∧ (𝐺‘𝑆) = 𝑋)) | ||
| Theorem | glbprdm 48808 | 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 48809 | 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 48810* | 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 48811* | 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 48812* | 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 48813* | 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 48814 | Poset join is idempotent. latjidm 18529 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋) | ||
| Theorem | posmidm 48815 | Poset meet is idempotent. latmidm 18541 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋) | ||
| Theorem | toslat 48816 | A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024.) |
| ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Lat) | ||
| Theorem | isclatd 48817* | The predicate "is a complete lattice" (deduction form). (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝑈 = (lub‘𝐾)) & ⊢ (𝜑 → 𝐺 = (glb‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝑈) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝐺) ⇒ ⊢ (𝜑 → 𝐾 ∈ CLat) | ||
| Theorem | intubeu 48818* | Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ (𝐶 ∈ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ ∀𝑦 ∈ 𝐵 (𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦)) ↔ 𝐶 = ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥})) | ||
| Theorem | unilbeu 48819* | Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴})) | ||
| Theorem | ipolublem 48820* | Lemma for ipolubdm 48821 and ipolub 48822. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧)))) | ||
| Theorem | ipolubdm 48821* | The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹)) | ||
| Theorem | ipolub 48822* | The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18481 is in quantified form. mrelatlub 18629 could potentially be shortened using this. See mrelatlubALT 48829. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
| Theorem | ipoglblem 48823* | Lemma for ipoglbdm 48824 and ipoglb 48825. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋)))) | ||
| Theorem | ipoglbdm 48824* | The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹)) | ||
| Theorem | ipoglb 48825* | The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18482 is in quantified form. mrelatglb 18627 could potentially be shortened using this. See mrelatglbALT 48830. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇) | ||
| Theorem | ipolub0 48826 | The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹) | ||
| Theorem | ipolub00 48827 | 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 48828 | The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹) | ||
| Theorem | mrelatlubALT 48829 | 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 48830 | 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 48831 | A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
| Theorem | topclat 48832 | A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat) | ||
| Theorem | toplatglb0 48833 | The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽) | ||
| Theorem | toplatlub 48834 | Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑆 ⊆ 𝐽) & ⊢ 𝑈 = (lub‘𝐼) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆) | ||
| Theorem | toplatglb 48835 | 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 48836 | Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∨ = (join‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵)) | ||
| Theorem | toplatmeet 48837 | Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∧ = (meet‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵)) | ||
| Theorem | topdlat 48838 | A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat) | ||
| Theorem | elmgpcntrd 48839* | The center of a ring. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntr‘𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑋)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑍) | ||
| Theorem | asclelbas 48840 | 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 48841 | Alternate proof for asclelbas 48840. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊)) | ||
| Theorem | asclcntr 48842 | 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 48843 |
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 21910, assa2ass2 21911, and asclval 21927, by setting 𝑋 and 𝑌 the multiplicative identity of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ∗ = (.r‘𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶 ∗ 𝐷)) = (𝐴‘(𝐷 ∗ 𝐶))) | ||
| Theorem | catprslem 48844* | Lemma for catprs 48845. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
| Theorem | catprs 48845* | A preorder can be extracted from a category. See catprs2 48846 for more details. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | catprs2 48846* | A category equipped with the induced preorder, where an object 𝑥 is defined to be "less than or equal to" 𝑦 iff there is a morphism from 𝑥 to 𝑦, is a preordered set, or a proset. The category might not be thin. See catprsc 48847 and catprsc2 48848 for constructions satisfying the hypothesis "catprs.1". See catprs 48845 for a more primitive version. See prsthinc 48980 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
| Theorem | catprsc 48847* | A construction of the preorder induced by a category. See catprs2 48846 for details. See also catprsc2 48848 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | catprsc2 48848* | An alternate construction of the preorder induced by a category. See catprs2 48846 for details. See also catprsc 48847 for a different construction. The two constructions are different because df-cat 17722 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐻𝑦) ≠ ∅}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | endmndlem 48849 | A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 49012 for converting a monoid to a category. Lemma for bj-endmnd 37313. (Contributed by Zhi Wang, 25-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀)) & ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (+g‘𝑀)) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mnd) | ||
| Theorem | idmon 48850 | An identity arrow, or an identity morphism, is a monomorphism. (Contributed by Zhi Wang, 21-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝑀 = (Mono‘𝐶) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝑀𝑋)) | ||
| Theorem | idepi 48851 | An identity arrow, or an identity morphism, is an epimorphism. (Contributed by Zhi Wang, 21-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ 𝐸 = (Epi‘𝐶) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐸𝑋)) | ||
| Theorem | isisod 48852 | The predicate "is an isomorphism" (deduction form). (Contributed by Zhi Wang, 16-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑋)) & ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑋)𝐹) = ( 1 ‘𝑋)) & ⊢ (𝜑 → (𝐹(⟨𝑌, 𝑋⟩ · 𝑌)𝐺) = ( 1 ‘𝑌)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) | ||
| Theorem | upeu2lem 48853* | Lemma for upeu2 48867. There exists a unique morphism from 𝑌 to 𝑍 that commutes if 𝐹:𝑋⟶𝑌 is an isomorphism. (Contributed by Zhi Wang, 20-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑍)) ⇒ ⊢ (𝜑 → ∃!𝑘 ∈ (𝑌𝐻𝑍)𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)) | ||
| Theorem | funcrcl2 48854 | Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐷 ∈ Cat) | ||
| Theorem | funcrcl3 48855 | Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → 𝐸 ∈ Cat) | ||
| Theorem | funcf2lem 48856* | A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 1-Oct-2024.) |
| ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | funcf2lem2 48857* | A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = (𝐸‘𝐶) ⇒ ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))) | ||
| Theorem | 0funclem 48858 | Lemma for 0func 48859. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ (𝜒 ↔ 𝜂) & ⊢ (𝜃 ↔ 𝜁) & ⊢ 𝜏 ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜂 ∧ 𝜁))) | ||
| Theorem | 0func 48859 | The functor from the empty category. (Contributed by Zhi Wang, 7-Oct-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → (∅ Func 𝐶) = {⟨∅, ∅⟩}) | ||
| Theorem | rescofuf 48860 | The restriction of functor composition is a function from product functor space to functor space. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ ( ∘func ↾ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))):((𝐷 Func 𝐸) × (𝐶 Func 𝐷))⟶(𝐶 Func 𝐸) | ||
| Theorem | upciclem1 48861* | Lemma for upcic 48865, upeu 48866, and upeu2 48867. (Contributed by Zhi Wang, 16-Sep-2025.) |
| ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑛 ∈ (𝑍𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑛 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) ⇒ ⊢ (𝜑 → ∃!𝑙 ∈ (𝑋𝐻𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑙)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) | ||
| Theorem | upciclem2 48862 | Lemma for upciclem3 48863 and upeu2 48867. (Contributed by Zhi Wang, 19-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) ⇒ ⊢ (𝜑 → (((𝑋𝐺𝑍)‘(𝐿(⟨𝑋, 𝑌⟩ · 𝑍)𝐾))(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑍))𝑀) = (((𝑌𝐺𝑍)‘𝐿)(⟨𝑊, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑍))𝑁)) | ||
| Theorem | upciclem3 48863* | Lemma for upciclem4 48864. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (𝑌𝐻𝑋)) & ⊢ (𝜑 → 𝑀 = (((𝑌𝐺𝑋)‘𝐿)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑋))𝑁)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) ⇒ ⊢ (𝜑 → (𝐿(⟨𝑋, 𝑌⟩ · 𝑋)𝐾) = ((Id‘𝐷)‘𝑋)) | ||
| Theorem | upciclem4 48864* | Lemma for upcic 48865 and upeu 48866. (Contributed by Zhi Wang, 19-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) & ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)) ⇒ ⊢ (𝜑 → (𝑋( ≃𝑐 ‘𝐷)𝑌 ∧ ∃𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))) | ||
| Theorem | upcic 48865* | A universal property defines an object up to isomorphism given its existence. (Contributed by Zhi Wang, 17-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) & ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)) ⇒ ⊢ (𝜑 → 𝑋( ≃𝑐 ‘𝐷)𝑌) | ||
| Theorem | upeu 48866* | A universal property defines an essentially unique (strong form) pair of object 𝑋 and morphism 𝑀 if it exists. (Contributed by Zhi Wang, 19-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌))) & ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)) ⇒ ⊢ (𝜑 → ∃!𝑟 ∈ (𝑋(Iso‘𝐷)𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) | ||
| Theorem | upeu2 48867* | Generate new universal morphism through isomorphism from existing universal object. (Contributed by Zhi Wang, 20-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐶) & ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋))) & ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀)) & ⊢ 𝐼 = (Iso‘𝐷) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀)) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)) ∧ ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))) | ||
| Syntax | cup 48868 | Extend class notation with the class of universal properties. |
| class UP | ||
| Definition | df-up 48869* |
Definition of the class of universal properties.
Given categories 𝐷 and 𝐸, if 𝐹:𝐷⟶𝐸 is a functor and 𝑊 an object of 𝐸, a universal pair from 𝑊 to 𝐹 is a pair ⟨𝑋, 𝑀⟩ consisting of an object 𝑋 of 𝐷 and a morphism 𝑀:𝑊⟶𝐹𝑋 of 𝐸, such that to every pair ⟨𝑦, 𝑔⟩ with 𝑦 an object of 𝐷 and 𝑔:𝑊⟶𝐹𝑦 a morphism of 𝐸, there is a unique morphism 𝑘:𝑋⟶𝑦 of 𝐷 with 𝐹𝑘 ⚬ 𝑀 = 𝑔. Such property is commonly referred to as a universal property. In our definition, it is denoted as 𝑋(𝐹(𝐷UP𝐸)𝑊)𝑀. Note that the universal pair is termed differently as "universal arrow" in p. 55 of Mac Lane, Saunders, Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf (retrieved 6 Oct 2025). Interestingly, the "universal arrow" is referring to the morphism 𝑀 instead of the pair near the end of the same piece of the text, causing name collision. The name "universal arrow" is also adopted in papers such as https://arxiv.org/pdf/2212.08981. Alternatively, the universal pair is called the "universal morphism" in Wikipedia (https://en.wikipedia.org/wiki/Universal_property) as well as published works, e.g., https://arxiv.org/pdf/2412.12179. But the pair ⟨𝑋, 𝑀⟩ should be named differently as the morphism 𝑀, and thus we call 𝑋 the universal object, 𝑀 the universal morphism, and ⟨𝑋, 𝑀⟩ the universal pair. Given its existence, such universal pair is essentially unique (upeu3 48883), and can be generated from an existing universal pair by isomorphisms (upeu4 48884). See also oppcup 48885 for the dual concept. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ UP = (𝑑 ∈ V, 𝑒 ∈ V ↦ ⦋(Base‘𝑑) / 𝑏⦌⦋(Base‘𝑒) / 𝑐⦌⦋(Hom ‘𝑑) / ℎ⦌⦋(Hom ‘𝑒) / 𝑗⦌⦋(comp‘𝑒) / 𝑜⦌(𝑓 ∈ (𝑑 Func 𝑒), 𝑤 ∈ 𝑐 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝑏 ∧ 𝑚 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝑏 ∀𝑔 ∈ (𝑤𝑗((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥ℎ𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑜((1st ‘𝑓)‘𝑦))𝑚))})) | ||
| Theorem | reldmup 48870 | The domain of UP is a relation. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ Rel dom UP | ||
| Theorem | upfval 48871* | Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) ⇒ ⊢ (𝐷UP𝐸) = (𝑓 ∈ (𝐷 Func 𝐸), 𝑤 ∈ 𝐶 ↦ {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑤𝐽((1st ‘𝑓)‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑤𝐽((1st ‘𝑓)‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥(2nd ‘𝑓)𝑦)‘𝑘)(⟨𝑤, ((1st ‘𝑓)‘𝑥)⟩𝑂((1st ‘𝑓)‘𝑦))𝑚))}) | ||
| Theorem | upfval2 48872* | Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸)) ⇒ ⊢ (𝜑 → (𝐹(𝐷UP𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽((1st ‘𝐹)‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽((1st ‘𝐹)‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥(2nd ‘𝐹)𝑦)‘𝑘)(⟨𝑊, ((1st ‘𝐹)‘𝑥)⟩𝑂((1st ‘𝐹)‘𝑦))𝑚))}) | ||
| Theorem | upfval3 48873* | Function value of the class of universal properties. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → (⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊) = {⟨𝑥, 𝑚⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑚 ∈ (𝑊𝐽(𝐹‘𝑥))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑥𝐻𝑦)𝑔 = (((𝑥𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑥)⟩𝑂(𝐹‘𝑦))𝑚))}) | ||
| Theorem | isuplem 48874* | Lemma for isup 48875 and other theorems. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) ⇒ ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ∧ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)))) | ||
| Theorem | isup 48875* | The predicate "is a universal pair". (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) ⇒ ⊢ (𝜑 → (𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀))) | ||
| Theorem | relup 48876 | The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ Rel (𝐹(𝐷UP𝐸)𝑊) | ||
| Theorem | uprcl 48877 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝑋 ∈ (𝐹(𝐷UP𝐸)𝑊) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝑊 ∈ 𝐶)) | ||
| Theorem | uprcl2 48878 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) | ||
| Theorem | uprcl3 48879 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀) & ⊢ 𝐶 = (Base‘𝐸) ⇒ ⊢ (𝜑 → 𝑊 ∈ 𝐶) | ||
| Theorem | uprcl4 48880 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀) & ⊢ 𝐵 = (Base‘𝐷) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐵) | ||
| Theorem | uprcl5 48881 | Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀) & ⊢ 𝐽 = (Hom ‘𝐸) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝑊𝐽(𝐹‘𝑋))) | ||
| Theorem | isup2 48882* | The universal property of a universal pair. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ 𝑂 = (comp‘𝐸) & ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀) ⇒ ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ (𝑊𝐽(𝐹‘𝑦))∃!𝑘 ∈ (𝑋𝐻𝑦)𝑔 = (((𝑋𝐺𝑦)‘𝑘)(⟨𝑊, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑦))𝑀)) | ||
| Theorem | upeu3 48883* | The universal pair ⟨𝑋, 𝑀⟩ from object 𝑊 to functor ⟨𝐹, 𝐺⟩ is essentially unique (strong form) if it exists. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ (𝜑 → 𝐼 = (Iso‘𝐷)) & ⊢ (𝜑 → ⚬ = (⟨𝑊, (𝐹‘𝑋)⟩(comp‘𝐸)(𝐹‘𝑌))) & ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀) & ⊢ (𝜑 → 𝑌(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑁) ⇒ ⊢ (𝜑 → ∃!𝑟 ∈ (𝑋𝐼𝑌)𝑁 = (((𝑋𝐺𝑌)‘𝑟) ⚬ 𝑀)) | ||
| Theorem | upeu4 48884 | Generate a new universal morphism through an isomorphism from an existing universal object, and pair with the codomain of the isomorphism to form a universal pair. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → 𝐼 = (Iso‘𝐷)) & ⊢ (𝜑 → ⚬ = (⟨𝑊, (𝐹‘𝑋)⟩(comp‘𝐸)(𝐹‘𝑌))) & ⊢ (𝜑 → 𝑋(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑀) & ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌)) & ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾) ⚬ 𝑀)) ⇒ ⊢ (𝜑 → 𝑌(⟨𝐹, 𝐺⟩(𝐷UP𝐸)𝑊)𝑁) | ||
| Theorem | oppcup 48885* | The universal pair ⟨𝑋, 𝑀⟩ from a functor to an object is universal from an object to a functor in the opposite category. (Contributed by Zhi Wang, 24-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝐷) & ⊢ 𝐶 = (Base‘𝐸) & ⊢ 𝐻 = (Hom ‘𝐷) & ⊢ 𝐽 = (Hom ‘𝐸) & ⊢ ∙ = (comp‘𝐸) & ⊢ (𝜑 → 𝑊 ∈ 𝐶) & ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ((𝐹‘𝑋)𝐽𝑊)) & ⊢ 𝑂 = (oppCat‘𝐷) & ⊢ 𝑃 = (oppCat‘𝐸) ⇒ ⊢ (𝜑 → (𝑋(⟨𝐹, tpos 𝐺⟩(𝑂UP𝑃)𝑊)𝑀 ↔ ∀𝑦 ∈ 𝐵 ∀𝑔 ∈ ((𝐹‘𝑦)𝐽𝑊)∃!𝑘 ∈ (𝑦𝐻𝑋)𝑔 = (𝑀(⟨(𝐹‘𝑦), (𝐹‘𝑋)⟩ ∙ 𝑊)((𝑦𝐺𝑋)‘𝑘)))) | ||
| Theorem | isnatd 48886* | Property of being a natural transformation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ · = (comp‘𝐷) & ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) & ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) & ⊢ (𝜑 → 𝐴 Fn 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐴‘𝑥) ∈ ((𝐹‘𝑥)𝐽(𝐾‘𝑥))) & ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ℎ ∈ (𝑥𝐻𝑦)) → ((𝐴‘𝑦)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ · (𝐾‘𝑦))((𝑥𝐺𝑦)‘ℎ)) = (((𝑥𝐿𝑦)‘ℎ)(⟨(𝐹‘𝑥), (𝐾‘𝑥)⟩ · (𝐾‘𝑦))(𝐴‘𝑥))) ⇒ ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) | ||
| Theorem | natrcl2 48887 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | ||
| Theorem | natrcl3 48888 | Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑁 = (𝐶 Nat 𝐷) & ⊢ (𝜑 → 𝐴 ∈ (⟨𝐹, 𝐺⟩𝑁⟨𝐾, 𝐿⟩)) ⇒ ⊢ (𝜑 → 𝐾(𝐶 Func 𝐷)𝐿) | ||
| Theorem | xpcfucbas 48889 | The base set of the product of two categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) ⇒ ⊢ ((𝐵 Func 𝐶) × (𝐷 Func 𝐸)) = (Base‘𝑇) | ||
| Theorem | xpcfuchomfval 48890* | Set of morphisms of the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝐴 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ 𝐾 = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐴 ↦ (((1st ‘𝑢)(𝐵 Nat 𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(𝐷 Nat 𝐸)(2nd ‘𝑣)))) | ||
| Theorem | xpcfuchom 48891 | Set of morphisms of the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝐴 = (Base‘𝑇) & ⊢ 𝐾 = (Hom ‘𝑇) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = (((1st ‘𝑋)(𝐵 Nat 𝐶)(1st ‘𝑌)) × ((2nd ‘𝑋)(𝐷 Nat 𝐸)(2nd ‘𝑌)))) | ||
| Theorem | xpcfuchom2 48892 | Value of the set of morphisms in the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ (𝜑 → 𝑀 ∈ (𝐵 Func 𝐶)) & ⊢ (𝜑 → 𝑁 ∈ (𝐷 Func 𝐸)) & ⊢ (𝜑 → 𝑃 ∈ (𝐵 Func 𝐶)) & ⊢ (𝜑 → 𝑄 ∈ (𝐷 Func 𝐸)) & ⊢ 𝐾 = (Hom ‘𝑇) ⇒ ⊢ (𝜑 → (⟨𝑀, 𝑁⟩𝐾⟨𝑃, 𝑄⟩) = ((𝑀(𝐵 Nat 𝐶)𝑃) × (𝑁(𝐷 Nat 𝐸)𝑄))) | ||
| Theorem | xpcfucco2 48893 | Value of composition in the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃)) & ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅)) & ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆)) ⇒ ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) = ⟨(𝐾(⟨𝑀, 𝑃⟩(comp‘(𝐵 FuncCat 𝐶))𝑅)𝐹), (𝐿(⟨𝑁, 𝑄⟩(comp‘(𝐷 FuncCat 𝐸))𝑆)𝐺)⟩) | ||
| Theorem | xpcfuccocl 48894 | The composition of two natural transformations is a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃)) & ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅)) & ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆)) ⇒ ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) ∈ ((𝑀(𝐵 Nat 𝐶)𝑅) × (𝑁(𝐷 Nat 𝐸)𝑆))) | ||
| Theorem | xpcfucco3 48895* | Value of composition in the binary product of categories of functors; expressed explicitly. (Contributed by Zhi Wang, 1-Oct-2025.) |
| ⊢ 𝑇 = ((𝐵 FuncCat 𝐶) ×c (𝐷 FuncCat 𝐸)) & ⊢ 𝑂 = (comp‘𝑇) & ⊢ (𝜑 → 𝐹 ∈ (𝑀(𝐵 Nat 𝐶)𝑃)) & ⊢ (𝜑 → 𝐺 ∈ (𝑁(𝐷 Nat 𝐸)𝑄)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃(𝐵 Nat 𝐶)𝑅)) & ⊢ (𝜑 → 𝐿 ∈ (𝑄(𝐷 Nat 𝐸)𝑆)) & ⊢ 𝑋 = (Base‘𝐵) & ⊢ 𝑌 = (Base‘𝐷) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐸) ⇒ ⊢ (𝜑 → (⟨𝐾, 𝐿⟩(⟨⟨𝑀, 𝑁⟩, ⟨𝑃, 𝑄⟩⟩𝑂⟨𝑅, 𝑆⟩)⟨𝐹, 𝐺⟩) = ⟨(𝑥 ∈ 𝑋 ↦ ((𝐾‘𝑥)(⟨((1st ‘𝑀)‘𝑥), ((1st ‘𝑃)‘𝑥)⟩ · ((1st ‘𝑅)‘𝑥))(𝐹‘𝑥))), (𝑦 ∈ 𝑌 ↦ ((𝐿‘𝑦)(⟨((1st ‘𝑁)‘𝑦), ((1st ‘𝑄)‘𝑦)⟩ ∙ ((1st ‘𝑆)‘𝑦))(𝐺‘𝑦)))⟩) | ||
| Theorem | fucofulem1 48896 | Lemma for proving functor theorems. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) & ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜏)) → 𝜂) & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜂) → 𝜃) & ⊢ ((𝜑 ∧ 𝜂) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜂)) | ||
| Theorem | fucofulem2 48897* | Lemma for proving functor theorems. Maybe consider eufnfv 7256 to prove the uniqueness of a functor. (Contributed by Zhi Wang, 25-Sep-2025.) |
| ⊢ 𝐵 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) & ⊢ 𝐻 = (Hom ‘((𝐷 FuncCat 𝐸) ×c (𝐶 FuncCat 𝐷))) ⇒ ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(𝐶 Nat 𝐸)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (𝑢𝐺𝑣)) ∧ ∀𝑚 ∈ 𝐵 ∀𝑛 ∈ 𝐵 ((𝑚𝐺𝑛) = (𝑏 ∈ ((1st ‘𝑚)(𝐷 Nat 𝐸)(1st ‘𝑛)), 𝑎 ∈ ((2nd ‘𝑚)(𝐶 Nat 𝐷)(2nd ‘𝑛)) ↦ (𝑏(𝑚𝐺𝑛)𝑎)) ∧ ∀𝑝 ∈ ((1st ‘𝑚)(𝐷 Nat 𝐸)(1st ‘𝑛))∀𝑞 ∈ ((2nd ‘𝑚)(𝐶 Nat 𝐷)(2nd ‘𝑛))(𝑝(𝑚𝐺𝑛)𝑞) ∈ ((𝐹‘𝑚)(𝐶 Nat 𝐸)(𝐹‘𝑛))))) | ||
| Theorem | fuco2el 48898 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩ ∈ (𝑆 × 𝑅) ↔ (𝐾𝑆𝐿 ∧ 𝐹𝑅𝐺)) | ||
| Theorem | fuco2eld 48899 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅)) & ⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩) & ⊢ (𝜑 → 𝐾𝑆𝐿) & ⊢ (𝜑 → 𝐹𝑅𝐺) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑊) | ||
| Theorem | fuco2eld2 48900 | Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025.) |
| ⊢ (𝜑 → 𝑊 = (𝑆 × 𝑅)) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ Rel 𝑆 & ⊢ Rel 𝑅 ⇒ ⊢ (𝜑 → 𝑈 = ⟨⟨(1st ‘(1st ‘𝑈)), (2nd ‘(1st ‘𝑈))⟩, ⟨(1st ‘(2nd ‘𝑈)), (2nd ‘(2nd ‘𝑈))⟩⟩) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |