idfth

Description: The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025)

		Ref	Expression
	Hypothesis	idfth.i	$⊢ I = {id}_{func} (C)$
	Assertion	idfth	$⊢ I \in (D Func E) \to I \in (D Faith E)$

Proof

Step	Hyp	Ref	Expression
1		idfth.i	$⊢ I = {id}_{func} (C)$
2		relfunc	$⊢ Rel (D Func E)$
3		1st2nd	$⊢ (Rel (D Func E) \land I \in (D Func E)) \to I = ⟨1^{st} (I), 2^{nd} (I)⟩$
4	2 3	mpan	$⊢ I \in (D Func E) \to I = ⟨1^{st} (I), 2^{nd} (I)⟩$
5		id	$⊢ I \in (D Func E) \to I \in (D Func E)$
6	5	func1st2nd	$⊢ I \in (D Func E) \to 1^{st} (I) (D Func E) 2^{nd} (I)$
7		f1oi	$⊢ ({I ↾}_{(x Hom (D) y)}) : x Hom (D) y \underset{1-1 onto}{⟶} x Hom (D) y$
8		dff1o3	$⊢ ({I ↾}_{(x Hom (D) y)}) : x Hom (D) y \underset{1-1 onto}{⟶} x Hom (D) y \leftrightarrow (({I ↾}_{(x Hom (D) y)}) : x Hom (D) y \underset{onto}{⟶} x Hom (D) y \land Fun {({I ↾}_{(x Hom (D) y)})}^{-1})$
9	7 8	mpbi	$⊢ (({I ↾}_{(x Hom (D) y)}) : x Hom (D) y \underset{onto}{⟶} x Hom (D) y \land Fun {({I ↾}_{(x Hom (D) y)})}^{-1})$
10	9	simpri	$⊢ Fun {({I ↾}_{(x Hom (D) y)})}^{-1}$
11		simpl	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to I \in (D Func E)$
12		eqidd	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to {Base}_{D} = {Base}_{D}$
13		simprl	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to x \in {Base}_{D}$
14		simprr	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to y \in {Base}_{D}$
15		eqidd	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to x Hom (D) y = x Hom (D) y$
16	1 11 12 13 14 15	idfu2nda	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to x 2^{nd} (I) y = {I ↾}_{(x Hom (D) y)}$
17	16	cnveqd	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to {(x 2^{nd} (I) y)}^{-1} = {({I ↾}_{(x Hom (D) y)})}^{-1}$
18	17	funeqd	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to (Fun {(x 2^{nd} (I) y)}^{-1} \leftrightarrow Fun {({I ↾}_{(x Hom (D) y)})}^{-1})$
19	10 18	mpbiri	$⊢ (I \in (D Func E) \land (x \in {Base}_{D} \land y \in {Base}_{D})) \to Fun {(x 2^{nd} (I) y)}^{-1}$
20	19	ralrimivva	$⊢ I \in (D Func E) \to \forall x \in {Base}_{D} \forall y \in {Base}_{D} Fun {(x 2^{nd} (I) y)}^{-1}$
21		eqid	$⊢ {Base}_{D} = {Base}_{D}$
22	21	isfth	$⊢ 1^{st} (I) (D Faith E) 2^{nd} (I) \leftrightarrow (1^{st} (I) (D Func E) 2^{nd} (I) \land \forall x \in {Base}_{D} \forall y \in {Base}_{D} Fun {(x 2^{nd} (I) y)}^{-1})$
23	6 20 22	sylanbrc	$⊢ I \in (D Func E) \to 1^{st} (I) (D Faith E) 2^{nd} (I)$
24		df-br	$⊢ 1^{st} (I) (D Faith E) 2^{nd} (I) \leftrightarrow ⟨1^{st} (I), 2^{nd} (I)⟩ \in (D Faith E)$
25	23 24	sylib	$⊢ I \in (D Func E) \to ⟨1^{st} (I), 2^{nd} (I)⟩ \in (D Faith E)$
26	4 25	eqeltrd	$⊢ I \in (D Func E) \to I \in (D Faith E)$

Metamath Proof Explorer

Theorem idfth

Proof