Metamath Proof Explorer

Theorem 0fucterm

Description: The category of functors from an initial category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses 0fucterm.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
0fucterm.b ⊢ ( 𝜑 → ∅ = ( Base ‘ 𝐶 ) )
0fucterm.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
0fucterm.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
Assertion 0fucterm ( 𝜑 → 𝑄 ∈ TermCat )

Proof

Step Hyp Ref Expression
1 0fucterm.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
2 0fucterm.b ⊢ ( 𝜑 → ∅ = ( Base ‘ 𝐶 ) )
3 0fucterm.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
4 0fucterm.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
5 4 fucbas ⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
6 5 a1i ⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 ) )
7 eqid ⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
8 4 7 fuchom ⊢ ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 )
9 8 a1i ⊢ ( 𝜑 → ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 ) )
10 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
11 7 10 nat1st2nd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 ∈ ( ⟨ ( 1st ‘ 𝑓 ) , ( 2nd ‘ 𝑓 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) ⟩ ) )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 7 11 12 natfn ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 Fn ( Base ‘ 𝐶 ) )
14 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → ∅ = ( Base ‘ 𝐶 ) )
15 14 fneq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → ( 𝑎 Fn ∅ ↔ 𝑎 Fn ( Base ‘ 𝐶 ) ) )
16 13 15 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 Fn ∅ )
17 fn0 ⊢ ( 𝑎 Fn ∅ ↔ 𝑎 = ∅ )
18 16 17 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 = ∅ )
19 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
20 7 19 nat1st2nd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑏 ∈ ( ⟨ ( 1st ‘ 𝑓 ) , ( 2nd ‘ 𝑓 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) ⟩ ) )
21 7 20 12 natfn ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑏 Fn ( Base ‘ 𝐶 ) )
22 14 fneq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → ( 𝑏 Fn ∅ ↔ 𝑏 Fn ( Base ‘ 𝐶 ) ) )
23 21 22 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑏 Fn ∅ )
24 fn0 ⊢ ( 𝑏 Fn ∅ ↔ 𝑏 = ∅ )
25 23 24 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑏 = ∅ )
26 18 25 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 = 𝑏 )
27 26 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ∀ 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∀ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) 𝑎 = 𝑏 )
28 moel ⊢ ( ∃* 𝑎 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ↔ ∀ 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∀ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) 𝑎 = 𝑏 )
29 27 28 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ∃* 𝑎 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
30 0catg ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
31 1 2 30 syl2anc ⊢ ( 𝜑 → 𝐶 ∈ Cat )
32 4 31 3 fuccat ⊢ ( 𝜑 → 𝑄 ∈ Cat )
33 6 9 29 32 isthincd ⊢ ( 𝜑 → 𝑄 ∈ ThinCat )
34 opex ⊢ ⟨ ∅ , ∅ ⟩ ∈ V
35 34 a1i ⊢ ( 𝜑 → ⟨ ∅ , ∅ ⟩ ∈ V )
36 1 2 3 0funcg ⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { ⟨ ∅ , ∅ ⟩ } )
37 sneq ⊢ ( 𝑓 = ⟨ ∅ , ∅ ⟩ → { 𝑓 } = { ⟨ ∅ , ∅ ⟩ } )
38 37 eqeq2d ⊢ ( 𝑓 = ⟨ ∅ , ∅ ⟩ → ( ( 𝐶 Func 𝐷 ) = { 𝑓 } ↔ ( 𝐶 Func 𝐷 ) = { ⟨ ∅ , ∅ ⟩ } ) )
39 35 36 38 spcedv ⊢ ( 𝜑 → ∃ 𝑓 ( 𝐶 Func 𝐷 ) = { 𝑓 } )
40 5 istermc ⊢ ( 𝑄 ∈ TermCat ↔ ( 𝑄 ∈ ThinCat ∧ ∃ 𝑓 ( 𝐶 Func 𝐷 ) = { 𝑓 } ) )
41 33 39 40 sylanbrc ⊢ ( 𝜑 → 𝑄 ∈ TermCat )