This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
Assertion idemb ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ( 𝐼 ∈ ( 𝐷 Faith 𝐸 ) ∧ Fun ◡ ( 1st ‘ 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 idfth.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2 1 idfth ⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → 𝐼 ∈ ( 𝐷 Faith 𝐸 ) )
3 1 eleq1i ⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) ↔ ( idfunc ‘ 𝐶 ) ∈ ( 𝐷 Func 𝐸 ) )
4 idfurcl ⊢ ( ( idfunc ‘ 𝐶 ) ∈ ( 𝐷 Func 𝐸 ) → 𝐶 ∈ Cat )
5 3 4 sylbi ⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → 𝐶 ∈ Cat )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 1 6 idfu1stf1o ⊢ ( 𝐶 ∈ Cat → ( 1st ‘ 𝐼 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐶 ) )
8 dff1o4 ⊢ ( ( 1st ‘ 𝐼 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐶 ) ↔ ( ( 1st ‘ 𝐼 ) Fn ( Base ‘ 𝐶 ) ∧ ◡ ( 1st ‘ 𝐼 ) Fn ( Base ‘ 𝐶 ) ) )
9 8 simprbi ⊢ ( ( 1st ‘ 𝐼 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐶 ) → ◡ ( 1st ‘ 𝐼 ) Fn ( Base ‘ 𝐶 ) )
10 5 7 9 3syl ⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ◡ ( 1st ‘ 𝐼 ) Fn ( Base ‘ 𝐶 ) )
11 10 fnfund ⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → Fun ◡ ( 1st ‘ 𝐼 ) )
12 2 11 jca ⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ( 𝐼 ∈ ( 𝐷 Faith 𝐸 ) ∧ Fun ◡ ( 1st ‘ 𝐼 ) ) )