imaidfu

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

	Ref	Expression
Hypotheses	imaidfu.i	$⊢ I = {id}_{func} (C)$
	imaidfu.d	$⊢ φ \to I \in (D Func E)$
	imaidfu.h	$⊢ H = Hom (D)$
	imaidfu.j	$⊢ J = {Hom}_{𝑓} (D)$
	imaidfu.k	$⊢ K = (x \in S, y \in S ⟼ ⋃_{p \in {1^{st} (I)}^{-1} [\{x\}] \times {1^{st} (I)}^{-1} [\{y\}]} 2^{nd} (I) (p) [H (p)])$
	imaidfu.s	$⊢ S = 1^{st} (I) [A]$
Assertion	imaidfu	$⊢ φ \to {J ↾}_{(S \times S)} = K$

Proof

Step	Hyp	Ref	Expression
1		imaidfu.i	$⊢ I = {id}_{func} (C)$
2		imaidfu.d	$⊢ φ \to I \in (D Func E)$
3		imaidfu.h	$⊢ H = Hom (D)$
4		imaidfu.j	$⊢ J = {Hom}_{𝑓} (D)$
5		imaidfu.k	$⊢ K = (x \in S, y \in S ⟼ ⋃_{p \in {1^{st} (I)}^{-1} [\{x\}] \times {1^{st} (I)}^{-1} [\{y\}]} 2^{nd} (I) (p) [H (p)])$
6		imaidfu.s	$⊢ S = 1^{st} (I) [A]$
7		eqidd	$⊢ φ \to {Base}_{D} = {Base}_{D}$
8	1 2 7	idfu1sta	$⊢ φ \to 1^{st} (I) = {I ↾}_{{Base}_{D}}$
9	8	adantr	$⊢ (φ \land (z \in S \land w \in S)) \to 1^{st} (I) = {I ↾}_{{Base}_{D}}$
10	9	cnveqd	$⊢ (φ \land (z \in S \land w \in S)) \to {1^{st} (I)}^{-1} = {({I ↾}_{{Base}_{D}})}^{-1}$
11		cnvresid	$⊢ {({I ↾}_{{Base}_{D}})}^{-1} = {I ↾}_{{Base}_{D}}$
12	10 11	eqtrdi	$⊢ (φ \land (z \in S \land w \in S)) \to {1^{st} (I)}^{-1} = {I ↾}_{{Base}_{D}}$
13	12	fveq1d	$⊢ (φ \land (z \in S \land w \in S)) \to {1^{st} (I)}^{-1} (z) = ({I ↾}_{{Base}_{D}}) (z)$
14		imassrn	$⊢ 1^{st} (I) [A] \subseteq ran 1^{st} (I)$
15	6 14	eqsstri	$⊢ S \subseteq ran 1^{st} (I)$
16	8	rneqd	$⊢ φ \to ran 1^{st} (I) = ran ({I ↾}_{{Base}_{D}})$
17		rnresi	$⊢ ran ({I ↾}_{{Base}_{D}}) = {Base}_{D}$
18	16 17	eqtrdi	$⊢ φ \to ran 1^{st} (I) = {Base}_{D}$
19	15 18	sseqtrid	$⊢ φ \to S \subseteq {Base}_{D}$
20	19	adantr	$⊢ (φ \land (z \in S \land w \in S)) \to S \subseteq {Base}_{D}$
21		simprl	$⊢ (φ \land (z \in S \land w \in S)) \to z \in S$
22	20 21	sseldd	$⊢ (φ \land (z \in S \land w \in S)) \to z \in {Base}_{D}$
23		fvresi	$⊢ z \in {Base}_{D} \to ({I ↾}_{{Base}_{D}}) (z) = z$
24	22 23	syl	$⊢ (φ \land (z \in S \land w \in S)) \to ({I ↾}_{{Base}_{D}}) (z) = z$
25	13 24	eqtrd	$⊢ (φ \land (z \in S \land w \in S)) \to {1^{st} (I)}^{-1} (z) = z$
26	12	fveq1d	$⊢ (φ \land (z \in S \land w \in S)) \to {1^{st} (I)}^{-1} (w) = ({I ↾}_{{Base}_{D}}) (w)$
27		simprr	$⊢ (φ \land (z \in S \land w \in S)) \to w \in S$
28	20 27	sseldd	$⊢ (φ \land (z \in S \land w \in S)) \to w \in {Base}_{D}$
29		fvresi	$⊢ w \in {Base}_{D} \to ({I ↾}_{{Base}_{D}}) (w) = w$
30	28 29	syl	$⊢ (φ \land (z \in S \land w \in S)) \to ({I ↾}_{{Base}_{D}}) (w) = w$
31	26 30	eqtrd	$⊢ (φ \land (z \in S \land w \in S)) \to {1^{st} (I)}^{-1} (w) = w$
32	25 31	oveq12d	$⊢ (φ \land (z \in S \land w \in S)) \to {1^{st} (I)}^{-1} (z) 2^{nd} (I) {1^{st} (I)}^{-1} (w) = z 2^{nd} (I) w$
33	25 31	oveq12d	$⊢ (φ \land (z \in S \land w \in S)) \to {1^{st} (I)}^{-1} (z) H {1^{st} (I)}^{-1} (w) = z H w$
34	32 33	imaeq12d	$⊢ (φ \land (z \in S \land w \in S)) \to ({1^{st} (I)}^{-1} (z) 2^{nd} (I) {1^{st} (I)}^{-1} (w)) [{1^{st} (I)}^{-1} (z) H {1^{st} (I)}^{-1} (w)] = (z 2^{nd} (I) w) [z H w]$
35		f1oi	$⊢ ({I ↾}_{{Base}_{D}}) : {Base}_{D} \underset{1-1 onto}{⟶} {Base}_{D}$
36	9	f1oeq1d	$⊢ (φ \land (z \in S \land w \in S)) \to (1^{st} (I) : {Base}_{D} \underset{1-1 onto}{⟶} {Base}_{D} \leftrightarrow ({I ↾}_{{Base}_{D}}) : {Base}_{D} \underset{1-1 onto}{⟶} {Base}_{D})$
37	35 36	mpbiri	$⊢ (φ \land (z \in S \land w \in S)) \to 1^{st} (I) : {Base}_{D} \underset{1-1 onto}{⟶} {Base}_{D}$
38		f1of1	$⊢ 1^{st} (I) : {Base}_{D} \underset{1-1 onto}{⟶} {Base}_{D} \to 1^{st} (I) : {Base}_{D} \underset{1-1}{⟶} {Base}_{D}$
39	37 38	syl	$⊢ (φ \land (z \in S \land w \in S)) \to 1^{st} (I) : {Base}_{D} \underset{1-1}{⟶} {Base}_{D}$
40		fvexd	$⊢ (φ \land (z \in S \land w \in S)) \to 1^{st} (I) \in V$
41	6 39 21 27 40 5	imaf1hom	$⊢ (φ \land (z \in S \land w \in S)) \to z K w = ({1^{st} (I)}^{-1} (z) 2^{nd} (I) {1^{st} (I)}^{-1} (w)) [{1^{st} (I)}^{-1} (z) H {1^{st} (I)}^{-1} (w)]$
42		eqid	$⊢ {Base}_{D} = {Base}_{D}$
43	4 42 3 22 28	homfval	$⊢ (φ \land (z \in S \land w \in S)) \to z J w = z H w$
44	2	adantr	$⊢ (φ \land (z \in S \land w \in S)) \to I \in (D Func E)$
45		eqidd	$⊢ (φ \land (z \in S \land w \in S)) \to {Base}_{D} = {Base}_{D}$
46	3	oveqi	$⊢ z H w = z Hom (D) w$
47	46	a1i	$⊢ (φ \land (z \in S \land w \in S)) \to z H w = z Hom (D) w$
48	1 44 45 22 28 47	idfu2nda	$⊢ (φ \land (z \in S \land w \in S)) \to z 2^{nd} (I) w = {I ↾}_{(z H w)}$
49	48	imaeq1d	$⊢ (φ \land (z \in S \land w \in S)) \to (z 2^{nd} (I) w) [z H w] = ({I ↾}_{(z H w)}) [z H w]$
50		ssid	$⊢ z H w \subseteq z H w$
51		resiima	$⊢ z H w \subseteq z H w \to ({I ↾}_{(z H w)}) [z H w] = z H w$
52	50 51	ax-mp	$⊢ ({I ↾}_{(z H w)}) [z H w] = z H w$
53	49 52	eqtrdi	$⊢ (φ \land (z \in S \land w \in S)) \to (z 2^{nd} (I) w) [z H w] = z H w$
54	43 53	eqtr4d	$⊢ (φ \land (z \in S \land w \in S)) \to z J w = (z 2^{nd} (I) w) [z H w]$
55	34 41 54	3eqtr4rd	$⊢ (φ \land (z \in S \land w \in S)) \to z J w = z K w$
56	55	ralrimivva	$⊢ φ \to \forall z \in S \forall w \in S z J w = z K w$
57		fveq2	$⊢ q = ⟨z, w⟩ \to J (q) = J (⟨z, w⟩)$
58		df-ov	$⊢ z J w = J (⟨z, w⟩)$
59	57 58	eqtr4di	$⊢ q = ⟨z, w⟩ \to J (q) = z J w$
60		fveq2	$⊢ q = ⟨z, w⟩ \to K (q) = K (⟨z, w⟩)$
61		df-ov	$⊢ z K w = K (⟨z, w⟩)$
62	60 61	eqtr4di	$⊢ q = ⟨z, w⟩ \to K (q) = z K w$
63	59 62	eqeq12d	$⊢ q = ⟨z, w⟩ \to (J (q) = K (q) \leftrightarrow z J w = z K w)$
64	63	ralxp	$⊢ \forall q \in (S \times S) J (q) = K (q) \leftrightarrow \forall z \in S \forall w \in S z J w = z K w$
65	56 64	sylibr	$⊢ φ \to \forall q \in (S \times S) J (q) = K (q)$
66	4 42	homffn	$⊢ J Fn ({Base}_{D} \times {Base}_{D})$
67	66	a1i	$⊢ φ \to J Fn ({Base}_{D} \times {Base}_{D})$
68		fvexd	$⊢ φ \to 1^{st} (I) \in V$
69	68 68 5	imasubclem2	$⊢ φ \to K Fn (S \times S)$
70		xpss12	$⊢ (S \subseteq {Base}_{D} \land S \subseteq {Base}_{D}) \to S \times S \subseteq {Base}_{D} \times {Base}_{D}$
71	19 19 70	syl2anc	$⊢ φ \to S \times S \subseteq {Base}_{D} \times {Base}_{D}$
72		fvreseq1	$⊢ ((J Fn ({Base}_{D} \times {Base}_{D}) \land K Fn (S \times S)) \land S \times S \subseteq {Base}_{D} \times {Base}_{D}) \to ({J ↾}_{(S \times S)} = K \leftrightarrow \forall q \in (S \times S) J (q) = K (q))$
73	67 69 71 72	syl21anc	$⊢ φ \to ({J ↾}_{(S \times S)} = K \leftrightarrow \forall q \in (S \times S) J (q) = K (q))$
74	65 73	mpbird	$⊢ φ \to {J ↾}_{(S \times S)} = K$

Metamath Proof Explorer

Theorem imaidfu

Proof