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 ↔ 𝑋 ( ≃_𝑐 ‘ 𝐶 ) 𝑌 ) )

Metamath Proof Explorer

Theorem termcciso

Proof