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	imaf1homlem	⊢ ( 𝜑 → ( { ( ^◡ 𝐹 ‘ 𝑋 ) } = ( ^◡ 𝐹 “ { 𝑋 } ) ∧ ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 ∧ ( ^◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )
18	17	simp3d	⊢ ( 𝜑 → ( ^◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
19	18	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ^◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ^◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ^◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
20	1 8 10	imaf1homlem	⊢ ( 𝜑 → ( { ( ^◡ 𝐹 ‘ 𝑌 ) } = ( ^◡ 𝐹 “ { 𝑌 } ) ∧ ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 ∧ ( ^◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) )
21	20	simp3d	⊢ ( 𝜑 → ( ^◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
22	21	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑌 ) ) ) ∧ ( ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 ) ∧ 𝑛 ∈ ( ( ^◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑍 ) ) ) ∧ ( ( ( ^◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑍 ) ) ‘ 𝑛 ) = 𝑁 ) → ( ^◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
23	1 8 11	imaf1homlem	⊢ ( 𝜑 → ( { ( ^◡ 𝐹 ‘ 𝑍 ) } = ( ^◡ 𝐹 “ { 𝑍 } ) ∧ ( 𝐹 ‘ ( ^◡ 𝐹 ‘ 𝑍 ) ) = 𝑍 ∧ ( ^◡ 𝐹 ‘ 𝑍 ) ∈ 𝐵 ) )
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	imaf1hom	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑍 ) = ( ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑍 ) ) ) )
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	imaf1hom	⊢ ( 𝜑 → ( 𝑌 𝐾 𝑍 ) = ( ( ( ^◡ 𝐹 ‘ 𝑌 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑍 ) ) “ ( ( ^◡ 𝐹 ‘ 𝑌 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑍 ) ) ) )
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	imaf1hom	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑌 ) ) ) )
65	12 64	eleqtrd	⊢ ( 𝜑 → 𝑀 ∈ ( ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑌 ) ) ) )
66		fvelima	⊢ ( ( Fun ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑌 ) ) ∧ 𝑀 ∈ ( ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑌 ) ) ) ) → ∃ 𝑚 ∈ ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑌 ) ) ( ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 )
67	63 65 66	syl2anc	⊢ ( 𝜑 → ∃ 𝑚 ∈ ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ^◡ 𝐹 ‘ 𝑌 ) ) ( ( ( ^◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ^◡ 𝐹 ‘ 𝑌 ) ) ‘ 𝑚 ) = 𝑀 )
68	61 67	r19.29a	⊢ ( 𝜑 → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) 𝑀 ) ∈ ( 𝑋 𝐾 𝑍 ) )

Metamath Proof Explorer

Theorem imaf1co

Proof