Metamath Proof Explorer

Theorem termcciso

Description: A category is isomorphic to a terminal category iff it itself is terminal. (Contributed by Zhi Wang, 26-Oct-2025)

Ref Expression
Hypotheses termcciso.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
termcciso.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
termcciso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
termcciso.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
termcciso.t ⊢ ( 𝜑 → 𝑋 ∈ TermCat )
Assertion termcciso ( 𝜑 → ( 𝑌 ∈ TermCat ↔ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 termcciso.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 termcciso.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 termcciso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 termcciso.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 termcciso.t ⊢ ( 𝜑 → 𝑋 ∈ TermCat )
6 1 2 elbasfv ⊢ ( 𝑋 ∈ 𝐵 → 𝑈 ∈ V )
7 3 6 syl ⊢ ( 𝜑 → 𝑈 ∈ V )
8 1 catccat ⊢ ( 𝑈 ∈ V → 𝐶 ∈ Cat )
9 7 8 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝐶 ∈ Cat )
11 1 2 7 catcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
12 3 11 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
13 12 elin1d ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
14 1 7 13 5 termcterm ⊢ ( 𝜑 → 𝑋 ∈ ( TermO ‘ 𝐶 ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝑋 ∈ ( TermO ‘ 𝐶 ) )
16 7 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝑈 ∈ V )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝑌 ∈ 𝐵 )
18 11 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝐵 = ( 𝑈 ∩ Cat ) )
19 17 18 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝑌 ∈ ( 𝑈 ∩ Cat ) )
20 19 elin1d ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝑌 ∈ 𝑈 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝑌 ∈ TermCat )
22 1 16 20 21 termcterm ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝑌 ∈ ( TermO ‘ 𝐶 ) )
23 10 15 22 termoeu1w ⊢ ( ( 𝜑 ∧ 𝑌 ∈ TermCat ) → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )
24 13 5 elind ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ TermCat ) )
25 24 ne0d ⊢ ( 𝜑 → ( 𝑈 ∩ TermCat ) ≠ ∅ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) → ( 𝑈 ∩ TermCat ) ≠ ∅ )
27 9 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) → 𝐶 ∈ Cat )
28 14 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) → 𝑋 ∈ ( TermO ‘ 𝐶 ) )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )
30 27 28 29 termoeu2 ⊢ ( ( 𝜑 ∧ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) → 𝑌 ∈ ( TermO ‘ 𝐶 ) )
31 1 26 30 termcterm2 ⊢ ( ( 𝜑 ∧ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) → 𝑌 ∈ TermCat )
32 23 31 impbida ⊢ ( 𝜑 → ( 𝑌 ∈ TermCat ↔ 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ) )