Theorem idfth 49964

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

Hypothesis

Ref	Expression
idfth.i	⊢ 𝐼 = (idfunc‘𝐶)

Assertion

Ref	Expression
idfth	⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸))

Proof of Theorem idfth

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relfunc 17925	. . 3 ⊢ Rel (𝐷 Func 𝐸)
2		1st2nd 8034	. . 3 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝐼 ∈ (𝐷 Func 𝐸)) → 𝐼 = ⟨(1st ‘𝐼), (2nd ‘𝐼)⟩)
3	1, 2	mpan 702	. 2 ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 = ⟨(1st ‘𝐼), (2nd ‘𝐼)⟩)
4		id 23	. . . . 5 ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Func 𝐸))
5	4	func1st2nd 49882	. . . 4 ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → (1st ‘𝐼)(𝐷 Func 𝐸)(2nd ‘𝐼))
6		f1oi 6859	. . . . . . . 8 ⊢ ( I ↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(𝑥(Hom ‘𝐷)𝑦)
7		dff1o3 6827	. . . . . . . 8 ⊢ (( I ↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(𝑥(Hom ‘𝐷)𝑦) ↔ (( I ↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–onto→(𝑥(Hom ‘𝐷)𝑦) ∧ Fun ◡( I ↾ (𝑥(Hom ‘𝐷)𝑦))))
8	6, 7	mpbi 233	. . . . . . 7 ⊢ (( I ↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–onto→(𝑥(Hom ‘𝐷)𝑦) ∧ Fun ◡( I ↾ (𝑥(Hom ‘𝐷)𝑦)))
9	8	simpri 490	. . . . . 6 ⊢ Fun ◡( I ↾ (𝑥(Hom ‘𝐷)𝑦))
10		idfth.i	. . . . . . . . 9 ⊢ 𝐼 = (idfunc‘𝐶)
11		simpl 487	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝐼 ∈ (𝐷 Func 𝐸))
12		eqidd 2763	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Base‘𝐷) = (Base‘𝐷))
13		simprl 782	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑥 ∈ (Base‘𝐷))
14		simprr 784	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑦 ∈ (Base‘𝐷))
15		eqidd 2763	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(Hom ‘𝐷)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
16	10, 11, 12, 13, 14, 15	idfu2nda 49909	. . . . . . . 8 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(2nd ‘𝐼)𝑦) = ( I ↾ (𝑥(Hom ‘𝐷)𝑦)))
17	16	cnveqd 5860	. . . . . . 7 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ◡(𝑥(2nd ‘𝐼)𝑦) = ◡( I ↾ (𝑥(Hom ‘𝐷)𝑦)))
18	17	funeqd 6558	. . . . . 6 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Fun ◡(𝑥(2nd ‘𝐼)𝑦) ↔ Fun ◡( I ↾ (𝑥(Hom ‘𝐷)𝑦))))
19	9, 18	mpbiri 261	. . . . 5 ⊢ ((𝐼 ∈ (𝐷 Func 𝐸) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → Fun ◡(𝑥(2nd ‘𝐼)𝑦))
20	19	ralrimivva 3207	. . . 4 ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → ∀𝑥 ∈ (Base‘𝐷)∀𝑦 ∈ (Base‘𝐷)Fun ◡(𝑥(2nd ‘𝐼)𝑦))
21		eqid 2762	. . . . 5 ⊢ (Base‘𝐷) = (Base‘𝐷)
22	21	isfth 17979	. . . 4 ⊢ ((1st ‘𝐼)(𝐷 Faith 𝐸)(2nd ‘𝐼) ↔ ((1st ‘𝐼)(𝐷 Func 𝐸)(2nd ‘𝐼) ∧ ∀𝑥 ∈ (Base‘𝐷)∀𝑦 ∈ (Base‘𝐷)Fun ◡(𝑥(2nd ‘𝐼)𝑦)))
23	5, 20, 22	sylanbrc 594	. . 3 ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → (1st ‘𝐼)(𝐷 Faith 𝐸)(2nd ‘𝐼))
24		df-br 5109	. . 3 ⊢ ((1st ‘𝐼)(𝐷 Faith 𝐸)(2nd ‘𝐼) ↔ ⟨(1st ‘𝐼), (2nd ‘𝐼)⟩ ∈ (𝐷 Faith 𝐸))
25	23, 24	sylib 221	. 2 ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → ⟨(1st ‘𝐼), (2nd ‘𝐼)⟩ ∈ (𝐷 Faith 𝐸))
26	3, 25	eqeltrd 2862	1 ⊢ (𝐼 ∈ (𝐷 Func 𝐸) → 𝐼 ∈ (𝐷 Faith 𝐸))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569   ∈ wcel 2142  ∀wral 3078  ⟨cop 4594   class class class wbr 5108   I cid 5554  ^◡ccnv 5659   ↾ cres 5662  Rel wrel 5665  Fun wfun 6530  –onto→wfo 6534  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7412  1^st c1st 7982  2^nd c2nd 7983  Basecbs 17275  Hom chom 17327   Func cfunc 17917  id_funccidfu 17918   Faith cfth 17968

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7984  df-2nd 7985  df-map 8824  df-ixp 8894  df-cat 17730  df-cid 17731  df-homf 17732  df-func 17921  df-idfu 17922  df-fth 17970

This theorem is used by:  idemb  49965