imaidfu

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 ‘ 𝐼 ) ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
	imaidfu.s	⊢ 𝑆 = ( ( 1^st ‘ 𝐼 ) “ 𝐴 )
Assertion	imaidfu	⊢ ( 𝜑 → ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 )

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		imaidfu.s	⊢ 𝑆 = ( ( 1^st ‘ 𝐼 ) “ 𝐴 )
7		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
8	1 2 7	idfu1sta	⊢ ( 𝜑 → ( 1^st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 1^st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
10	9	cnveqd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ^◡ ( 1^st ‘ 𝐼 ) = ^◡ ( I ↾ ( Base ‘ 𝐷 ) ) )
11		cnvresid	⊢ ^◡ ( I ↾ ( Base ‘ 𝐷 ) ) = ( I ↾ ( Base ‘ 𝐷 ) )
12	10 11	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ^◡ ( 1^st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
13	12	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑧 ) = ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑧 ) )
14		imassrn	⊢ ( ( 1^st ‘ 𝐼 ) “ 𝐴 ) ⊆ ran ( 1^st ‘ 𝐼 )
15	6 14	eqsstri	⊢ 𝑆 ⊆ ran ( 1^st ‘ 𝐼 )
16	8	rneqd	⊢ ( 𝜑 → ran ( 1^st ‘ 𝐼 ) = ran ( I ↾ ( Base ‘ 𝐷 ) ) )
17		rnresi	⊢ ran ( I ↾ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 )
18	16 17	eqtrdi	⊢ ( 𝜑 → ran ( 1^st ‘ 𝐼 ) = ( Base ‘ 𝐷 ) )
19	15 18	sseqtrid	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐷 ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝐷 ) )
21		simprl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑧 ∈ 𝑆 )
22	20 21	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
23		fvresi	⊢ ( 𝑧 ∈ ( Base ‘ 𝐷 ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑧 ) = 𝑧 )
24	22 23	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑧 ) = 𝑧 )
25	13 24	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑧 ) = 𝑧 )
26	12	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑤 ) = ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑤 ) )
27		simprr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑤 ∈ 𝑆 )
28	20 27	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑤 ∈ ( Base ‘ 𝐷 ) )
29		fvresi	⊢ ( 𝑤 ∈ ( Base ‘ 𝐷 ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑤 ) = 𝑤 )
30	28 29	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( I ↾ ( Base ‘ 𝐷 ) ) ‘ 𝑤 ) = 𝑤 )
31	26 30	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑤 ) = 𝑤 )
32	25 31	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑧 ) ( 2^nd ‘ 𝐼 ) ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑤 ) ) = ( 𝑧 ( 2^nd ‘ 𝐼 ) 𝑤 ) )
33	25 31	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑧 ) 𝐻 ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑤 ) ) = ( 𝑧 𝐻 𝑤 ) )
34	32 33	imaeq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑧 ) ( 2^nd ‘ 𝐼 ) ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑤 ) ) “ ( ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑧 ) 𝐻 ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑤 ) ) ) = ( ( 𝑧 ( 2^nd ‘ 𝐼 ) 𝑤 ) “ ( 𝑧 𝐻 𝑤 ) ) )
35		f1oi	⊢ ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 )
36	9	f1oeq1d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( 1^st ‘ 𝐼 ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 ) ↔ ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 ) ) )
37	35 36	mpbiri	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 1^st ‘ 𝐼 ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 ) )
38		f1of1	⊢ ( ( 1^st ‘ 𝐼 ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 ) → ( 1^st ‘ 𝐼 ) : ( Base ‘ 𝐷 ) –1-1→ ( Base ‘ 𝐷 ) )
39	37 38	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 1^st ‘ 𝐼 ) : ( Base ‘ 𝐷 ) –1-1→ ( Base ‘ 𝐷 ) )
40		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 1^st ‘ 𝐼 ) ∈ V )
41	6 39 21 27 40 5	imaf1hom	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐾 𝑤 ) = ( ( ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑧 ) ( 2^nd ‘ 𝐼 ) ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑤 ) ) “ ( ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑧 ) 𝐻 ( ^◡ ( 1^st ‘ 𝐼 ) ‘ 𝑤 ) ) ) )
42		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
43	4 42 3 22 28	homfval	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐻 𝑤 ) )
44	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
45		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
46	3	oveqi	⊢ ( 𝑧 𝐻 𝑤 ) = ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 )
47	46	a1i	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐻 𝑤 ) = ( 𝑧 ( Hom ‘ 𝐷 ) 𝑤 ) )
48	1 44 45 22 28 47	idfu2nda	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 ( 2^nd ‘ 𝐼 ) 𝑤 ) = ( I ↾ ( 𝑧 𝐻 𝑤 ) ) )
49	48	imaeq1d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐼 ) 𝑤 ) “ ( 𝑧 𝐻 𝑤 ) ) = ( ( I ↾ ( 𝑧 𝐻 𝑤 ) ) “ ( 𝑧 𝐻 𝑤 ) ) )
50		ssid	⊢ ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐻 𝑤 )
51		resiima	⊢ ( ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐻 𝑤 ) → ( ( I ↾ ( 𝑧 𝐻 𝑤 ) ) “ ( 𝑧 𝐻 𝑤 ) ) = ( 𝑧 𝐻 𝑤 ) )
52	50 51	ax-mp	⊢ ( ( I ↾ ( 𝑧 𝐻 𝑤 ) ) “ ( 𝑧 𝐻 𝑤 ) ) = ( 𝑧 𝐻 𝑤 )
53	49 52	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐼 ) 𝑤 ) “ ( 𝑧 𝐻 𝑤 ) ) = ( 𝑧 𝐻 𝑤 ) )
54	43 53	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐽 𝑤 ) = ( ( 𝑧 ( 2^nd ‘ 𝐼 ) 𝑤 ) “ ( 𝑧 𝐻 𝑤 ) ) )
55	34 41 54	3eqtr4rd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐾 𝑤 ) )
56	55	ralrimivva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐾 𝑤 ) )
57		fveq2	⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐽 ‘ 𝑞 ) = ( 𝐽 ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
58		df-ov	⊢ ( 𝑧 𝐽 𝑤 ) = ( 𝐽 ‘ ⟨ 𝑧 , 𝑤 ⟩ )
59	57 58	eqtr4di	⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐽 ‘ 𝑞 ) = ( 𝑧 𝐽 𝑤 ) )
60		fveq2	⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐾 ‘ 𝑞 ) = ( 𝐾 ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
61		df-ov	⊢ ( 𝑧 𝐾 𝑤 ) = ( 𝐾 ‘ ⟨ 𝑧 , 𝑤 ⟩ )
62	60 61	eqtr4di	⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐾 ‘ 𝑞 ) = ( 𝑧 𝐾 𝑤 ) )
63	59 62	eqeq12d	⊢ ( 𝑞 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) ↔ ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐾 𝑤 ) ) )
64	63	ralxp	⊢ ( ∀ 𝑞 ∈ ( 𝑆 × 𝑆 ) ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) ↔ ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( 𝑧 𝐽 𝑤 ) = ( 𝑧 𝐾 𝑤 ) )
65	56 64	sylibr	⊢ ( 𝜑 → ∀ 𝑞 ∈ ( 𝑆 × 𝑆 ) ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) )
66	4 42	homffn	⊢ 𝐽 Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) )
67	66	a1i	⊢ ( 𝜑 → 𝐽 Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
68		fvexd	⊢ ( 𝜑 → ( 1^st ‘ 𝐼 ) ∈ V )
69	68 68 5	imasubclem2	⊢ ( 𝜑 → 𝐾 Fn ( 𝑆 × 𝑆 ) )
70		xpss12	⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝐷 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐷 ) ) → ( 𝑆 × 𝑆 ) ⊆ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
71	19 19 70	syl2anc	⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ⊆ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
72		fvreseq1	⊢ ( ( ( 𝐽 Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ∧ 𝐾 Fn ( 𝑆 × 𝑆 ) ) ∧ ( 𝑆 × 𝑆 ) ⊆ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 ↔ ∀ 𝑞 ∈ ( 𝑆 × 𝑆 ) ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) ) )
73	67 69 71 72	syl21anc	⊢ ( 𝜑 → ( ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 ↔ ∀ 𝑞 ∈ ( 𝑆 × 𝑆 ) ( 𝐽 ‘ 𝑞 ) = ( 𝐾 ‘ 𝑞 ) ) )
74	65 73	mpbird	⊢ ( 𝜑 → ( 𝐽 ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 )

Metamath Proof Explorer

Theorem imaidfu

Proof