Step |
Hyp |
Ref |
Expression |
1 |
|
subcixp.1 |
⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) |
2 |
|
subcssc.h |
⊢ 𝐻 = ( Homf ‘ 𝐶 ) |
3 |
|
eqid |
⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 ) |
4 |
|
eqid |
⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) |
5 |
|
subcrcl |
⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat ) |
6 |
1 5
|
syl |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
7 |
|
eqidd |
⊢ ( 𝜑 → dom dom 𝐽 = dom dom 𝐽 ) |
8 |
2 3 4 6 7
|
issubc |
⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐽 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ dom dom 𝐽 ∀ 𝑧 ∈ dom dom 𝐽 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) ) |
9 |
1 8
|
mpbid |
⊢ ( 𝜑 → ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐽 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ dom dom 𝐽 ∀ 𝑧 ∈ dom dom 𝐽 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) |
10 |
9
|
simpld |
⊢ ( 𝜑 → 𝐽 ⊆cat 𝐻 ) |