imaid

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

	Ref	Expression
Hypotheses	imasubc.s	$⊢ S = F [A]$
	imasubc.h	$⊢ H = Hom (D)$
	imasubc.k	$⊢ K = (x \in S, y \in S ⟼ ⋃_{p \in F^{-1} [\{x\}] \times F^{-1} [\{y\}]} G (p) [H (p)])$
	imassc.f	$⊢ φ \to F (D Func E) G$
	imaid.i	$⊢ I = Id (E)$
	imaid.x	$⊢ φ \to X \in S$
Assertion	imaid	$⊢ φ \to I (X) \in (X K X)$

Proof

Step	Hyp	Ref	Expression
1		imasubc.s	$⊢ S = F [A]$
2		imasubc.h	$⊢ H = Hom (D)$
3		imasubc.k	$⊢ K = (x \in S, y \in S ⟼ ⋃_{p \in F^{-1} [\{x\}] \times F^{-1} [\{y\}]} G (p) [H (p)])$
4		imassc.f	$⊢ φ \to F (D Func E) G$
5		imaid.i	$⊢ I = Id (E)$
6		imaid.x	$⊢ φ \to X \in S$
7	6 1	eleqtrdi	$⊢ φ \to X \in F [A]$
8		inisegn0a	$⊢ X \in F [A] \to F^{-1} [\{X\}] \neq \emptyset$
9	7 8	syl	$⊢ φ \to F^{-1} [\{X\}] \neq \emptyset$
10		n0	$⊢ F^{-1} [\{X\}] \neq \emptyset \leftrightarrow \exists m m \in F^{-1} [\{X\}]$
11	9 10	sylib	$⊢ φ \to \exists m m \in F^{-1} [\{X\}]$
12		fveq2	$⊢ p = ⟨m, m⟩ \to G (p) = G (⟨m, m⟩)$
13		df-ov	$⊢ m G m = G (⟨m, m⟩)$
14	12 13	eqtr4di	$⊢ p = ⟨m, m⟩ \to G (p) = m G m$
15		fveq2	$⊢ p = ⟨m, m⟩ \to H (p) = H (⟨m, m⟩)$
16		df-ov	$⊢ m H m = H (⟨m, m⟩)$
17	15 16	eqtr4di	$⊢ p = ⟨m, m⟩ \to H (p) = m H m$
18	14 17	imaeq12d	$⊢ p = ⟨m, m⟩ \to G (p) [H (p)] = (m G m) [m H m]$
19	18	eleq2d	$⊢ p = ⟨m, m⟩ \to (I (X) \in G (p) [H (p)] \leftrightarrow I (X) \in (m G m) [m H m])$
20		simpr	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to m \in F^{-1} [\{X\}]$
21	20 20	opelxpd	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to ⟨m, m⟩ \in (F^{-1} [\{X\}] \times F^{-1} [\{X\}])$
22		eqid	$⊢ {Base}_{D} = {Base}_{D}$
23		eqid	$⊢ Id (D) = Id (D)$
24	4	adantr	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to F (D Func E) G$
25		eqid	$⊢ {Base}_{E} = {Base}_{E}$
26	22 25 4	funcf1	$⊢ φ \to F : {Base}_{D} ⟶ {Base}_{E}$
27	26	ffnd	$⊢ φ \to F Fn {Base}_{D}$
28		fniniseg	$⊢ F Fn {Base}_{D} \to (m \in F^{-1} [\{X\}] \leftrightarrow (m \in {Base}_{D} \land F (m) = X))$
29	27 28	syl	$⊢ φ \to (m \in F^{-1} [\{X\}] \leftrightarrow (m \in {Base}_{D} \land F (m) = X))$
30	29	biimpa	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to (m \in {Base}_{D} \land F (m) = X)$
31	30	simpld	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to m \in {Base}_{D}$
32	22 23 5 24 31	funcid	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to (m G m) (Id (D) (m)) = I (F (m))$
33	30	simprd	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to F (m) = X$
34	33	fveq2d	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to I (F (m)) = I (X)$
35	32 34	eqtrd	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to (m G m) (Id (D) (m)) = I (X)$
36	24	funcrcl2	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to D \in Cat$
37	22 2 23 36 31	catidcl	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to Id (D) (m) \in (m H m)$
38		eqid	$⊢ Hom (E) = Hom (E)$
39	22 2 38 24 31 31	funcf2	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to (m G m) : m H m ⟶ F (m) Hom (E) F (m)$
40	39	funfvima2d	$⊢ ((φ \land m \in F^{-1} [\{X\}]) \land Id (D) (m) \in (m H m)) \to (m G m) (Id (D) (m)) \in (m G m) [m H m]$
41	37 40	mpdan	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to (m G m) (Id (D) (m)) \in (m G m) [m H m]$
42	35 41	eqeltrrd	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to I (X) \in (m G m) [m H m]$
43	19 21 42	rspcedvdw	$⊢ (φ \land m \in F^{-1} [\{X\}]) \to \exists p \in (F^{-1} [\{X\}] \times F^{-1} [\{X\}]) I (X) \in G (p) [H (p)]$
44	11 43	exlimddv	$⊢ φ \to \exists p \in (F^{-1} [\{X\}] \times F^{-1} [\{X\}]) I (X) \in G (p) [H (p)]$
45	44	eliund	$⊢ φ \to I (X) \in ⋃_{p \in F^{-1} [\{X\}] \times F^{-1} [\{X\}]} G (p) [H (p)]$
46		relfunc	$⊢ Rel (D Func E)$
47	46	brrelex1i	$⊢ F (D Func E) G \to F \in V$
48	4 47	syl	$⊢ φ \to F \in V$
49	48 48 6 6 3	imasubclem3	$⊢ φ \to X K X = ⋃_{p \in F^{-1} [\{X\}] \times F^{-1} [\{X\}]} G (p) [H (p)]$
50	45 49	eleqtrrd	$⊢ φ \to I (X) \in (X K X)$

Metamath Proof Explorer

Theorem imaid

Proof