Metamath Proof Explorer

Theorem discsubc

Description: A discrete category, whose only morphisms are the identity morphisms, is a subcategory. (Contributed by Zhi Wang, 1-Nov-2025)

Ref Expression
Hypotheses discsubc.j ⊢ 𝐽 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
discsubc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
discsubc.i ⊢ 𝐼 = ( Id ‘ 𝐶 )
discsubc.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
discsubc.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion discsubc ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 discsubc.j ⊢ 𝐽 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
2 discsubc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 discsubc.i ⊢ 𝐼 = ( Id ‘ 𝐶 )
4 discsubc.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
5 discsubc.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
6 eqeq12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 = 𝑦 ↔ 𝑎 = 𝑏 ) )
7 simpl ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑥 = 𝑎 )
8 7 fveq2d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑎 ) )
9 8 sneqd ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → { ( 𝐼 ‘ 𝑥 ) } = { ( 𝐼 ‘ 𝑎 ) } )
10 6 9 ifbieq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) = if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) )
11 snex ⊢ { ( 𝐼 ‘ 𝑎 ) } ∈ V
12 0ex ⊢ ∅ ∈ V
13 11 12 ifex ⊢ if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) ∈ V
14 10 1 13 ovmpoa ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 𝐽 𝑏 ) = if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 𝐽 𝑏 ) = if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) )
16 sseq1 ⊢ ( { ( 𝐼 ‘ 𝑎 ) } = if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) → ( { ( 𝐼 ‘ 𝑎 ) } ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) ↔ if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) ) )
17 sseq1 ⊢ ( ∅ = if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) → ( ∅ ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) ↔ if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) ) )
18 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
19 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → 𝐶 ∈ Cat )
20 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → 𝑆 ⊆ 𝐵 )
21 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → 𝑎 ∈ 𝑆 )
22 20 21 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → 𝑎 ∈ 𝐵 )
23 2 18 3 19 22 catidcl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → ( 𝐼 ‘ 𝑎 ) ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑎 ) )
24 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
25 24 2 18 22 22 homfval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → ( 𝑎 ( Homf ‘ 𝐶 ) 𝑎 ) = ( 𝑎 ( Hom ‘ 𝐶 ) 𝑎 ) )
26 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → 𝑎 = 𝑏 )
27 26 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → ( 𝑎 ( Homf ‘ 𝐶 ) 𝑎 ) = ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) )
28 25 27 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → ( 𝑎 ( Hom ‘ 𝐶 ) 𝑎 ) = ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) )
29 23 28 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → ( 𝐼 ‘ 𝑎 ) ∈ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) )
30 29 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ 𝑎 = 𝑏 ) → { ( 𝐼 ‘ 𝑎 ) } ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) )
31 0ss ⊢ ∅ ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 )
32 31 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) ∧ ¬ 𝑎 = 𝑏 ) → ∅ ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) )
33 16 17 30 32 ifbothda ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) )
34 15 33 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 𝐽 𝑏 ) ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) )
35 34 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ( 𝑎 𝐽 𝑏 ) ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) )
36 1 discsubclem ⊢ 𝐽 Fn ( 𝑆 × 𝑆 )
37 36 a1i ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
38 24 2 homffn ⊢ ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 )
39 38 a1i ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) )
40 2 fvexi ⊢ 𝐵 ∈ V
41 40 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
42 37 39 41 isssc ⊢ ( 𝜑 → ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ( 𝑎 𝐽 𝑏 ) ⊆ ( 𝑎 ( Homf ‘ 𝐶 ) 𝑏 ) ) ) )
43 4 35 42 mpbir2and ⊢ ( 𝜑 → 𝐽 ⊆cat ( Homf ‘ 𝐶 ) )
44 fvex ⊢ ( 𝐼 ‘ 𝑎 ) ∈ V
45 44 snid ⊢ ( 𝐼 ‘ 𝑎 ) ∈ { ( 𝐼 ‘ 𝑎 ) }
46 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 )
47 equtr2 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → 𝑥 = 𝑦 )
48 47 iftrued ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) = { ( 𝐼 ‘ 𝑥 ) } )
49 simpl ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → 𝑥 = 𝑎 )
50 49 fveq2d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑎 ) )
51 50 sneqd ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → { ( 𝐼 ‘ 𝑥 ) } = { ( 𝐼 ‘ 𝑎 ) } )
52 48 51 eqtrd ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑎 ) → if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) = { ( 𝐼 ‘ 𝑎 ) } )
53 52 1 11 ovmpoa ⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 𝐽 𝑎 ) = { ( 𝐼 ‘ 𝑎 ) } )
54 46 46 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 𝐽 𝑎 ) = { ( 𝐼 ‘ 𝑎 ) } )
55 45 54 eleqtrrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑎 ) ∈ ( 𝑎 𝐽 𝑎 ) )
56 45 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝐼 ‘ 𝑎 ) ∈ { ( 𝐼 ‘ 𝑎 ) } )
57 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) )
58 46 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑎 ∈ 𝑆 )
59 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑏 ∈ 𝑆 )
60 58 59 14 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑎 𝐽 𝑏 ) = if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) )
61 57 60 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑓 ∈ if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) )
62 61 ne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) ≠ ∅ )
63 iffalse ⊢ ( ¬ 𝑎 = 𝑏 → if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) = ∅ )
64 63 necon1ai ⊢ ( if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) ≠ ∅ → 𝑎 = 𝑏 )
65 62 64 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑎 = 𝑏 )
66 65 opeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ⟨ 𝑎 , 𝑎 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
67 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) )
68 eqeq12 ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑐 ) → ( 𝑥 = 𝑦 ↔ 𝑏 = 𝑐 ) )
69 simpl ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑐 ) → 𝑥 = 𝑏 )
70 69 fveq2d ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑐 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑏 ) )
71 70 sneqd ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑐 ) → { ( 𝐼 ‘ 𝑥 ) } = { ( 𝐼 ‘ 𝑏 ) } )
72 68 71 ifbieq1d ⊢ ( ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑐 ) → if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) = if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) )
73 snex ⊢ { ( 𝐼 ‘ 𝑏 ) } ∈ V
74 73 12 ifex ⊢ if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) ∈ V
75 72 1 74 ovmpoa ⊢ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) → ( 𝑏 𝐽 𝑐 ) = if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) )
76 75 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑏 𝐽 𝑐 ) = if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) )
77 67 76 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑔 ∈ if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) )
78 77 ne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) ≠ ∅ )
79 iffalse ⊢ ( ¬ 𝑏 = 𝑐 → if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) = ∅ )
80 79 necon1ai ⊢ ( if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) ≠ ∅ → 𝑏 = 𝑐 )
81 78 80 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑏 = 𝑐 )
82 65 81 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑎 = 𝑐 )
83 66 82 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( ⟨ 𝑎 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑎 ) = ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) )
84 83 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) = ( ⟨ 𝑎 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑎 ) )
85 81 iftrued ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → if ( 𝑏 = 𝑐 , { ( 𝐼 ‘ 𝑏 ) } , ∅ ) = { ( 𝐼 ‘ 𝑏 ) } )
86 77 85 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑔 ∈ { ( 𝐼 ‘ 𝑏 ) } )
87 86 elsnd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑔 = ( 𝐼 ‘ 𝑏 ) )
88 65 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝐼 ‘ 𝑎 ) = ( 𝐼 ‘ 𝑏 ) )
89 87 88 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑔 = ( 𝐼 ‘ 𝑎 ) )
90 65 iftrued ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → if ( 𝑎 = 𝑏 , { ( 𝐼 ‘ 𝑎 ) } , ∅ ) = { ( 𝐼 ‘ 𝑎 ) } )
91 61 90 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑓 ∈ { ( 𝐼 ‘ 𝑎 ) } )
92 91 elsnd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑓 = ( 𝐼 ‘ 𝑎 ) )
93 84 89 92 oveq123d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) = ( ( 𝐼 ‘ 𝑎 ) ( ⟨ 𝑎 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑎 ) ( 𝐼 ‘ 𝑎 ) ) )
94 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝐶 ∈ Cat )
95 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑆 ⊆ 𝐵 )
96 95 58 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → 𝑎 ∈ 𝐵 )
97 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
98 2 18 3 94 96 catidcl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝐼 ‘ 𝑎 ) ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑎 ) )
99 2 18 3 94 96 97 96 98 catlid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( ( 𝐼 ‘ 𝑎 ) ( ⟨ 𝑎 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑎 ) ( 𝐼 ‘ 𝑎 ) ) = ( 𝐼 ‘ 𝑎 ) )
100 93 99 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) = ( 𝐼 ‘ 𝑎 ) )
101 82 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑎 𝐽 𝑎 ) = ( 𝑎 𝐽 𝑐 ) )
102 58 58 53 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑎 𝐽 𝑎 ) = { ( 𝐼 ‘ 𝑎 ) } )
103 101 102 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑎 𝐽 𝑐 ) = { ( 𝐼 ‘ 𝑎 ) } )
104 56 100 103 3eltr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ) ) → ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐽 𝑐 ) )
105 104 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) → ∀ 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐽 𝑐 ) )
106 105 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ∀ 𝑏 ∈ 𝑆 ∀ 𝑐 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐽 𝑐 ) )
107 55 106 jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝐼 ‘ 𝑎 ) ∈ ( 𝑎 𝐽 𝑎 ) ∧ ∀ 𝑏 ∈ 𝑆 ∀ 𝑐 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐽 𝑐 ) ) )
108 107 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( ( 𝐼 ‘ 𝑎 ) ∈ ( 𝑎 𝐽 𝑎 ) ∧ ∀ 𝑏 ∈ 𝑆 ∀ 𝑐 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐽 𝑐 ) ) )
109 24 3 97 5 37 issubc2 ⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ 𝑆 ( ( 𝐼 ‘ 𝑎 ) ∈ ( 𝑎 𝐽 𝑎 ) ∧ ∀ 𝑏 ∈ 𝑆 ∀ 𝑐 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑎 𝐽 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐽 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐽 𝑐 ) ) ) ) )
110 43 108 109 mpbir2and ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )