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