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) (Proof shortened by Zhi Wang, 23-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 9 termoo2 ⊢ ( 𝐶 ∈ ( TermO ‘ 𝐸 ) → 𝐶 ∈ ( Base ‘ 𝐸 ) )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ∈ ( Base ‘ 𝐸 ) )
13 1 9 elbasfv ⊢ ( 𝐶 ∈ ( Base ‘ 𝐸 ) → 𝑈 ∈ V )
14 12 13 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑈 ∈ V )
15 6 elin1d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ 𝑈 )
16 7 termccd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ Cat )
17 15 16 elind ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ ( 𝑈 ∩ Cat ) )
18 1 9 14 catcbas ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
19 17 18 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ ( Base ‘ 𝐸 ) )
20 termorcl ⊢ ( 𝐶 ∈ ( TermO ‘ 𝐸 ) → 𝐸 ∈ Cat )
21 10 20 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐸 ∈ Cat )
22 1 14 15 7 termcterm ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝑑 ∈ ( TermO ‘ 𝐸 ) )
23 21 10 22 termoeu1w ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ( ≃𝑐 ‘ 𝐸 ) 𝑑 )
24 1 9 14 12 19 23 thincciso4 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( 𝐶 ∈ ThinCat ↔ 𝑑 ∈ ThinCat ) )
25 8 24 mpbird ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ∈ ThinCat )
26 21 10 22 termoeu1 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ∃! 𝑓 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) )
27 euex ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) )
29 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
30 eqid ⊢ ( Base ‘ 𝑑 ) = ( Base ‘ 𝑑 )
31 eqid ⊢ ( Iso ‘ 𝐸 ) = ( Iso ‘ 𝐸 )
32 1 9 29 30 14 12 19 31 catciso ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) ↔ ( 𝑓 ∈ ( ( 𝐶 Full 𝑑 ) ∩ ( 𝐶 Faith 𝑑 ) ) ∧ ( 1st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑑 ) ) ) )
33 32 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) ∧ 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) ) → ( 1st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑑 ) )
34 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
35 34 f1oen ⊢ ( ( 1st ‘ 𝑓 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑑 ) → ( Base ‘ 𝐶 ) ≈ ( Base ‘ 𝑑 ) )
36 33 35 syl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) ∧ 𝑓 ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑑 ) ) → ( Base ‘ 𝐶 ) ≈ ( Base ‘ 𝑑 ) )
37 28 36 exlimddv ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( Base ‘ 𝐶 ) ≈ ( Base ‘ 𝑑 ) )
38 30 istermc3 ⊢ ( 𝑑 ∈ TermCat ↔ ( 𝑑 ∈ ThinCat ∧ ( Base ‘ 𝑑 ) ≈ 1o ) )
39 7 38 sylib ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( 𝑑 ∈ ThinCat ∧ ( Base ‘ 𝑑 ) ≈ 1o ) )
40 39 simprd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( Base ‘ 𝑑 ) ≈ 1o )
41 entr ⊢ ( ( ( Base ‘ 𝐶 ) ≈ ( Base ‘ 𝑑 ) ∧ ( Base ‘ 𝑑 ) ≈ 1o ) → ( Base ‘ 𝐶 ) ≈ 1o )
42 37 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → ( Base ‘ 𝐶 ) ≈ 1o )
43 29 istermc3 ⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ( Base ‘ 𝐶 ) ≈ 1o ) )
44 25 42 43 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 𝑈 ∩ TermCat ) ) → 𝐶 ∈ TermCat )
45 5 44 exlimddv ⊢ ( 𝜑 → 𝐶 ∈ TermCat )