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

Metamath Proof Explorer

Theorem diagffth

Description: The diagonal functor is a fully faithful functor from a category C to the category of functors from a terminal category to C . (Contributed by Zhi Wang, 21-Oct-2025)

Ref Expression
Hypotheses diagffth.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
diagffth.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
diagffth.q ⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
diagffth.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
Assertion diagffth ( 𝜑 → 𝐿 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 diagffth.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 diagffth.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3 diagffth.q ⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
4 diagffth.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
5 relfunc ⊢ Rel ( 𝐶 Func 𝑄 )
6 2 termccd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
7 4 1 6 3 diagcl ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝑄 ) )
8 1st2nd ⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝑄 ) ) → 𝐿 = ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ )
9 5 7 8 sylancr ⊢ ( 𝜑 → 𝐿 = ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ )
10 7 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝐿 ) )
11 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
14 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
15 eqid ⊢ ( 𝐷 Nat 𝐶 ) = ( 𝐷 Nat 𝐶 )
16 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐷 ∈ TermCat )
17 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
18 4 11 12 13 14 15 16 17 diag2f1o ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) )
19 18 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) )
20 3 15 fuchom ⊢ ( 𝐷 Nat 𝐶 ) = ( Hom ‘ 𝑄 )
21 11 12 20 isffth2 ⊢ ( ( 1st ‘ 𝐿 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2nd ‘ 𝐿 ) ↔ ( ( 1st ‘ 𝐿 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝐿 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) ) )
22 10 19 21 sylanbrc ⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2nd ‘ 𝐿 ) )
23 df-br ⊢ ( ( 1st ‘ 𝐿 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2nd ‘ 𝐿 ) ↔ ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
24 22 23 sylib ⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
25 9 24 eqeltrd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )