Metamath Proof Explorer


Theorem issubc2

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𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦𝑆𝑧𝑆𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦· 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )

Proof

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𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦𝑆𝑧𝑆𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦· 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )