Description: Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | subcrcl | ⊢ ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-subc | ⊢ Subcat = ( 𝑐 ∈ Cat ↦ { ℎ ∣ ( ℎ ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom ℎ / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ℎ 𝑧 ) ( 𝑔 ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ℎ 𝑧 ) ) ) } ) | |
2 | 1 | mptrcl | ⊢ ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat ) |