Home | Metamath
Proof Explorer Theorem List (p. 162 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mrcidb2 16101 | A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) ⊆ 𝑈)) | ||
Theorem | mrcidm 16102 | The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘(𝐹‘𝑈)) = (𝐹‘𝑈)) | ||
Theorem | mrcsscl 16103 | The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶) → (𝐹‘𝑈) ⊆ 𝑉) | ||
Theorem | mrcuni 16104 | Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) = (𝐹‘∪ (𝐹 “ 𝑈))) | ||
Theorem | mrcun 16105 | Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘(𝑈 ∪ 𝑉)) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉)))) | ||
Theorem | mrcssvd 16106 | The Moore closure of a set is a subset of the base. Deduction form of mrcssv 16097. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) ⇒ ⊢ (𝜑 → (𝑁‘𝐵) ⊆ 𝑋) | ||
Theorem | mrcssd 16107 | Moore closure preserves subset ordering. Deduction form of mrcss 16099. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑉) & ⊢ (𝜑 → 𝑉 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘𝑈) ⊆ (𝑁‘𝑉)) | ||
Theorem | mrcssidd 16108 | A set is contained in its Moore closure. Deduction form of mrcssid 16100. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑋) ⇒ ⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈)) | ||
Theorem | mrcidmd 16109 | Moore closure is idempotent. Deduction form of mrcidm 16102. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈)) | ||
Theorem | mressmrcd 16110 | In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) | ||
Theorem | submrc 16111 | In a closure system which is cut off above some level, closures below that level act as normal. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) & ⊢ 𝐺 = (mrCls‘(𝐶 ∩ 𝒫 𝐷)) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐷 ∈ 𝐶 ∧ 𝑈 ⊆ 𝐷) → (𝐺‘𝑈) = (𝐹‘𝑈)) | ||
Theorem | mrieqvlemd 16112 | In a Moore system, if 𝑌 is a member of 𝑆, (𝑆 ∖ {𝑌}) and 𝑆 have the same closure if and only if 𝑌 is in the closure of (𝑆 ∖ {𝑌}). Used in the proof of mrieqvd 16121 and mrieqv2d 16122. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})) ↔ (𝑁‘(𝑆 ∖ {𝑌})) = (𝑁‘𝑆))) | ||
Theorem | mrisval 16113* | Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) | ||
Theorem | ismri 16114* | Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ (𝐴 ∈ (Moore‘𝑋) → (𝑆 ∈ 𝐼 ↔ (𝑆 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))) | ||
Theorem | ismri2 16115* | Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) | ||
Theorem | ismri2d 16116* | Criterion for a subset of the base set in a Moore system to be independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) | ||
Theorem | ismri2dd 16117* | Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐼) | ||
Theorem | mriss 16118 | An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐼) → 𝑆 ⊆ 𝑋) | ||
Theorem | mrissd 16119 | An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝑋) | ||
Theorem | ismri2dad 16120 | Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌}))) | ||
Theorem | mrieqvd 16121* | In a Moore system, a set is independent if and only if, for all elements of the set, the closure of the set with the element removed is unequal to the closure of the original set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆))) | ||
Theorem | mrieqv2d 16122* | In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)))) | ||
Theorem | mrissmrcd 16123 | In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd 16110, and so are equal by mrieqv2d 16122.) (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑆 = 𝑇) | ||
Theorem | mrissmrid 16124 | In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → 𝑇 ∈ 𝐼) | ||
Theorem | mreexd 16125* | In a Moore system, the closure operator is said to have the exchange property if, for all elements 𝑦 and 𝑧 of the base set and subsets 𝑆 of the base set such that 𝑧 is in the closure of (𝑆 ∪ {𝑦}) but not in the closure of 𝑆, 𝑦 is in the closure of (𝑆 ∪ {𝑧}) (Definition 3.1.9 in [FaureFrolicher] p. 57 to 58.) This theorem allows us to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌}))) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆)) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))) | ||
Theorem | mreexmrid 16126* | In a Moore system whose closure operator has the exchange property, if a set is independent and an element is not in its closure, then adding the element to the set gives another independent set. Lemma 4.1.5 in [FaureFrolicher] p. 84. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘𝑆)) ⇒ ⊢ (𝜑 → (𝑆 ∪ {𝑌}) ∈ 𝐼) | ||
Theorem | mreexexlemd 16127* | This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 16131. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → (𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾)) & ⊢ (𝜑 → ∀𝑡∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼))) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)) | ||
Theorem | mreexexlem2d 16128* | Used in mreexexlem4d 16130 to prove the induction step in mreexexd 16131. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐹) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ 𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)) | ||
Theorem | mreexexlem3d 16129* | Base case of the induction in mreexexd 16131. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → (𝐹 = ∅ ∨ 𝐺 = ∅)) ⇒ ⊢ (𝜑 → ∃𝑖 ∈ 𝒫 𝐺(𝐹 ≈ 𝑖 ∧ (𝑖 ∪ 𝐻) ∈ 𝐼)) | ||
Theorem | mreexexlem4d 16130* | Induction step of the induction in mreexexd 16131. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → 𝐿 ∈ ω) & ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐿 ∨ 𝑔 ≈ 𝐿) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼))) & ⊢ (𝜑 → (𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿)) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)) | ||
Theorem | mreexexd 16131* | Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if 𝐹 and 𝐺 are disjoint from 𝐻, (𝐹 ∪ 𝐻) is independent, 𝐹 is contained in the closure of (𝐺 ∪ 𝐻), and either 𝐹 or 𝐺 is finite, then there is a subset 𝑞 of 𝐺 equinumerous to 𝐹 such that (𝑞 ∪ 𝐻) is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either (𝐴 ∖ 𝐵) or (𝐵 ∖ 𝐴) is finite. The theorem is proven by induction using mreexexlem3d 16129 for the base case and mreexexlem4d 16130 for the induction step. (Contributed by David Moews, 1-May-2017.) Removed dependencies on ax-rep 4699 and ax-ac2 9168. (Revised by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin)) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼)) | ||
Theorem | mreexexdOLD 16132* | Obsolete proof of mreexexd 16131 as of 2-Jun-2021. Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if 𝐹 and 𝐺 are disjoint from 𝐻, (𝐹 ∪ 𝐻) is independent, 𝐹 is contained in the closure of (𝐺 ∪ 𝐻), and either 𝐹 or 𝐺 is finite, then there is a subset 𝑞 of 𝐺 equinumerous to 𝐹 such that (𝑞 ∪ 𝐻) is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either (𝐴 ∖ 𝐵) or (𝐵 ∖ 𝐴) is finite. The theorem is proven by induction using mreexexlem3d 16129 for the base case and mreexexlem4d 16130 for the induction step. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin)) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼)) | ||
Theorem | mreexdomd 16133* | In a Moore system whose closure operator has the exchange property, if 𝑆 is independent and contained in the closure of 𝑇, and either 𝑆 or 𝑇 is finite, then 𝑇 dominates 𝑆. This is an immediate consequence of mreexexd 16131. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑋) & ⊢ (𝜑 → (𝑆 ∈ Fin ∨ 𝑇 ∈ Fin)) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑆 ≼ 𝑇) | ||
Theorem | mreexfidimd 16134* | In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd 16133 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝐼) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
Theorem | isacs 16135* | A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | ||
Theorem | acsmre 16136 | Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) | ||
Theorem | isacs2 16137* | In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑠))) | ||
Theorem | acsfiel 16138* | A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) → (𝑆 ∈ 𝐶 ↔ (𝑆 ⊆ 𝑋 ∧ ∀𝑦 ∈ (𝒫 𝑆 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑆))) | ||
Theorem | acsfiel2 16139* | A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑆 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑆)) | ||
Theorem | acsmred 16140 | An algebraic closure system is also a Moore system. Deduction form of acsmre 16136. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) | ||
Theorem | isacs1i 16141* | A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (ACS‘𝑋)) | ||
Theorem | mreacs 16142 | Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)) | ||
Theorem | acsfn 16143* | Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) ∧ (𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎)} ∈ (ACS‘𝑋)) | ||
Theorem | acsfn0 16144* | Algebraicity of a point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ 𝐾 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | acsfn1 16145* | Algebraicity of a one-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | acsfn1c 16146* | Algebraicity of a one-argument closure condition with additional constant. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Theorem | acsfn2 16147* | Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋)) | ||
Syntax | ccat 16148 | Extend class notation with the class of categories. |
class Cat | ||
Syntax | ccid 16149 | Extend class notation with the identity arrow of a category. |
class Id | ||
Syntax | chomf 16150 | Extend class notation to include functionalized Hom-set extractor. |
class Homf | ||
Syntax | ccomf 16151 | Extend class notation to include functionalized composition operation. |
class compf | ||
Definition | df-cat 16152* | A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated with those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. Definition in [Lang] p. 53. In contrast to definition 3.1 of [Adamek] p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" ((Base‘𝑐)), the morphisms "hom" ((Hom ‘𝑐)) and the composition law "o" ((comp‘𝑐)). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in [Adamek] p. 21 and df-cid 16153. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.) |
⊢ Cat = {𝑐 ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))))} | ||
Definition | df-cid 16153* | Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)))) | ||
Definition | df-homf 16154* | Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦))) | ||
Definition | df-comf 16155* | Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)))) | ||
Theorem | iscat 16156* | The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))))) | ||
Theorem | iscatd 16157* | Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ⇒ ⊢ (𝜑 → 𝐶 ∈ Cat) | ||
Theorem | catidex 16158* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓)) | ||
Theorem | catideu 16159* | Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃!𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓)) | ||
Theorem | cidfval 16160* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝜑 → 1 = (𝑥 ∈ 𝐵 ↦ (℩𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓)))) | ||
Theorem | cidval 16161* | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) = (℩𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(〈𝑦, 𝑋〉 · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(〈𝑋, 𝑋〉 · 𝑦)𝑔) = 𝑓))) | ||
Theorem | cidffn 16162 | The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ Id Fn Cat | ||
Theorem | cidfn 16163 | The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 1 = (Id‘𝐶) ⇒ ⊢ (𝐶 ∈ Cat → 1 Fn 𝐵) | ||
Theorem | catidd 16164* | Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(〈𝑥, 𝑥〉 · 𝑦) 1 ) = 𝑓) ⇒ ⊢ (𝜑 → (Id‘𝐶) = (𝑥 ∈ 𝐵 ↦ 1 )) | ||
Theorem | iscatd2 16165* | Version of iscatd 16157 with a uniform assumption list, for increased proof sharing capabilities. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) & ⊢ (𝜑 → · = (comp‘𝐶)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦)) & ⊢ ((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) & ⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) & ⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) & ⊢ ((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) | ||
Theorem | catidcl 16166 | Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋𝐻𝑋)) | ||
Theorem | catlid 16167 | Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (( 1 ‘𝑌)(〈𝑋, 𝑌〉 · 𝑌)𝐹) = 𝐹) | ||
Theorem | catrid 16168 | Right identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 1 = (Id‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) ⇒ ⊢ (𝜑 → (𝐹(〈𝑋, 𝑋〉 · 𝑌)( 1 ‘𝑋)) = 𝐹) | ||
Theorem | catcocl 16169 | Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) ∈ (𝑋𝐻𝑍)) | ||
Theorem | catass 16170 | Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊)) ⇒ ⊢ (𝜑 → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹))) | ||
Theorem | 0catg 16171 | Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ Cat) | ||
Theorem | 0cat 16172 | The empty set is a category, the empty category, see example 3.3(4.c) in [Adamek] p. 24. (Contributed by Mario Carneiro, 3-Jan-2017.) |
⊢ ∅ ∈ Cat | ||
Theorem | homffval 16173* | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐹 = (Homf ‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥𝐻𝑦)) | ||
Theorem | fnhomeqhomf 16174 | If the Hom-set operation is a function it is equal to the corresponding functionalized Hom-set operation. (Contributed by AV, 1-Mar-2020.) |
⊢ 𝐹 = (Homf ‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐻 Fn (𝐵 × 𝐵) → 𝐹 = 𝐻) | ||
Theorem | homfval 16175 | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐹 = (Homf ‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑋𝐻𝑌)) | ||
Theorem | homffn 16176 | The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐹 = (Homf ‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ 𝐹 Fn (𝐵 × 𝐵) | ||
Theorem | homfeq 16177* | Condition for two categories with the same base to have the same hom-sets. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐷)) ⇒ ⊢ (𝜑 → ((Homf ‘𝐶) = (Homf ‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) = (𝑥𝐽𝑦))) | ||
Theorem | homfeqd 16178 | If two structures have the same Hom slot, they have the same Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) & ⊢ (𝜑 → (Hom ‘𝐶) = (Hom ‘𝐷)) ⇒ ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) | ||
Theorem | homfeqbas 16179 | Deduce equality of base sets from equality of Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) ⇒ ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) | ||
Theorem | homfeqval 16180 | Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝐽 = (Hom ‘𝐷) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋𝐽𝑌)) | ||
Theorem | comfffval 16181* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) | ||
Theorem | comffval 16182* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑍)𝑓))) | ||
Theorem | comfval 16183 | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉𝑂𝑍)𝐹) = (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)) | ||
Theorem | comfffval2 16184* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ · = (comp‘𝐶) ⇒ ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓))) | ||
Theorem | comffval2 16185* | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(〈𝑋, 𝑌〉 · 𝑍)𝑓))) | ||
Theorem | comfval2 16186 | Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Homf ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉𝑂𝑍)𝐹) = (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)) | ||
Theorem | comfffn 16187 | The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ 𝑂 Fn ((𝐵 × 𝐵) × 𝐵) | ||
Theorem | comffn 16188 | The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝑂 = (compf‘𝐶) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉𝑂𝑍) Fn ((𝑌𝐻𝑍) × (𝑋𝐻𝑌))) | ||
Theorem | comfeq 16189* | Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ (𝜑 → 𝐵 = (Base‘𝐶)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐷)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) ⇒ ⊢ (𝜑 → ((compf‘𝐶) = (compf‘𝐷) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉 ∙ 𝑧)𝑓))) | ||
Theorem | comfeqd 16190 | Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (𝜑 → (comp‘𝐶) = (comp‘𝐷)) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) ⇒ ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) | ||
Theorem | comfeqval 16191 | Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ ∙ = (comp‘𝐷) & ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) & ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹) = (𝐺(〈𝑋, 𝑌〉 ∙ 𝑍)𝐹)) | ||
Theorem | catpropd 16192 | Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat)) | ||
Theorem | cidpropd 16193 | Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017.) |
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷)) & ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷)) | ||
Syntax | coppc 16194 | The opposite category operation. |
class oppCat | ||
Definition | df-oppc 16195* | Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. Definition 3.5 of [Adamek] p. 25. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ oppCat = (𝑓 ∈ V ↦ ((𝑓 sSet 〈(Hom ‘ndx), tpos (Hom ‘𝑓)〉) sSet 〈(comp‘ndx), (𝑢 ∈ ((Base‘𝑓) × (Base‘𝑓)), 𝑧 ∈ (Base‘𝑓) ↦ tpos (〈𝑧, (2nd ‘𝑢)〉(comp‘𝑓)(1st ‘𝑢)))〉)) | ||
Theorem | oppcval 16196* | Value of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ 𝐻 = (Hom ‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝐶 ∈ 𝑉 → 𝑂 = ((𝐶 sSet 〈(Hom ‘ndx), tpos 𝐻〉) sSet 〈(comp‘ndx), (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st ‘𝑢)))〉)) | ||
Theorem | oppchomfval 16197 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ tpos 𝐻 = (Hom ‘𝑂) | ||
Theorem | oppchom 16198 | Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐻 = (Hom ‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) ⇒ ⊢ (𝑋(Hom ‘𝑂)𝑌) = (𝑌𝐻𝑋) | ||
Theorem | oppccofval 16199 | Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉(comp‘𝑂)𝑍) = tpos (〈𝑍, 𝑌〉 · 𝑋)) | ||
Theorem | oppcco 16200 | Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐵 = (Base‘𝐶) & ⊢ · = (comp‘𝐶) & ⊢ 𝑂 = (oppCat‘𝐶) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑍)𝐹) = (𝐹(〈𝑍, 𝑌〉 · 𝑋)𝐺)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |