HomeTheorem List (p. 499 of 508)
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. 499 of 508) | < 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-31341) |
Hilbert Space Explorer
(31342-32864) |
Users' Mathboxes
(32865-50710) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | glbprdm 49801 | 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 49802 | 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 49803* | 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 49804* | 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 49805* | 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 49806* | 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 49807 | Poset join is idempotent. latjidm 18540 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋) | ||
| Theorem | posmidm 49808 | Poset meet is idempotent. latmidm 18552 could be shortened by this. (Contributed by Zhi Wang, 27-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋) | ||
| Theorem | resiposbas 49809 | Construct a poset (resipos 49810) for any base set. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ( I ↾ 𝐵)⟩} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐾)) | ||
| Theorem | resipos 49810 | 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 49811* | There exists a poset for any base set. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Poset 𝐵 = (Base‘𝑘)) | ||
| Theorem | exbasprs 49812* | There exists a preordered set for any base set. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ (𝐵 ∈ 𝑉 → ∃𝑘 ∈ Proset 𝐵 = (Base‘𝑘)) | ||
| Theorem | basresposfo 49813 | 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 49814 | 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 49815 | The class of posets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ Poset ∉ V | ||
| Theorem | prsnex 49816 | The class of preordered sets is a proper class. (Contributed by Zhi Wang, 20-Oct-2025.) |
| ⊢ Proset ∉ V | ||
| Theorem | toslat 49817 | A toset is a lattice. (Contributed by Zhi Wang, 26-Sep-2024.) |
| ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Lat) | ||
| Theorem | isclatd 49818* | The predicate "is a complete lattice" (deduction form). (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝑈 = (lub‘𝐾)) & ⊢ (𝜑 → 𝐺 = (glb‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝑈) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝐺) ⇒ ⊢ (𝜑 → 𝐾 ∈ CLat) | ||
| Theorem | intubeu 49819* | Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ (𝐶 ∈ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ ∀𝑦 ∈ 𝐵 (𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦)) ↔ 𝐶 = ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥})) | ||
| Theorem | unilbeu 49820* | Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴})) | ||
| Theorem | ipolublem 49821* | Lemma for ipolubdm 49822 and ipolub 49823. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((∪ 𝑆 ⊆ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∪ 𝑆 ⊆ 𝑧 → 𝑋 ⊆ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑋 ≤ 𝑧)))) | ||
| Theorem | ipolubdm 49822* | The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹)) | ||
| Theorem | ipolub 49823* | The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with 𝑆 ∈ dom 𝑈.) Could be significantly shortened if poslubdg 18490 is in quantified form. mrelatlub 18640 could potentially be shortened using this. See mrelatlubALT 49830. (Contributed by Zhi Wang, 28-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∩ {𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
| Theorem | ipoglblem 49824* | Lemma for ipoglbdm 49825 and ipoglb 49826. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐹) → ((𝑋 ⊆ ∩ 𝑆 ∧ ∀𝑧 ∈ 𝐹 (𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋)) ↔ (∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐹 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋)))) | ||
| Theorem | ipoglbdm 49825* | The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) ⇒ ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹)) | ||
| Theorem | ipoglb 49826* | The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with 𝑆 ∈ dom 𝐺.) Could be significantly shortened if posglbdg 18491 is in quantified form. mrelatglb 18638 could potentially be shortened using this. See mrelatglbALT 49831. (Contributed by Zhi Wang, 29-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → 𝑇 = ∪ {𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆}) & ⊢ (𝜑 → 𝑇 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇) | ||
| Theorem | ipolub0 49827 | The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝑈 = (lub‘𝐼)) & ⊢ (𝜑 → ∩ 𝐹 ∈ 𝐹) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑈‘∅) = ∩ 𝐹) | ||
| Theorem | ipolub00 49828 | 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 49829 | The GLB of the empty set is the union of the base. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐹) & ⊢ (𝜑 → 𝐺 = (glb‘𝐼)) & ⊢ (𝜑 → ∪ 𝐹 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐹) | ||
| Theorem | mrelatlubALT 49830 | 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 49831 | 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 49832 | A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
| Theorem | topclat 49833 | A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ CLat) | ||
| Theorem | toplatglb0 49834 | The empty intersection in a topology is realized by the base set. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ (𝜑 → (𝐺‘∅) = ∪ 𝐽) | ||
| Theorem | toplatlub 49835 | Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑆 ⊆ 𝐽) & ⊢ 𝑈 = (lub‘𝐼) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = ∪ 𝑆) | ||
| Theorem | toplatglb 49836 | 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 49837 | Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∨ = (join‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∨ 𝐵) = (𝐴 ∪ 𝐵)) | ||
| Theorem | toplatmeet 49838 | Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ ∧ = (meet‘𝐼) ⇒ ⊢ (𝜑 → (𝐴 ∧ 𝐵) = (𝐴 ∩ 𝐵)) | ||
| Theorem | topdlat 49839 | A topology is a distributive lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024.) |
| ⊢ 𝐼 = (toInc‘𝐽) ⇒ ⊢ (𝐽 ∈ Top → 𝐼 ∈ DLat) | ||
| Theorem | elmgpcntrd 49840* | The center of a ring. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑍 = (Cntr‘𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑋)) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑍) | ||
| Theorem | asclelbasALT 49841 | Alternate proof of asclelbas 22083. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘𝐶) ∈ (Base‘𝑊)) | ||
| Theorem | asclcntr 49842 | 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 49843 |
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 22063, assa2ass2 22064, and asclval 22079, by setting 𝑋 and 𝑌 the multiplicative identity of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ∗ = (.r‘𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴‘(𝐶 ∗ 𝐷)) = (𝐴‘(𝐷 ∗ 𝐶))) | ||
| Theorem | homf0 49844 | The base is empty iff the functionalized Hom-set operation is empty. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ ((Base‘𝐶) = ∅ ↔ (Homf ‘𝐶) = ∅) | ||
| Theorem | catprslem 49845* | Lemma for catprs 49846. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ≤ 𝑌 ↔ (𝑋𝐻𝑌) ≠ ∅)) | ||
| Theorem | catprs 49846* | A preorder can be extracted from a category. See catprs2 49847 for more details. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
| Theorem | catprs2 49847* | 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 49848 and catprsc2 49849 for constructions satisfying the hypothesis "catprs.1". See catprs 49846 for a more primitive version. See prsthinc 50299 for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑥𝐻𝑦) ≠ ∅)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → ≤ = (le‘𝐶)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Proset ) | ||
| Theorem | catprsc 49848* | A construction of the preorder induced by a category. See catprs2 49847 for details. See also catprsc2 49849 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ (𝑥𝐻𝑦) ≠ ∅)}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | catprsc2 49849* | An alternate construction of the preorder induced by a category. See catprs2 49847 for details. See also catprsc 49848 for a different construction. The two constructions are different because df-cat 17746 does not require the domain of 𝐻 to be 𝐵 × 𝐵. (Contributed by Zhi Wang, 23-Sep-2024.) |
| ⊢ (𝜑 → ≤ = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐻𝑦) ≠ ∅}) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧 ≤ 𝑤 ↔ (𝑧𝐻𝑤) ≠ ∅)) | ||
| Theorem | endmndlem 49850 | A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc 50413 for converting a monoid to a category. Lemma for bj-endmnd 38019. (Contributed by Zhi Wang, 25-Sep-2024.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑋𝐻𝑋) = (Base‘𝑀)) & ⊢ (𝜑 → (⟨𝑋, 𝑋⟩ · 𝑋) = (+g‘𝑀)) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mnd) | ||
| Theorem | oppccatb 49851 | An opposite category is a category. (Contributed by Zhi Wang, 23-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝑂 ∈ Cat)) | ||
| Theorem | oppcmndclem 49852 | Lemma for oppcmndc 49854. Everything is true for two distinct elements in a singleton or an empty set (since it is impossible). Note that if this theorem and oppcendc 49853 are in ¬ 𝑥 = 𝑦 form, then both proofs should be one step shorter. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ (𝜑 → 𝐵 = {𝐴}) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≠ 𝑌 → 𝜓)) | ||
| Theorem | oppcendc 49853* | The opposite category of a category whose morphisms are all endomorphisms has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 ≠ 𝑦 → (𝑥𝐻𝑦) = ∅)) ⇒ ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂)) | ||
| Theorem | oppcmndc 49854 | The opposite category of a category whose base set is a singleton or an empty set has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ (𝜑 → 𝐵 = {𝑋}) ⇒ ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝑂)) | ||
| Theorem | idmon 49855 | 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 49856 | 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 | sectrcl 49857 | Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | sectrcl2 49858 | Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑆 = (Sect‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑆𝑌)𝐺) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | invrcl 49859 | Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | invrcl2 49860 | Reverse closure for inverse relations. (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐹(𝑋𝑁𝑌)𝐺) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | isinv2 49861 | The property "𝐹 is an inverse of 𝐺". (Contributed by Zhi Wang, 14-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝑆 = (Sect‘𝐶) ⇒ ⊢ (𝐹(𝑋𝑁𝑌)𝐺 ↔ (𝐹(𝑋𝑆𝑌)𝐺 ∧ 𝐺(𝑌𝑆𝑋)𝐹)) | ||
| Theorem | isisod 49862 | 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 49863* | Lemma for upeu2 50007. 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 | sectfn 49864 | The function value of the function returning the sections of a category is a function over the Cartesian square of the base set of the category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → (Sect‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | invfn 49865 | The function value of the function returning the inverses of a category is a function over the Cartesian square of the base set of the category. Simplifies isofn 17854 (see isofnALT 49866). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → (Inv‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | isofnALT 49866 | The function value of the function returning the isomorphisms of a category is a function over the Cartesian square of the base set of the category. (Contributed by AV, 5-Apr-2020.) (Proof shortened by Zhi Wang, 3-Nov-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐶 ∈ Cat → (Iso‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))) | ||
| Theorem | isofval2 49867* | Function value of the function returning the isomorphisms of a category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝑁 = (Inv‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝜑 → 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ dom (𝑥𝑁𝑦))) | ||
| Theorem | isorcl 49868 | Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
| Theorem | isorcl2 49869 | Reverse closure for isomorphism relations. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝐼 = (Iso‘𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌)) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | isoval2 49870 | The isomorphisms are the domain of the inverse relation. (Contributed by Zhi Wang, 17-Nov-2025.) |
| ⊢ 𝑁 = (Inv‘𝐶) & ⊢ 𝐼 = (Iso‘𝐶) ⇒ ⊢ (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌) | ||
| Theorem | sectpropdlem 49871 | Lemma for sectpropd 49872. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷)) | ||
| Theorem | sectpropd 49872 | Two structures with the same base, hom-sets and composition operation have the same sections. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (Sect‘𝐶) = (Sect‘𝐷)) | ||
| Theorem | invpropdlem 49873 | Lemma for invpropd 49874. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Inv‘𝐶)) → 𝑃 ∈ (Inv‘𝐷)) | ||
| Theorem | invpropd 49874 | Two structures with the same base, hom-sets and composition operation have the same inverses. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (Inv‘𝐶) = (Inv‘𝐷)) | ||
| Theorem | isopropdlem 49875 | Lemma for isopropd 49876. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ (Iso‘𝐶)) → 𝑃 ∈ (Iso‘𝐷)) | ||
| Theorem | isopropd 49876 | Two structures with the same base, hom-sets and composition operation have the same isomorphisms. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → (Iso‘𝐶) = (Iso‘𝐷)) | ||
| Theorem | cicfn 49877 | ≃𝑐 is a function on Cat. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ ≃𝑐 Fn Cat | ||
| Theorem | cicrcl2 49878 | Isomorphism implies the structure being a category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 → 𝐶 ∈ Cat) | ||
| Theorem | oppccic 49879 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 26-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝐶)𝑆) ⇒ ⊢ (𝜑 → 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | relcic 49880 | The set of isomorphic objects is a relation. Simplifies cicer 17885 (see cicerALT 49881). (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝐶 ∈ Cat → Rel ( ≃𝑐 ‘𝐶)) | ||
| Theorem | cicerALT 49881 | Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in [Adamek] p. 29. (Contributed by AV, 5-Apr-2020.) (Proof shortened by Zhi Wang, 3-Nov-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐶 ∈ Cat → ( ≃𝑐 ‘𝐶) Er (Base‘𝐶)) | ||
| Theorem | cic1st2nd 49882 | Reconstruction of a pair of isomorphic objects in terms of its ordered pair components. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝑃 ∈ ( ≃𝑐 ‘𝐶) → 𝑃 = ⟨(1st ‘𝑃), (2nd ‘𝑃)⟩) | ||
| Theorem | cic1st2ndbr 49883 | Rewrite the predicate of isomorphic objects with separated parts. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝑃 ∈ ( ≃𝑐 ‘𝐶) → (1st ‘𝑃)( ≃𝑐 ‘𝐶)(2nd ‘𝑃)) | ||
| Theorem | cicpropdlem 49884 | Lemma for cicpropd 49885. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ ( ≃𝑐 ‘𝐶)) → 𝑃 ∈ ( ≃𝑐 ‘𝐷)) | ||
| Theorem | cicpropd 49885 | Two structures with the same base, hom-sets and composition operation have the same isomorphic objects. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) ⇒ ⊢ (𝜑 → ( ≃𝑐 ‘𝐶) = ( ≃𝑐 ‘𝐷)) | ||
| Theorem | oppccicb 49886 | Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝑅( ≃𝑐 ‘𝐶)𝑆 ↔ 𝑅( ≃𝑐 ‘𝑂)𝑆) | ||
| Theorem | oppcciceq 49887 | The opposite category has the same isomorphic objects as the original category. (Contributed by Zhi Wang, 27-Oct-2025.) |
| ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ ( ≃𝑐 ‘𝐶) = ( ≃𝑐 ‘𝑂) | ||
| Theorem | dmdm 49888 | The double domain of a function on a Cartesian square. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ (𝐴 Fn (𝐵 × 𝐵) → 𝐵 = dom dom 𝐴) | ||
| Theorem | iinfssclem1 49889* | Lemma for iinfssc 49892. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 = (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝑆, 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 𝑆 ↦ ∩ 𝑥 ∈ 𝐴 (𝑧𝐻𝑤))) | ||
| Theorem | iinfssclem2 49890* | Lemma for iinfssc 49892. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → 𝐾 Fn (∩ 𝑥 ∈ 𝐴 𝑆 × ∩ 𝑥 ∈ 𝐴 𝑆)) | ||
| Theorem | iinfssclem3 49891* | Lemma for iinfssc 49892. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 = dom dom 𝐻) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑋 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) & ⊢ (𝜑 → 𝑌 ∈ ∩ 𝑥 ∈ 𝐴 𝑆) ⇒ ⊢ (𝜑 → (𝑋𝐾𝑌) = ∩ 𝑥 ∈ 𝐴 (𝑋𝐻𝑌)) | ||
| Theorem | iinfssc 49892* | Indexed intersection of subcategories is a subcategory (the category-agnostic version). (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ⊆cat 𝐽) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ⊆cat 𝐽) | ||
| Theorem | iinfsubc 49893* | Indexed intersection of subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐾 = (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 (𝐻‘𝑦))) ⇒ ⊢ (𝜑 → 𝐾 ∈ (Subcat‘𝐶)) | ||
| Theorem | iinfprg 49894* | Indexed intersection of functions with an unordered pair index. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) = (𝑥 ∈ ∩ 𝑦 ∈ {𝐴, 𝐵}dom 𝑦 ↦ ∩ 𝑦 ∈ {𝐴, 𝐵} (𝑦‘𝑥))) | ||
| Theorem | infsubc 49895* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ (Subcat‘𝐶) ∧ 𝐵 ∈ (Subcat‘𝐶)) → (𝑥 ∈ (dom 𝐴 ∩ dom 𝐵) ↦ ((𝐴‘𝑥) ∩ (𝐵‘𝑥))) ∈ (Subcat‘𝐶)) | ||
| Theorem | infsubc2 49896* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ ((𝐴 ∈ (Subcat‘𝐶) ∧ 𝐵 ∈ (Subcat‘𝐶)) → (𝑥 ∈ (dom dom 𝐴 ∩ dom dom 𝐵), 𝑦 ∈ (dom dom 𝐴 ∩ dom dom 𝐵) ↦ ((𝑥𝐴𝑦) ∩ (𝑥𝐵𝑦))) ∈ (Subcat‘𝐶)) | ||
| Theorem | infsubc2d 49897* | The intersection of two subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025.) |
| ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) & ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) & ⊢ (𝜑 → 𝐻 ∈ (Subcat‘𝐶)) & ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝑆 ∩ 𝑇), 𝑦 ∈ (𝑆 ∩ 𝑇) ↦ ((𝑥𝐻𝑦) ∩ (𝑥𝐽𝑦))) ∈ (Subcat‘𝐶)) | ||
| Theorem | discsubclem 49898* | Lemma for discsubc 49899. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) ⇒ ⊢ 𝐽 Fn (𝑆 × 𝑆) | ||
| Theorem | discsubc 49899* | A discrete category, whose only morphisms are the identity morphisms, is a subcategory. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Cat) ⇒ ⊢ (𝜑 → 𝐽 ∈ (Subcat‘𝐶)) | ||
| Theorem | iinfconstbaslem 49900* | Lemma for iinfconstbas 49901. (Contributed by Zhi Wang, 1-Nov-2025.) |
| ⊢ 𝐽 = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝑦, {(𝐼‘𝑥)}, ∅)) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐼 = (Id‘𝐶) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝐴 = ((Subcat‘𝐶) ∩ {𝑗 ∣ 𝑗 Fn (𝑆 × 𝑆)})) ⇒ ⊢ (𝜑 → 𝐽 ∈ 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |