Metamath Proof Explorer

Theorem funcsn

Description: The category of one functor to a thin category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses funcsn.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
funcsn.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
funcsn.c ⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { 𝐹 } )
funcsn.d ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
Assertion funcsn ( 𝜑 → 𝑄 ∈ TermCat )

Proof

Step Hyp Ref Expression
1 funcsn.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2 funcsn.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3 funcsn.c ⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { 𝐹 } )
4 funcsn.d ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
5 1 fucbas ⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
6 5 a1i ⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 ) )
7 eqid ⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
8 1 7 fuchom ⊢ ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 )
9 8 a1i ⊢ ( 𝜑 → ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 ) )
10 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
11 7 10 nat1st2nd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 ∈ ( ⟨ ( 1st ‘ 𝑓 ) , ( 2nd ‘ 𝑓 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) ⟩ ) )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 7 11 12 natfn ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 Fn ( Base ‘ 𝐶 ) )
14 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
15 7 14 nat1st2nd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑏 ∈ ( ⟨ ( 1st ‘ 𝑓 ) , ( 2nd ‘ 𝑓 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) ⟩ ) )
16 7 15 12 natfn ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑏 Fn ( Base ‘ 𝐶 ) )
17 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18 7 11 natrcl2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → ( 1st ‘ 𝑓 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝑓 ) )
19 12 17 18 funcf1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → ( 1st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
20 19 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
21 7 11 natrcl3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → ( 1st ‘ 𝑔 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝑔 ) )
22 12 17 21 funcf1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → ( 1st ‘ 𝑔 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
23 22 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
24 11 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑎 ∈ ( ⟨ ( 1st ‘ 𝑓 ) , ( 2nd ‘ 𝑓 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) ⟩ ) )
25 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
26 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
27 7 24 12 25 26 natcl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ ( ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ) )
28 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑏 ∈ ( ⟨ ( 1st ‘ 𝑓 ) , ( 2nd ‘ 𝑓 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) ⟩ ) )
29 7 28 12 25 26 natcl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑏 ‘ 𝑥 ) ∈ ( ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ) )
30 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ ThinCat )
31 20 23 27 29 17 25 30 thincmo2 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
32 13 16 31 eqfnfvd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ) ) → 𝑎 = 𝑏 )
33 32 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∀ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) 𝑎 = 𝑏 )
34 moel ⊢ ( ∃* 𝑎 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ↔ ∀ 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ∀ 𝑏 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) 𝑎 = 𝑏 )
35 33 34 sylibr ⊢ ( 𝜑 → ∃* 𝑎 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ∃* 𝑎 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) )
37 snidg ⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ { 𝐹 } )
38 2 37 syl ⊢ ( 𝜑 → 𝐹 ∈ { 𝐹 } )
39 38 3 eleqtrrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
40 39 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
41 40 funcrcl2 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
42 4 thinccatd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
43 1 41 42 fuccat ⊢ ( 𝜑 → 𝑄 ∈ Cat )
44 6 9 36 43 isthincd ⊢ ( 𝜑 → 𝑄 ∈ ThinCat )
45 sneq ⊢ ( 𝑓 = 𝐹 → { 𝑓 } = { 𝐹 } )
46 45 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝐶 Func 𝐷 ) = { 𝑓 } ↔ ( 𝐶 Func 𝐷 ) = { 𝐹 } ) )
47 2 3 46 spcedv ⊢ ( 𝜑 → ∃ 𝑓 ( 𝐶 Func 𝐷 ) = { 𝑓 } )
48 5 istermc ⊢ ( 𝑄 ∈ TermCat ↔ ( 𝑄 ∈ ThinCat ∧ ∃ 𝑓 ( 𝐶 Func 𝐷 ) = { 𝑓 } ) )
49 44 47 48 sylanbrc ⊢ ( 𝜑 → 𝑄 ∈ TermCat )