Theorem issubc

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 )
	issubc.s	⊢ ( 𝜑 → 𝑆 = dom dom 𝐽 )
Assertion	issubc	⊢ ( 𝜑 → ( 𝐽 ∈ ( 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		issubc.s	⊢ ( 𝜑 → 𝑆 = dom dom 𝐽 )
6		simpl	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) → 𝐶 ∈ Cat )
7		sscpwex	⊢ { 𝑗 ∣ 𝑗 ⊆cat ( Homf ‘ 𝑐 ) } ∈ V
8		simpl	⊢ ( ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) → 𝑗 ⊆cat ( Homf ‘ 𝑐 ) )
9	8	ss2abi	⊢ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ⊆ { 𝑗 ∣ 𝑗 ⊆cat ( Homf ‘ 𝑐 ) }
10	7 9	ssexi	⊢ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ∈ V
11	10	csbex	⊢ ⦋ 𝐶 / 𝑐 ⦌ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ∈ V
12	11	a1i	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) → ⦋ 𝐶 / 𝑐 ⦌ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ∈ V )
13		df-subc	⊢ Subcat = ( 𝑐 ∈ Cat ↦ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } )
14	13	fvmpts	⊢ ( ( 𝐶 ∈ Cat ∧ ⦋ 𝐶 / 𝑐 ⦌ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ∈ V ) → ( Subcat ‘ 𝐶 ) = ⦋ 𝐶 / 𝑐 ⦌ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } )
15	6 12 14	syl2anc	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) → ( Subcat ‘ 𝐶 ) = ⦋ 𝐶 / 𝑐 ⦌ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } )
16	15	eleq2d	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ 𝐽 ∈ ⦋ 𝐶 / 𝑐 ⦌ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ) )
17		sbcel2	⊢ ( [ 𝐶 / 𝑐 ] 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ↔ 𝐽 ∈ ⦋ 𝐶 / 𝑐 ⦌ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } )
18	17	a1i	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) → ( [ 𝐶 / 𝑐 ] 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ↔ 𝐽 ∈ ⦋ 𝐶 / 𝑐 ⦌ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ) )
19		elex	⊢ ( 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } → 𝐽 ∈ V )
20	19	a1i	⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) → ( 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } → 𝐽 ∈ V ) )
21		sscrel	⊢ Rel ⊆cat
22	21	brrelex1i	⊢ ( 𝐽 ⊆cat 𝐻 → 𝐽 ∈ V )
23	22	adantr	⊢ ( ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) → 𝐽 ∈ V )
24	23	a1i	⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) → ( ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) → 𝐽 ∈ V ) )
25		df-sbc	⊢ ( [ 𝐽 / 𝑗 ] ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ↔ 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } )
26		simpr	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝐽 ∈ V ) → 𝐽 ∈ V )
27		simpr	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → 𝑗 = 𝐽 )
28		simpr	⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) → 𝑐 = 𝐶 )
29	28	fveq2d	⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) → ( Homf ‘ 𝑐 ) = ( Homf ‘ 𝐶 ) )
30	29 1	eqtr4di	⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) → ( Homf ‘ 𝑐 ) = 𝐻 )
31	30	adantr	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → ( Homf ‘ 𝑐 ) = 𝐻 )
32	27 31	breq12d	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ↔ 𝐽 ⊆cat 𝐻 ) )
33		vex	⊢ 𝑗 ∈ V
34	33	dmex	⊢ dom 𝑗 ∈ V
35	34	dmex	⊢ dom dom 𝑗 ∈ V
36	35	a1i	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → dom dom 𝑗 ∈ V )
37	27	dmeqd	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → dom 𝑗 = dom 𝐽 )
38	37	dmeqd	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → dom dom 𝑗 = dom dom 𝐽 )
39		simpllr	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → 𝑆 = dom dom 𝐽 )
40	38 39	eqtr4d	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → dom dom 𝑗 = 𝑆 )
41		simpr	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
42		simpllr	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → 𝑐 = 𝐶 )
43	42	fveq2d	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( Id ‘ 𝑐 ) = ( Id ‘ 𝐶 ) )
44	43 2	eqtr4di	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( Id ‘ 𝑐 ) = 1 )
45	44	fveq1d	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) = ( 1 ‘ 𝑥 ) )
46		simplr	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → 𝑗 = 𝐽 )
47	46	oveqd	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( 𝑥 𝑗 𝑥 ) = ( 𝑥 𝐽 𝑥 ) )
48	45 47	eleq12d	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ↔ ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ) )
49	46	oveqd	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( 𝑥 𝑗 𝑦 ) = ( 𝑥 𝐽 𝑦 ) )
50	46	oveqd	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( 𝑦 𝑗 𝑧 ) = ( 𝑦 𝐽 𝑧 ) )
51	42	fveq2d	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
52	51 3	eqtr4di	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( comp ‘ 𝑐 ) = · )
53	52	oveqd	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) )
54	53	oveqd	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) )
55	46	oveqd	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( 𝑥 𝑗 𝑧 ) = ( 𝑥 𝐽 𝑧 ) )
56	54 55	eleq12d	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
57	50 56	raleqbidv	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
58	49 57	raleqbidv	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
59	41 58	raleqbidv	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
60	41 59	raleqbidv	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ↔ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
61	48 60	anbi12d	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ↔ ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
62	41 61	raleqbidv	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
63	36 40 62	sbcied2	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → ( [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
64	32 63	anbi12d	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝑗 = 𝐽 ) → ( ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
65	64	adantlr	⊢ ( ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝐽 ∈ V ) ∧ 𝑗 = 𝐽 ) → ( ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
66	26 65	sbcied	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝐽 ∈ V ) → ( [ 𝐽 / 𝑗 ] ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
67	25 66	bitr3id	⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) ∧ 𝐽 ∈ V ) → ( 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
68	67	ex	⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) → ( 𝐽 ∈ V → ( 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) ) )
69	20 24 68	pm5.21ndd	⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) ∧ 𝑐 = 𝐶 ) → ( 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
70	6 69	sbcied	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) → ( [ 𝐶 / 𝑐 ] 𝐽 ∈ { 𝑗 ∣ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ [ dom dom 𝑗 / 𝑠 ] ∀ 𝑥 ∈ 𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) } ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
71	16 18 70	3bitr2d	⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽 ) → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
72	4 5 71	syl2anc	⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )