Description: Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | issubc.h | ⊢ 𝐻 = ( Homf ‘ 𝐶 ) | |
issubc.i | ⊢ 1 = ( Id ‘ 𝐶 ) | ||
issubc.o | ⊢ · = ( comp ‘ 𝐶 ) | ||
issubc.c | ⊢ ( 𝜑 → 𝐶 ∈ Cat ) | ||
issubc2.a | ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) ) | ||
Assertion | issubc2 | ⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( 〈 𝑥 , 𝑦 〉 · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issubc.h | ⊢ 𝐻 = ( Homf ‘ 𝐶 ) | |
2 | issubc.i | ⊢ 1 = ( Id ‘ 𝐶 ) | |
3 | issubc.o | ⊢ · = ( comp ‘ 𝐶 ) | |
4 | issubc.c | ⊢ ( 𝜑 → 𝐶 ∈ Cat ) | |
5 | issubc2.a | ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) ) | |
6 | 5 | fndmd | ⊢ ( 𝜑 → dom 𝐽 = ( 𝑆 × 𝑆 ) ) |
7 | 6 | dmeqd | ⊢ ( 𝜑 → dom dom 𝐽 = dom ( 𝑆 × 𝑆 ) ) |
8 | dmxpid | ⊢ dom ( 𝑆 × 𝑆 ) = 𝑆 | |
9 | 7 8 | eqtr2di | ⊢ ( 𝜑 → 𝑆 = dom dom 𝐽 ) |
10 | 1 2 3 4 9 | issubc | ⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( 〈 𝑥 , 𝑦 〉 · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) ) |