Metamath Proof Explorer

Theorem issubc3

Description: Alternate definition of a subcategory, as a subset of the category which is itself a category. The assumption that the identity be closed is necessary just as in the case of a monoid, issubm2 , for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses issubc3.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
issubc3.i ⊢ 1 = ( Id ‘ 𝐶 )
issubc3.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
issubc3.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
issubc3.a ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
Assertion issubc3 ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) )

Proof

Step Hyp Ref Expression
1 issubc3.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
2 issubc3.i ⊢ 1 = ( Id ‘ 𝐶 )
3 issubc3.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
4 issubc3.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 issubc3.a ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
6 simpr ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
7 6 1 subcssc ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → 𝐽 ⊆cat 𝐻 )
8 6 adantr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
9 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐽 Fn ( 𝑆 × 𝑆 ) )
10 simpr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
11 8 9 10 2 subcidcl ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
12 11 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
13 3 6 subccat ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
14 7 12 13 3jca ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) )
15 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) → 𝐽 ⊆cat 𝐻 )
16 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) → ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
17 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
19 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
20 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐷 ∈ Cat )
21 simprl1 ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑥 ∈ 𝑆 )
22 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
23 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐶 ∈ Cat )
24 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐽 Fn ( 𝑆 × 𝑆 ) )
25 1 22 homffn ⊢ 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
26 25 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
27 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐽 ⊆cat 𝐻 )
28 24 26 27 ssc1 ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
29 3 22 23 24 28 rescbas ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑆 = ( Base ‘ 𝐷 ) )
30 21 29 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐷 ) )
31 simprl2 ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑦 ∈ 𝑆 )
32 31 29 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
33 simprl3 ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑧 ∈ 𝑆 )
34 33 29 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
35 simprrl ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) )
36 3 22 23 24 28 reschom ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝐽 = ( Hom ‘ 𝐷 ) )
37 36 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑥 𝐽 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
38 35 37 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
39 simprrr ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) )
40 36 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑦 𝐽 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
41 39 40 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
42 17 18 19 20 30 32 34 38 41 catcocl ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑧 ) )
43 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
44 3 22 23 24 28 43 rescco ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐷 ) )
45 44 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) )
46 45 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) )
47 36 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑥 𝐽 𝑧 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑧 ) )
48 42 46 47 3eltr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) )
49 48 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) )
50 49 ralrimivva ⊢ ( ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) )
51 50 ralrimivvva ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) )
52 51 3adantr2 ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) )
53 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
54 16 52 53 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) → ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
55 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) → 𝐶 ∈ Cat )
56 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) → 𝐽 Fn ( 𝑆 × 𝑆 ) )
57 1 2 43 55 56 issubc2 ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
58 15 54 57 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
59 14 58 impbida ⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat 𝐻 ∧ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ 𝐷 ∈ Cat ) ) )