This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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