Metamath Proof Explorer

Theorem cofidfth

Description: If " F is a section of G " in a category of small categories (in a universe), then F is faithful. Combined with cofidf1 , this theorem proves that F is an embedding (a faithful functor injective on objects, remark 3.28(1) of Adamek p. 34). (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Hypotheses cofidfth.i ⊢ 𝐼 = ( idfunc ‘ 𝐷 )
cofidfth.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
cofidfth.k ⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
cofidfth.o ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
Assertion cofidfth ( 𝜑 → 𝐹 ( 𝐷 Faith 𝐸 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 cofidfth.i ⊢ 𝐼 = ( idfunc ‘ 𝐷 )
2 cofidfth.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
3 cofidfth.k ⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
4 cofidfth.o ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
5 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
7 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
8 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
9 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐷 ) )
12 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
13 1 5 6 7 8 9 10 11 12 cofidf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) : ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) –onto→ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
14 13 simpld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) )
15 14 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) )
16 5 9 10 isfth2 ⊢ ( 𝐹 ( 𝐷 Faith 𝐸 ) 𝐺 ↔ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1→ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) ) )
17 2 15 16 sylanbrc ⊢ ( 𝜑 → 𝐹 ( 𝐷 Faith 𝐸 ) 𝐺 )