imaidfu2

Description: The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025)

	Ref	Expression
Hypotheses	imaidfu.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
	imaidfu.d	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
	imaidfu.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	imaidfu.j	⊢ 𝐽 = ( Hom_f ‘ 𝐷 )
	imaidfu.k	⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
	imaidfu2.s	⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐷 ) )
Assertion	imaidfu2	⊢ ( 𝜑 → 𝐽 = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		imaidfu.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
2		imaidfu.d	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
3		imaidfu.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
4		imaidfu.j	⊢ 𝐽 = ( Hom_f ‘ 𝐷 )
5		imaidfu.k	⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
6		imaidfu2.s	⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐷 ) )
7		eqid	⊢ ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ) = ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
8		eqid	⊢ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) )
9	1 2 3 4 7 8	imaidfu	⊢ ( 𝜑 → ( 𝐽 ↾ ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) ) = ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ) )
10		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
11	1 2 10	idfu1sta	⊢ ( 𝜑 → ( 1^st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
12	11	imaeq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( ( I ↾ ( Base ‘ 𝐷 ) ) “ ( Base ‘ 𝐷 ) ) )
13		ssid	⊢ ( Base ‘ 𝐷 ) ⊆ ( Base ‘ 𝐷 )
14		resiima	⊢ ( ( Base ‘ 𝐷 ) ⊆ ( Base ‘ 𝐷 ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 ) )
15	13 14	ax-mp	⊢ ( ( I ↾ ( Base ‘ 𝐷 ) ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 )
16	12 15	eqtrdi	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 ) )
17	16	sqxpeqd	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
18	17	reseq2d	⊢ ( 𝜑 → ( 𝐽 ↾ ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) ) = ( 𝐽 ↾ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ) )
19		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
20	4 19	homffn	⊢ 𝐽 Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) )
21		fnresdm	⊢ ( 𝐽 Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) → ( 𝐽 ↾ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ) = 𝐽 )
22	20 21	ax-mp	⊢ ( 𝐽 ↾ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ) = 𝐽
23	18 22	eqtrdi	⊢ ( 𝜑 → ( 𝐽 ↾ ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) ) = 𝐽 )
24	15 12 6	3eqtr4a	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = 𝑆 )
25		eqidd	⊢ ( 𝜑 → ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
26	24 24 25	mpoeq123dv	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ) )
27	9 23 26	3eqtr3d	⊢ ( 𝜑 → 𝐽 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ) )
28	27 5	eqtr4di	⊢ ( 𝜑 → 𝐽 = 𝐾 )

Metamath Proof Explorer

Theorem imaidfu2

Proof