Theorem imaid

Description: An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025)

	Ref	Expression
Hypotheses	imasubc.s	⊢ 𝑆 = ( 𝐹 “ 𝐴 )
	imasubc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	imasubc.k	⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
	imassc.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	imaid.i	⊢ 𝐼 = ( Id ‘ 𝐸 )
	imaid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion	imaid	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝑋 𝐾 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		imasubc.s	⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2		imasubc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
3		imasubc.k	⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
4		imassc.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5		imaid.i	⊢ 𝐼 = ( Id ‘ 𝐸 )
6		imaid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
7	6 1	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 “ 𝐴 ) )
8		inisegn0a	⊢ ( 𝑋 ∈ ( 𝐹 “ 𝐴 ) → ( ◡ 𝐹 “ { 𝑋 } ) ≠ ∅ )
9	7 8	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑋 } ) ≠ ∅ )
10		n0	⊢ ( ( ◡ 𝐹 “ { 𝑋 } ) ≠ ∅ ↔ ∃ 𝑚 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) )
11	9 10	sylib	⊢ ( 𝜑 → ∃ 𝑚 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) )
12		fveq2	⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ ⟨ 𝑚 , 𝑚 ⟩ ) )
13		df-ov	⊢ ( 𝑚 𝐺 𝑚 ) = ( 𝐺 ‘ ⟨ 𝑚 , 𝑚 ⟩ )
14	12 13	eqtr4di	⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝑚 𝐺 𝑚 ) )
15		fveq2	⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝐻 ‘ ⟨ 𝑚 , 𝑚 ⟩ ) )
16		df-ov	⊢ ( 𝑚 𝐻 𝑚 ) = ( 𝐻 ‘ ⟨ 𝑚 , 𝑚 ⟩ )
17	15 16	eqtr4di	⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝑚 𝐻 𝑚 ) )
18	14 17	imaeq12d	⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) )
19	18	eleq2d	⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ↔ ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) ) )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) )
21	20 20	opelxpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ⟨ 𝑚 , 𝑚 ⟩ ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) )
22		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
23		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
24	4	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
25		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
26	22 25 4	funcf1	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
27	26	ffnd	⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝐷 ) )
28		fniniseg	⊢ ( 𝐹 Fn ( Base ‘ 𝐷 ) → ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ↔ ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑋 ) ) )
29	27 28	syl	⊢ ( 𝜑 → ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ↔ ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑋 ) ) )
30	29	biimpa	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑋 ) )
31	30	simpld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → 𝑚 ∈ ( Base ‘ 𝐷 ) )
32	22 23 5 24 31	funcid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( ( 𝑚 𝐺 𝑚 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑚 ) ) )
33	30	simprd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑚 ) = 𝑋 )
34	33	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑚 ) ) = ( 𝐼 ‘ 𝑋 ) )
35	32 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( ( 𝑚 𝐺 𝑚 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ) = ( 𝐼 ‘ 𝑋 ) )
36	24	funcrcl2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → 𝐷 ∈ Cat )
37	22 2 23 36 31	catidcl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ∈ ( 𝑚 𝐻 𝑚 ) )
38		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
39	22 2 38 24 31 31	funcf2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝑚 𝐺 𝑚 ) : ( 𝑚 𝐻 𝑚 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑚 ) ) )
40	39	funfvima2d	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) ∧ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ∈ ( 𝑚 𝐻 𝑚 ) ) → ( ( 𝑚 𝐺 𝑚 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ) ∈ ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) )
41	37 40	mpdan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( ( 𝑚 𝐺 𝑚 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ) ∈ ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) )
42	35 41	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) )
43	19 21 42	rspcedvdw	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ∃ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
44	11 43	exlimddv	⊢ ( 𝜑 → ∃ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
45	44	eliund	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
46		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
47	46	brrelex1i	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → 𝐹 ∈ V )
48	4 47	syl	⊢ ( 𝜑 → 𝐹 ∈ V )
49	48 48 6 6 3	imasubclem3	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑋 ) = ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
50	45 49	eleqtrrd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝑋 𝐾 𝑋 ) )