P. 177 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17601-17700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mriss 17601	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 17602	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 17603	Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})))
Theorem	mrieqvd 17604*	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 17605*	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 17606	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 17593, and so are equal by mrieqv2d 17605.) (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑆 = 𝑇)
Theorem	mrissmrid 17607	In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝑇 ∈ 𝐼)
Theorem	mreexd 17608*	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 to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))    &   ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))
Theorem	mreexmrid 17609*	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 17610*	This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 17614. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾))    &   ⊢ (𝜑 → ∀𝑡∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼)))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexlem2d 17611*	Used in mreexexlem4d 17613 to prove the induction step in mreexexd 17614. 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 17612*	Base case of the induction in mreexexd 17614. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 = ∅ ∨ 𝐺 = ∅))    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ 𝒫 𝐺(𝐹 ≈ 𝑖 ∧ (𝑖 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexlem4d 17613*	Induction step of the induction in mreexexd 17614. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → 𝐿 ∈ ω)    &   ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐿 ∨ 𝑔 ≈ 𝐿) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼)))    &   ⊢ (𝜑 → (𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexexd 17614*	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 17612 for the base case and mreexexlem4d 17613 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5212 and ax-ac2 10385. (Revised by Brendan Leahy, 2-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))    &   ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)    &   ⊢ (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin))    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼))
Theorem	mreexdomd 17615*	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 17614. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇))    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑆 ∈ Fin ∨ 𝑇 ∈ Fin))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    ⇒   ⊢ (𝜑 → 𝑆 ≼ 𝑇)
Theorem	mreexfidimd 17616*	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 17615 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)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
7.2.3  Algebraic closure systems
Theorem	isacs 17617*	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 17618	Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋))
Theorem	isacs2 17619*	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 17620*	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 17621*	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 17622	An algebraic closure system is also a Moore system. Deduction form of acsmre 17618. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
Theorem	isacs1i 17623*	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 17624	Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))
Theorem	acsfn 17625*	Algebraicity of a conditional point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) ∧ (𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin)) → {𝑎 ∈ 𝒫 𝑋 ∣ (𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎)} ∈ (ACS‘𝑋))
Theorem	acsfn0 17626*	Algebraicity of a point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ 𝐾 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn1 17627*	Algebraicity of a one-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn1c 17628*	Algebraicity of a one-argument closure condition with additional constant. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝐾 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
Theorem	acsfn2 17629*	Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑏 ∈ 𝑋 ∀𝑐 ∈ 𝑋 𝐸 ∈ 𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 𝐸 ∈ 𝑎} ∈ (ACS‘𝑋))
PART 8  BASIC CATEGORY THEORY
8.1  Categories
8.1.1  Categories
Syntax	ccat 17630	Extend class notation with the class of categories.
class Cat
Syntax	ccid 17631	Extend class notation with the identity arrow of a category.
class Id
Syntax	chomf 17632	Extend class notation to include functionalized Hom-set extractor.
class Homf
Syntax	ccomf 17633	Extend class notation to include functionalized composition operation.
class compf
Definition	df-cat 17634*	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, without the axiom CAT 1, i.e., pairwise disjointness of hom-sets (cat1 18064). See setc2obas 18061 and setc2ohom 18062 for a counterexample. 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 17635. (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 17635*	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 17636*	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 17637*	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 17638*	The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥⟩ · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓))))))
Theorem	iscatd 17639*	Properties that determine a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝐵 = (Base‘𝐶))    &   ⊢ (𝜑 → 𝐻 = (Hom ‘𝐶))    &   ⊢ (𝜑 → · = (comp‘𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 1 ∈ (𝑥𝐻𝑥))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦𝐻𝑥))) → ( 1 (⟨𝑦, 𝑥⟩ · 𝑥)𝑓) = 𝑓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑓 ∈ (𝑥𝐻𝑦))) → (𝑓(⟨𝑥, 𝑥⟩ · 𝑦) 1 ) = 𝑓)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧))) → (𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓) ∈ (𝑥𝐻𝑧))    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(⟨𝑦, 𝑧⟩ · 𝑤)𝑔)(⟨𝑥, 𝑦⟩ · 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧⟩ · 𝑤)(𝑔(⟨𝑥, 𝑦⟩ · 𝑧)𝑓)))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Cat)
Theorem	catidex 17640*	Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋⟩ · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋⟩ · 𝑦)𝑔) = 𝑓))
Theorem	catideu 17641*	Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃!𝑔 ∈ (𝑋𝐻𝑋)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋⟩ · 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋⟩ · 𝑦)𝑔) = 𝑓))
Theorem	cidfval 17642*	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 17643*	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 17644	The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ Id Fn Cat
Theorem	cidfn 17645	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 17646*	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 17647*	Version of iscatd 17639 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 17648	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 17649	Left identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (( 1 ‘𝑌)(⟨𝑋, 𝑌⟩ · 𝑌)𝐹) = 𝐹)
Theorem	catrid 17650	Right identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    ⇒   ⊢ (𝜑 → (𝐹(⟨𝑋, 𝑋⟩ · 𝑌)( 1 ‘𝑋)) = 𝐹)
Theorem	catcocl 17651	Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ∈ (𝑋𝐻𝑍))
Theorem	catass 17652	Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊))    ⇒   ⊢ (𝜑 → ((𝐾(⟨𝑌, 𝑍⟩ · 𝑊)𝐺)(⟨𝑋, 𝑌⟩ · 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍⟩ · 𝑊)(𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)))
Theorem	catcone0 17653	Composition of non-empty hom-sets is non-empty. (Contributed by Zhi Wang, 18-Sep-2024.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋𝐻𝑌) ≠ ∅)    &   ⊢ (𝜑 → (𝑌𝐻𝑍) ≠ ∅)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑍) ≠ ∅)
Theorem	0catg 17654	Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ ((𝐶 ∈ 𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ Cat)
Theorem	0cat 17655	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 17656*	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    ⇒   ⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥𝐻𝑦))
Theorem	fnhomeqhomf 17657	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 17658	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = (𝑋𝐻𝑌))
Theorem	homffn 17659	The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐹 = (Homf ‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐹 Fn (𝐵 × 𝐵)
Theorem	homfeq 17660*	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 17661	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 17662	Deduce equality of base sets from equality of Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    ⇒   ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
Theorem	homfeqval 17663	Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝐽 = (Hom ‘𝐷)    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋𝐻𝑌) = (𝑋𝐽𝑌))
Theorem	comfffval 17664*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 1-Mar-2024.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))
Theorem	comffval 17665*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(⟨𝑋, 𝑌⟩ · 𝑍)𝑓)))
Theorem	comfval 17666	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
Theorem	comfffval2 17667*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    ⇒   ⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐻𝑦), 𝑓 ∈ (𝐻‘𝑥) ↦ (𝑔(𝑥 · 𝑦)𝑓)))
Theorem	comffval2 17668*	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) = (𝑔 ∈ (𝑌𝐻𝑍), 𝑓 ∈ (𝑋𝐻𝑌) ↦ (𝑔(⟨𝑋, 𝑌⟩ · 𝑍)𝑓)))
Theorem	comfval2 17669	Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
Theorem	comfffn 17670	The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝑂 Fn ((𝐵 × 𝐵) × 𝐵)
Theorem	comffn 17671	The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝑂 = (compf‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩𝑂𝑍) Fn ((𝑌𝐻𝑍) × (𝑋𝐻𝑌)))
Theorem	comfeq 17672*	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 17673	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 17674	Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ ∙ = (comp‘𝐷)    &   ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍))    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺(⟨𝑋, 𝑌⟩ ∙ 𝑍)𝐹))
Theorem	catpropd 17675	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 17676	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‘𝐷))
8.1.2  Opposite category
Syntax	coppc 17677	The opposite category operation.
class oppCat
Definition	df-oppc 17678*	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 17679*	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 17680	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ tpos 𝐻 = (Hom ‘𝑂)
Theorem	oppchom 17681	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝑋(Hom ‘𝑂)𝑌) = (𝑌𝐻𝑋)
Theorem	oppccofval 17682	Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩(comp‘𝑂)𝑍) = tpos (⟨𝑍, 𝑌⟩ · 𝑋))
Theorem	oppcco 17683	Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩(comp‘𝑂)𝑍)𝐹) = (𝐹(⟨𝑍, 𝑌⟩ · 𝑋)𝐺))
Theorem	oppcbas 17684	Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 18-Oct-2024.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	oppccatid 17685	Lemma for oppccat 17688. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧ (Id‘𝑂) = (Id‘𝐶)))
Theorem	oppchomf 17686	Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐻 = (Homf ‘𝐶)    ⇒   ⊢ tpos 𝐻 = (Homf ‘𝑂)
Theorem	oppcid 17687	Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Id‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 𝐵)
Theorem	oppccat 17688	An opposite category is a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
Theorem	2oppcbas 17689	The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd 17704. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ 𝐵 = (Base‘(oppCat‘𝑂))
Theorem	2oppchomf 17690	The double opposite category has the same morphisms as the original category. Intended for use with property lemmas such as monpropd 17704. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (Homf ‘𝐶) = (Homf ‘(oppCat‘𝑂))
Theorem	2oppccomf 17691	The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd 17704. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝑂 = (oppCat‘𝐶)    ⇒   ⊢ (compf‘𝐶) = (compf‘(oppCat‘𝑂))
Theorem	oppchomfpropd 17692	If two categories have the same hom-sets, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    ⇒   ⊢ (𝜑 → (Homf ‘(oppCat‘𝐶)) = (Homf ‘(oppCat‘𝐷)))
Theorem	oppccomfpropd 17693	If two categories have the same hom-sets and composition, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017.)
⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))    &   ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))    ⇒   ⊢ (𝜑 → (compf‘(oppCat‘𝐶)) = (compf‘(oppCat‘𝐷)))
Theorem	oppccatf 17694	oppCat restricted to Cat is a function from Cat to Cat. (Contributed by Zhi Wang, 29-Aug-2024.)
⊢ (oppCat ↾ Cat):Cat⟶Cat
8.1.3  Monomorphisms and epimorphisms
Syntax	cmon 17695	Extend class notation with the class of all monomorphisms.
class Mono
Syntax	cepi 17696	Extend class notation with the class of all epimorphisms.
class Epi
Definition	df-mon 17697*	Function returning the monomorphisms of the category 𝑐. JFM CAT1 def. 10. (Contributed by FL, 5-Dec-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Mono = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))
Definition	df-epi 17698	Function returning the epimorphisms of the category 𝑐. JFM CAT1 def. 11. (Contributed by FL, 8-Aug-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)
⊢ Epi = (𝑐 ∈ Cat ↦ tpos (Mono‘(oppCat‘𝑐)))
Theorem	monfval 17699*	Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    ⇒   ⊢ (𝜑 → 𝑀 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑓 ∈ (𝑥𝐻𝑦) ∣ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩ · 𝑦)𝑔))}))
Theorem	ismon 17700*	Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐻 = (Hom ‘𝐶)    &   ⊢ · = (comp‘𝐶)    &   ⊢ 𝑀 = (Mono‘𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑋𝑀𝑌) ↔ (𝐹 ∈ (𝑋𝐻𝑌) ∧ ∀𝑧 ∈ 𝐵 Fun ◡(𝑔 ∈ (𝑧𝐻𝑋) ↦ (𝐹(⟨𝑧, 𝑋⟩ · 𝑌)𝑔)))))