Metamath Proof Explorer

Theorem termcterm2

Description: A terminal object of the category of small categories is a terminal category. (Contributed by Zhi Wang, 18-Oct-2025)

Ref Expression
Hypotheses termcterm.e ⊢ 𝐸 = ( CatCat ‘ 𝑈 )
termcterm2. ⊢ ( 𝜑 → ( 𝑈 ∩ TermCat ) ≠ ∅ )
termcterm2.t ⊢ ( 𝜑 → 𝐶 ∈ ( TermO ‘ 𝐸 ) )
Assertion termcterm2 ( 𝜑 → 𝐶 ∈ TermCat )

Proof

Step Hyp Ref Expression
1 termcterm.e ⊢ 𝐸 = ( CatCat ‘ 𝑈 )
2 termcterm2. ⊢ ( 𝜑 → ( 𝑈 ∩ TermCat ) ≠ ∅ )
3 termcterm2.t ⊢ ( 𝜑 → 𝐶 ∈ ( TermO ‘ 𝐸 ) )
4 n0 ⊢ ( ( 𝑈 ∩ TermCat ) ≠ ∅ ↔ ∃ 𝑑 𝑑 ∈ ( 𝑈 ∩ TermCat ) )
5 2 4 sylib ⊢ ( 𝜑 → ∃ 𝑑 𝑑 ∈ ( 𝑈 ∩ TermCat ) )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ ( 𝑈 ∩ TermCat ) )
7 6 elin2d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ TermCat )
8 7 termcthind ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ ThinCat )
9 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ∈ ( TermO ‘ 𝐸 ) )
11 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
12 termorcl ⊢ ( 𝐶 ∈ ( TermO ‘ 𝐸 ) → 𝐸 ∈ Cat )
13 10 12 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐸 ∈ Cat )
14 9 11 13 istermoi ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) ∧ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) → ( 𝐶 ∈ ( Base ‘ 𝐸 ) ∧ ∀ 𝑑 ∈ ( Base ‘ 𝐸 ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) ) )
15 10 14 mpdan ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( 𝐶 ∈ ( Base ‘ 𝐸 ) ∧ ∀ 𝑑 ∈ ( Base ‘ 𝐸 ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) ) )
16 15 simpld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ∈ ( Base ‘ 𝐸 ) )
17 1 9 elbasfv ⊢ ( 𝐶 ∈ ( Base ‘ 𝐸 ) → 𝑈 ∈ V )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑈 ∈ V )
19 6 elin1d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ 𝑈 )
20 7 termccd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ Cat )
21 19 20 elind ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ ( 𝑈 ∩ Cat ) )
22 1 9 18 catcbas ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
23 21 22 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ ( Base ‘ 𝐸 ) )
24 1 18 19 7 termcterm ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ ( TermO ‘ 𝐸 ) )
25 13 10 24 termoeu1w ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ( ≃𝑐 ‘ 𝐸 ) 𝑑 )
26 1 9 18 16 23 25 thincciso4 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( 𝐶 ∈ ThinCat ↔ 𝑑 ∈ ThinCat ) )
27 8 26 mpbird ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ∈ ThinCat )
28 13 10 24 termoeu1 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) )
29 euex ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) )
30 28 29 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) )
31 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
32 eqid ⊢ ( Base ‘ 𝑑 ) = ( Base ‘ 𝑑 )
33 eqid ⊢ ( Iso ‘ 𝐸 ) = ( Iso ‘ 𝐸 )
34 1 9 31 32 18 16 23 33 catciso ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) ↔ ( 𝑓 ∈ ( ( 𝐶 Full 𝑑 ) ∩ ( 𝐶 Faith 𝑑 ) ) ∧ ( 1st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑑 ) ) ) )
35 34 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) ∧ 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) ) → ( 1st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑑 ) )
36 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
37 36 f1oen ⊢ ( ( 1st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑑 ) → ( Base ‘ 𝐶 ) ≈ ( Base ‘ 𝑑 ) )
38 35 37 syl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) ∧ 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) ) → ( Base ‘ 𝐶 ) ≈ ( Base ‘ 𝑑 ) )
39 30 38 exlimddv ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( Base ‘ 𝐶 ) ≈ ( Base ‘ 𝑑 ) )
40 32 istermc3 ⊢ ( 𝑑 ∈ TermCat ↔ ( 𝑑 ∈ ThinCat ∧ ( Base ‘ 𝑑 ) ≈ 1o ) )
41 7 40 sylib ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( 𝑑 ∈ ThinCat ∧ ( Base ‘ 𝑑 ) ≈ 1o ) )
42 41 simprd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( Base ‘ 𝑑 ) ≈ 1o )
43 entr ⊢ ( ( ( Base ‘ 𝐶 ) ≈ ( Base ‘ 𝑑 ) ∧ ( Base ‘ 𝑑 ) ≈ 1o ) → ( Base ‘ 𝐶 ) ≈ 1o )
44 39 42 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( Base ‘ 𝐶 ) ≈ 1o )
45 31 istermc3 ⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ( Base ‘ 𝐶 ) ≈ 1o ) )
46 27 44 45 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ∈ TermCat )
47 5 46 exlimddv ⊢ ( 𝜑 → 𝐶 ∈ TermCat )