Metamath Proof Explorer

Theorem imaf1co

Description: An image of a functor whose object part is injective preserves the composition. (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imasubc.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
imassc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
imaf1co.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
imaf1co.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
imaf1co.o ⊢ ∙ = ( comp ‘ 𝐸 )
imaf1co.f ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐶 )
imaf1co.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
imaf1co.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
imaf1co.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
imaf1co.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐾 𝑌 ) )
imaf1co.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐾 𝑍 ) )
Assertion imaf1co ( 𝜑 → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝑀 ) ∈ ( 𝑋 𝐾 𝑍 ) )

Proof

Step Hyp Ref Expression
1 imasubc.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2 imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
3 imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
4 imassc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5 imaf1co.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
6 imaf1co.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
7 imaf1co.o ⊢ ∙ = ( comp ‘ 𝐸 )
8 imaf1co.f ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐶 )
9 imaf1co.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
10 imaf1co.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
11 imaf1co.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
12 imaf1co.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐾 𝑌 ) )
13 imaf1co.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐾 𝑍 ) )
14 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
15 4 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
16 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → 𝐷 ∈ Cat )
17 1 8 9 imasubc3lem1 ⊢ ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑋 ) } = ( ◡ 𝐹 “ { 𝑋 } ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )
18 17 simp3d ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
19 18 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
20 1 8 10 imasubc3lem1 ⊢ ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑌 ) } = ( ◡ 𝐹 “ { 𝑌 } ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 ∧ ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) )
21 20 simp3d ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
22 21 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
23 1 8 11 imasubc3lem1 ⊢ ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑍 ) } = ( ◡ 𝐹 “ { 𝑍 } ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) = 𝑍 ∧ ( ◡ 𝐹 ‘ 𝑍 ) ∈ 𝐵 ) )
24 23 simp3d ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝑍 ) ∈ 𝐵 )
25 24 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ◡ 𝐹 ‘ 𝑍 ) ∈ 𝐵 )
26 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) )
27 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) )
28 5 2 14 16 19 22 25 26 27 catcocl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( 𝑛 ( ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ◡ 𝐹 ‘ 𝑍 ) ) 𝑚 ) ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) )
29 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
30 5 2 29 4 18 24 funcf2 ⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) : ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ⟶ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
31 30 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) : ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ⟶ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
32 31 funfvima2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) ∧ ( 𝑛 ( ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ◡ 𝐹 ‘ 𝑍 ) ) 𝑚 ) ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) → ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ ( 𝑛 ( ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ◡ 𝐹 ‘ 𝑍 ) ) 𝑚 ) ) ∈ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
33 28 32 mpdan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ ( 𝑛 ( ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ◡ 𝐹 ‘ 𝑍 ) ) 𝑚 ) ) ∈ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
34 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
35 5 2 14 7 34 19 22 25 26 27 funcco ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ ( 𝑛 ( ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ◡ 𝐹 ‘ 𝑍 ) ) 𝑚 ) ) = ( ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ⟩ ∙ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) ) ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) ) )
36 17 simp2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 )
37 36 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 )
38 20 simp2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 )
39 38 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 )
40 37 39 opeq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ⟨ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
41 23 simp2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) = 𝑍 )
42 41 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) = 𝑍 )
43 40 42 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ⟨ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ⟩ ∙ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) ) = ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) )
44 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 )
45 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 )
46 43 44 45 oveq123d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ⟩ ∙ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) ) ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) ) = ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝑀 ) )
47 35 46 eqtr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝑀 ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ ( 𝑛 ( ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( ◡ 𝐹 ‘ 𝑍 ) ) 𝑚 ) ) )
48 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
49 48 brrelex1i ⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → 𝐹 ∈ V )
50 4 49 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
51 1 8 9 11 50 3 imasubc3lem2 ⊢ ( 𝜑 → ( 𝑋 𝐾 𝑍 ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
52 51 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( 𝑋 𝐾 𝑍 ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
53 33 47 52 3eltr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝑀 ) ∈ ( 𝑋 𝐾 𝑍 ) )
54 5 2 29 4 21 24 funcf2 ⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) : ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ⟶ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
55 54 ffund ⊢ ( 𝜑 → Fun ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) )
56 1 8 10 11 50 3 imasubc3lem2 ⊢ ( 𝜑 → ( 𝑌 𝐾 𝑍 ) = ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
57 13 56 eleqtrd ⊢ ( 𝜑 → 𝑁 ∈ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) )
58 fvelima ⊢ ( ( Fun ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ∧ 𝑁 ∈ ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ) ) → ∃ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 )
59 55 57 58 syl2anc ⊢ ( 𝜑 → ∃ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 )
60 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) → ∃ 𝑛 ∈ ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ◡ 𝐹 ‘ 𝑍 ) ) ( ( ( ◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 )
61 53 60 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝑀 ) ∈ ( 𝑋 𝐾 𝑍 ) )
62 5 2 29 4 18 21 funcf2 ⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) : ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ⟶ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ) )
63 62 ffund ⊢ ( 𝜑 → Fun ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) )
64 1 8 9 10 50 3 imasubc3lem2 ⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) )
65 12 64 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) )
66 fvelima ⊢ ( ( Fun ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ∧ 𝑀 ∈ ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) ) → ∃ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 )
67 63 65 66 syl2anc ⊢ ( 𝜑 → ∃ 𝑚 ∈ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 )
68 61 67 r19.29a ⊢ ( 𝜑 → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝑀 ) ∈ ( 𝑋 𝐾 𝑍 ) )