Metamath Proof Explorer

Theorem idemb

Description: The inclusion functor is an embedding. Remark 4.4(1) in Adamek p. 49. (Contributed by Zhi Wang, 16-Nov-2025)

Ref Expression
Hypothesis idfth.i ⊢ I = id func ⁡ C
Assertion idemb ⊢ I ∈ D Func E → I ∈ D Faith E ∧ Fun ⁡ 1 st ⁡ I -1

Proof

Step Hyp Ref Expression
1 idfth.i ⊢ I = id func ⁡ C
2 1 idfth ⊢ I ∈ D Func E → I ∈ D Faith E
3 1 eleq1i ⊢ I ∈ D Func E ↔ id func ⁡ C ∈ D Func E
4 idfurcl ⊢ id func ⁡ C ∈ D Func E → C ∈ Cat
5 3 4 sylbi ⊢ I ∈ D Func E → C ∈ Cat
6 eqid ⊢ Base C = Base C
7 1 6 idfu1stf1o ⊢ C ∈ Cat → 1 st ⁡ I : Base C ⟶ 1-1 onto Base C
8 dff1o4 ⊢ 1 st ⁡ I : Base C ⟶ 1-1 onto Base C ↔ 1 st ⁡ I Fn Base C ∧ 1 st ⁡ I -1 Fn Base C
9 8 simprbi ⊢ 1 st ⁡ I : Base C ⟶ 1-1 onto Base C → 1 st ⁡ I -1 Fn Base C
10 5 7 9 3syl ⊢ I ∈ D Func E → 1 st ⁡ I -1 Fn Base C
11 10 fnfund ⊢ I ∈ D Func E → Fun ⁡ 1 st ⁡ I -1
12 2 11 jca ⊢ I ∈ D Func E → I ∈ D Faith E ∧ Fun ⁡ 1 st ⁡ I -1