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	$$⊢C=\mathrm{CatCat}\left(U\right)$$
	termcciso.b	$$⊢B={\mathrm{Base}}_C$$
	termcciso.x	$$⊢\phi \to X\in B$$
	termcciso.y	$$⊢\phi \to Y\in B$$
	termcciso.t	No typesetting found for |- ( ph -> X e. TermCat ) with typecode |-
Assertion	termcciso	Could not format assertion : No typesetting found for |- ( ph -> ( Y e. TermCat <-> X ( ~=c ` C ) Y ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		termcciso.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		termcciso.b	$$⊢B={\mathrm{Base}}_C$$
3		termcciso.x	$$⊢\phi \to X\in B$$
4		termcciso.y	$$⊢\phi \to Y\in B$$
5		termcciso.t	Could not format ( ph -> X e. TermCat ) : No typesetting found for |- ( ph -> X e. TermCat ) with typecode |-
6	1 2	elbasfv	$$⊢X\in B\to U\in \mathrm{V}$$
7	3 6	syl	$$⊢\phi \to U\in \mathrm{V}$$
8	1	catccat	$$⊢U\in \mathrm{V}\to C\in \mathrm{Cat}$$
9	7 8	syl	$$⊢\phi \to C\in \mathrm{Cat}$$
10	9	adantr	Could not format ( ( ph /\ Y e. TermCat ) -> C e. Cat ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> C e. Cat ) with typecode |-
11	1 2 7	catcbas	$$⊢\phi \to B=U\cap \mathrm{Cat}$$
12	3 11	eleqtrd	$$⊢\phi \to X\in \left(U\cap \mathrm{Cat}\right)$$
13	12	elin1d	$$⊢\phi \to X\in U$$
14	1 7 13 5	termcterm	$$⊢\phi \to X\in \mathrm{TermO}\left(C\right)$$
15	14	adantr	Could not format ( ( ph /\ Y e. TermCat ) -> X e. ( TermO ` C ) ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> X e. ( TermO ` C ) ) with typecode |-
16	7	adantr	Could not format ( ( ph /\ Y e. TermCat ) -> U e. _V ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> U e. _V ) with typecode |-
17	4	adantr	Could not format ( ( ph /\ Y e. TermCat ) -> Y e. B ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> Y e. B ) with typecode |-
18	11	adantr	Could not format ( ( ph /\ Y e. TermCat ) -> B = ( U i^i Cat ) ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> B = ( U i^i Cat ) ) with typecode |-
19	17 18	eleqtrd	Could not format ( ( ph /\ Y e. TermCat ) -> Y e. ( U i^i Cat ) ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> Y e. ( U i^i Cat ) ) with typecode |-
20	19	elin1d	Could not format ( ( ph /\ Y e. TermCat ) -> Y e. U ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> Y e. U ) with typecode |-
21		simpr	Could not format ( ( ph /\ Y e. TermCat ) -> Y e. TermCat ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> Y e. TermCat ) with typecode |-
22	1 16 20 21	termcterm	Could not format ( ( ph /\ Y e. TermCat ) -> Y e. ( TermO ` C ) ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> Y e. ( TermO ` C ) ) with typecode |-
23	10 15 22	termoeu1w	Could not format ( ( ph /\ Y e. TermCat ) -> X ( ~=c ` C ) Y ) : No typesetting found for |- ( ( ph /\ Y e. TermCat ) -> X ( ~=c ` C ) Y ) with typecode |-
24	13 5	elind	Could not format ( ph -> X e. ( U i^i TermCat ) ) : No typesetting found for |- ( ph -> X e. ( U i^i TermCat ) ) with typecode |-
25	24	ne0d	Could not format ( ph -> ( U i^i TermCat ) =/= (/) ) : No typesetting found for |- ( ph -> ( U i^i TermCat ) =/= (/) ) with typecode |-
26	25	adantr	Could not format ( ( ph /\ X ( ~=c ` C ) Y ) -> ( U i^i TermCat ) =/= (/) ) : No typesetting found for |- ( ( ph /\ X ( ~=c ` C ) Y ) -> ( U i^i TermCat ) =/= (/) ) with typecode |-
27	9	adantr	$$⊢\left(\phi \wedge X{\simeq }_{𝑐}\left(C\right)Y\right)\to C\in \mathrm{Cat}$$
28	14	adantr	$$⊢\left(\phi \wedge X{\simeq }_{𝑐}\left(C\right)Y\right)\to X\in \mathrm{TermO}\left(C\right)$$
29		simpr	$$⊢\left(\phi \wedge X{\simeq }_{𝑐}\left(C\right)Y\right)\to X{\simeq }_{𝑐}\left(C\right)Y$$
30	27 28 29	termoeu2	$$⊢\left(\phi \wedge X{\simeq }_{𝑐}\left(C\right)Y\right)\to Y\in \mathrm{TermO}\left(C\right)$$
31	1 26 30	termcterm2	Could not format ( ( ph /\ X ( ~=c ` C ) Y ) -> Y e. TermCat ) : No typesetting found for |- ( ( ph /\ X ( ~=c ` C ) Y ) -> Y e. TermCat ) with typecode |-
32	23 31	impbida	Could not format ( ph -> ( Y e. TermCat <-> X ( ~=c ` C ) Y ) ) : No typesetting found for |- ( ph -> ( Y e. TermCat <-> X ( ~=c ` C ) Y ) ) with typecode |-