Metamath Proof Explorer

Theorem idfudiag1

Description: If the identity functor of a category is the same as a constant functor to the category, then the category is terminal. (Contributed by Zhi Wang, 19-Oct-2025)

Ref Expression
Hypotheses idfudiag1.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
idfudiag1.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐶 )
idfudiag1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
idfudiag1.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
idfudiag1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
idfudiag1.k ⊢ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 )
idfudiag1.e ⊢ ( 𝜑 → 𝐼 = 𝐾 )
Assertion idfudiag1 ( 𝜑 → 𝐶 ∈ TermCat )

Proof

Step Hyp Ref Expression
1 idfudiag1.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2 idfudiag1.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐶 )
3 idfudiag1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 idfudiag1.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
5 idfudiag1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 idfudiag1.k ⊢ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 )
7 idfudiag1.e ⊢ ( 𝜑 → 𝐼 = 𝐾 )
8 4 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
9 eqidd ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
10 fveq2 ⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
11 df-ov ⊢ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ 𝑦 , 𝑧 ⟩ )
12 10 11 eqtr4di ⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
13 12 reseq2d ⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) = ( I ↾ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) )
14 13 mpompt ⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( I ↾ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) )
15 14 a1i ⊢ ( 𝜑 → ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( I ↾ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) )
16 ovex ⊢ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∈ V
17 resiexg ⊢ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∈ V → ( I ↾ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ∈ V )
18 16 17 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( I ↾ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ∈ V )
19 15 18 ovmpt4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) 𝑧 ) = ( I ↾ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) )
20 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
21 1 4 3 20 idfuval ⊢ ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ⟩ )
22 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
23 2 3 3 4 5 6 4 20 22 diag1a ⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ )
24 7 21 23 3eqtr3d ⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ⟩ = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ )
25 4 fvexi ⊢ 𝐵 ∈ V
26 resiexg ⊢ ( 𝐵 ∈ V → ( I ↾ 𝐵 ) ∈ V )
27 25 26 ax-mp ⊢ ( I ↾ 𝐵 ) ∈ V
28 25 25 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
29 28 mptex ⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ∈ V
30 27 29 opth ⊢ ( ⟨ ( I ↾ 𝐵 ) , ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ⟩ = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ ↔ ( ( I ↾ 𝐵 ) = ( 𝐵 × { 𝑋 } ) ∧ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ) )
31 30 simprbi ⊢ ( ⟨ ( I ↾ 𝐵 ) , ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) ⟩ = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ → ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) )
32 24 31 syl ⊢ ( 𝜑 → ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) )
33 snex ⊢ { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ∈ V
34 16 33 xpex ⊢ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ∈ V
35 34 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ∈ V )
36 32 35 ovmpt4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐶 ) ‘ 𝑝 ) ) ) 𝑧 ) = ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) )
37 19 36 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( I ↾ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) = ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) )
38 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐶 ∈ Cat )
39 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
40 4 20 22 38 39 catidcl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑦 ) )
41 1 2 3 4 5 6 7 idfudiag1bas ⊢ ( 𝜑 → 𝐵 = { 𝑋 } )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐵 = { 𝑋 } )
43 39 42 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ { 𝑋 } )
44 elsni ⊢ ( 𝑦 ∈ { 𝑋 } → 𝑦 = 𝑋 )
45 43 44 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 = 𝑋 )
46 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
47 46 42 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ { 𝑋 } )
48 elsni ⊢ ( 𝑧 ∈ { 𝑋 } → 𝑧 = 𝑋 )
49 47 48 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 = 𝑋 )
50 45 49 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 = 𝑧 )
51 50 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
52 40 51 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
53 52 ne0d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ≠ ∅ )
54 37 53 idfudiag1lem ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } )
55 mosn ⊢ ( ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) = { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } → ∃* 𝑓 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
56 54 55 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
57 8 9 56 3 isthincd ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
58 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
59 58 eqeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐵 = { 𝑥 } ↔ 𝐵 = { 𝑋 } ) )
60 5 41 59 spcedv ⊢ ( 𝜑 → ∃ 𝑥 𝐵 = { 𝑥 } )
61 4 istermc ⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 𝐵 = { 𝑥 } ) )
62 57 60 61 sylanbrc ⊢ ( 𝜑 → 𝐶 ∈ TermCat )