Metamath Proof Explorer

Theorem parmapfunc

Description: A map fixing the identity value and preserving the parallel-arrow class induces an endofunctor fixing every object. Category membership and the hom construction suffice: every composable pair contains an identity. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses parmapfunc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
parmapfunc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
parmapfunc.c ⊢ 𝐶 ∈ Cat
parmapfunc.hv ⊢ 𝐻 = ( 𝑟 ∈ 𝐵 , 𝑠 ∈ 𝐵 ↦ if ( 𝑟 = 𝑠 , { 𝐽 } , if ( ( 𝑟 = 𝑋 ∧ 𝑠 = 𝑌 ) , 𝑆 , ∅ ) ) )
parmapfunc.l ⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
parmapfunc.ai ⊢ ( 𝐴 ‘ 𝐽 ) = 𝐽
parmapfunc.as ⊢ ∀ 𝑡 ∈ 𝑆 ( 𝐴 ‘ 𝑡 ) ∈ 𝑆
Assertion parmapfunc ( I ↾ 𝐵 ) ( 𝐶 Func 𝐶 ) 𝐿

Proof

Step Hyp Ref Expression
1 parmapfunc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 parmapfunc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 parmapfunc.c ⊢ 𝐶 ∈ Cat
4 parmapfunc.hv ⊢ 𝐻 = ( 𝑟 ∈ 𝐵 , 𝑠 ∈ 𝐵 ↦ if ( 𝑟 = 𝑠 , { 𝐽 } , if ( ( 𝑟 = 𝑋 ∧ 𝑠 = 𝑌 ) , 𝑆 , ∅ ) ) )
5 parmapfunc.l ⊢ 𝐿 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
6 parmapfunc.ai ⊢ ( 𝐴 ‘ 𝐽 ) = 𝐽
7 parmapfunc.as ⊢ ∀ 𝑡 ∈ 𝑆 ( 𝐴 ‘ 𝑡 ) ∈ 𝑆
8 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
10 3 a1i ⊢ ( ⊤ → 𝐶 ∈ Cat )
11 f1oi ⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵
12 f1of ⊢ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
13 11 12 mp1i ⊢ ( ⊤ → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
14 5 fnmpompt ⊢ 𝐿 Fn ( 𝐵 × 𝐵 )
15 14 a1i ⊢ ( ⊤ → 𝐿 Fn ( 𝐵 × 𝐵 ) )
16 simprl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
17 simprr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
18 5 16 17 ovmpomptd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐿 𝑦 ) = ( 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
19 simpr ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ) → 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) )
20 6 a1i ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
21 fveq2 ⊢ ( 𝑡 = 𝑎 → ( 𝐴 ‘ 𝑡 ) = ( 𝐴 ‘ 𝑎 ) )
22 21 eleq1d ⊢ ( 𝑡 = 𝑎 → ( ( 𝐴 ‘ 𝑡 ) ∈ 𝑆 ↔ ( 𝐴 ‘ 𝑎 ) ∈ 𝑆 ) )
23 22 7 vtoclri ⊢ ( 𝑎 ∈ 𝑆 → ( 𝐴 ‘ 𝑎 ) ∈ 𝑆 )
24 23 adantl ⊢ ( ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ) ∧ 𝑎 ∈ 𝑆 ) → ( 𝐴 ‘ 𝑎 ) ∈ 𝑆 )
25 4 19 20 24 parmapcl ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑎 ∈ ( 𝑥 𝐻 𝑦 ) ) → ( 𝐴 ‘ 𝑎 ) ∈ ( 𝑥 𝐻 𝑦 ) )
26 18 25 fmpt3d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐿 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( 𝑥 𝐻 𝑦 ) )
27 fvresi ⊢ ( 𝑥 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
28 16 27 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
29 fvresi ⊢ ( 𝑦 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
30 17 29 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
31 28 30 oveq12d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) 𝐻 ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑥 𝐻 𝑦 ) )
32 31 feq3d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 𝐿 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) 𝐻 ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ( 𝑥 𝐿 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( 𝑥 𝐻 𝑦 ) ) )
33 26 32 mpbird ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐿 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) 𝐻 ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) )
34 3 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ Cat )
35 simpr ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
36 1 2 4 34 35 paridval ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) = 𝐽 )
37 36 fveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝐿 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( 𝑥 𝐿 𝑥 ) ‘ 𝐽 ) )
38 6 eqcomi ⊢ 𝐽 = ( 𝐴 ‘ 𝐽 )
39 38 fvexi ⊢ 𝐽 ∈ V
40 4 39 35 parhomid ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → 𝐽 ∈ ( 𝑥 𝐻 𝑥 ) )
41 5 35 35 40 fvmpomptd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝐿 𝑥 ) ‘ 𝐽 ) = ( 𝐴 ‘ 𝐽 ) )
42 37 41 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝐿 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( 𝐴 ‘ 𝐽 ) )
43 27 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
44 43 fveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
45 44 36 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ) = 𝐽 )
46 6 42 45 3eqtr4a ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 𝐿 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ) )
47 fvif ⊢ ( 𝐴 ‘ if ( 𝑥 = 𝑦 , 𝑛 , 𝑚 ) ) = if ( 𝑥 = 𝑦 , ( 𝐴 ‘ 𝑛 ) , ( 𝐴 ‘ 𝑚 ) )
48 3 a1i ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝐶 ∈ Cat )
49 simp3l ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) )
50 simp3r ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) )
51 1 2 4 48 9 49 50 parcoval2 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑚 ) = if ( 𝑥 = 𝑦 , 𝑛 , 𝑚 ) )
52 51 fveq2d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑚 ) ) = ( ( 𝑥 𝐿 𝑧 ) ‘ if ( 𝑥 = 𝑦 , 𝑛 , 𝑚 ) ) )
53 simp21 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑥 ∈ 𝐵 )
54 simp23 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
55 simp22 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑦 ∈ 𝐵 )
56 1 2 9 48 53 55 54 49 50 catcocl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑚 ) ∈ ( 𝑥 𝐻 𝑧 ) )
57 51 56 eqeltrrd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → if ( 𝑥 = 𝑦 , 𝑛 , 𝑚 ) ∈ ( 𝑥 𝐻 𝑧 ) )
58 5 53 54 57 fvmpomptd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ if ( 𝑥 = 𝑦 , 𝑛 , 𝑚 ) ) = ( 𝐴 ‘ if ( 𝑥 = 𝑦 , 𝑛 , 𝑚 ) ) )
59 52 58 eqtrd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑚 ) ) = ( 𝐴 ‘ if ( 𝑥 = 𝑦 , 𝑛 , 𝑚 ) ) )
60 53 27 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
61 55 29 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
62 60 61 opeq12d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
63 fvresi ⊢ ( 𝑧 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑧 ) = 𝑧 )
64 54 63 syl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑧 ) = 𝑧 )
65 62 64 oveq12d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ 𝐵 ) ‘ 𝑧 ) ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) )
66 5 55 54 50 fvmpomptd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑦 𝐿 𝑧 ) ‘ 𝑛 ) = ( 𝐴 ‘ 𝑛 ) )
67 5 53 55 49 fvmpomptd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑚 ) = ( 𝐴 ‘ 𝑚 ) )
68 65 66 67 oveq123d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( ( 𝑦 𝐿 𝑧 ) ‘ 𝑛 ) ( ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ 𝐵 ) ‘ 𝑧 ) ) ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑚 ) ) = ( ( 𝐴 ‘ 𝑛 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝐴 ‘ 𝑚 ) ) )
69 6 a1i ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
70 fveq2 ⊢ ( 𝑡 = 𝑚 → ( 𝐴 ‘ 𝑡 ) = ( 𝐴 ‘ 𝑚 ) )
71 70 eleq1d ⊢ ( 𝑡 = 𝑚 → ( ( 𝐴 ‘ 𝑡 ) ∈ 𝑆 ↔ ( 𝐴 ‘ 𝑚 ) ∈ 𝑆 ) )
72 71 7 vtoclri ⊢ ( 𝑚 ∈ 𝑆 → ( 𝐴 ‘ 𝑚 ) ∈ 𝑆 )
73 72 adantl ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) ∧ 𝑚 ∈ 𝑆 ) → ( 𝐴 ‘ 𝑚 ) ∈ 𝑆 )
74 4 49 69 73 parmapcl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ 𝑚 ) ∈ ( 𝑥 𝐻 𝑦 ) )
75 fveq2 ⊢ ( 𝑡 = 𝑛 → ( 𝐴 ‘ 𝑡 ) = ( 𝐴 ‘ 𝑛 ) )
76 75 eleq1d ⊢ ( 𝑡 = 𝑛 → ( ( 𝐴 ‘ 𝑡 ) ∈ 𝑆 ↔ ( 𝐴 ‘ 𝑛 ) ∈ 𝑆 ) )
77 76 7 vtoclri ⊢ ( 𝑛 ∈ 𝑆 → ( 𝐴 ‘ 𝑛 ) ∈ 𝑆 )
78 77 adantl ⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) ∧ 𝑛 ∈ 𝑆 ) → ( 𝐴 ‘ 𝑛 ) ∈ 𝑆 )
79 4 50 69 78 parmapcl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝐴 ‘ 𝑛 ) ∈ ( 𝑦 𝐻 𝑧 ) )
80 1 2 4 48 9 74 79 parcoval2 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝐴 ‘ 𝑛 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝐴 ‘ 𝑚 ) ) = if ( 𝑥 = 𝑦 , ( 𝐴 ‘ 𝑛 ) , ( 𝐴 ‘ 𝑚 ) ) )
81 68 80 eqtrd ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( ( 𝑦 𝐿 𝑧 ) ‘ 𝑛 ) ( ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ 𝐵 ) ‘ 𝑧 ) ) ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑚 ) ) = if ( 𝑥 = 𝑦 , ( 𝐴 ‘ 𝑛 ) , ( 𝐴 ‘ 𝑚 ) ) )
82 47 59 81 3eqtr4a ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( ( 𝑥 𝐿 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐿 𝑧 ) ‘ 𝑛 ) ( ⟨ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) , ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( ( I ↾ 𝐵 ) ‘ 𝑧 ) ) ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑚 ) ) )
83 1 1 2 2 8 8 9 9 10 10 13 15 33 46 82 isfuncd ⊢ ( ⊤ → ( I ↾ 𝐵 ) ( 𝐶 Func 𝐶 ) 𝐿 )
84 83 mptru ⊢ ( I ↾ 𝐵 ) ( 𝐶 Func 𝐶 ) 𝐿