Metamath Proof Explorer

Theorem idfth

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

Ref Expression
Hypothesis idfth.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
Assertion idfth ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → 𝐼 ∈ ( 𝐷 Faith 𝐸 ) )

Proof

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