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