Theorem oppctermo

Description: Terminal objects are initial in the opposite category. Comments before Definition 7.4 in Adamek p. 102. (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Assertion	oppctermo	⊢ ( 𝐼 ∈ ( TermO ‘ 𝐶 ) ↔ 𝐼 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		termorcl	⊢ ( 𝐼 ∈ ( TermO ‘ 𝐶 ) → 𝐶 ∈ Cat )
2		initorcl	⊢ ( 𝐼 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) → ( oppCat ‘ 𝐶 ) ∈ Cat )
3		eqid	⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5	3 4	oppcbas	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( oppCat ‘ 𝐶 ) )
6	5	initoo2	⊢ ( 𝐼 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) → 𝐼 ∈ ( Base ‘ 𝐶 ) )
7		elfvex	⊢ ( 𝐼 ∈ ( Base ‘ 𝐶 ) → 𝐶 ∈ V )
8		id	⊢ ( 𝐶 ∈ V → 𝐶 ∈ V )
9	3 8	oppccatb	⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ Cat ↔ ( oppCat ‘ 𝐶 ) ∈ Cat ) )
10	6 7 9	3syl	⊢ ( 𝐼 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) → ( 𝐶 ∈ Cat ↔ ( oppCat ‘ 𝐶 ) ∈ Cat ) )
11	2 10	mpbird	⊢ ( 𝐼 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
12		2fveq3	⊢ ( 𝑐 = 𝐶 → ( InitO ‘ ( oppCat ‘ 𝑐 ) ) = ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )
13		dftermo2	⊢ TermO = ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) )
14		fvex	⊢ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) ∈ V
15	12 13 14	fvmpt	⊢ ( 𝐶 ∈ Cat → ( TermO ‘ 𝐶 ) = ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )
16	15	eleq2d	⊢ ( 𝐶 ∈ Cat → ( 𝐼 ∈ ( TermO ‘ 𝐶 ) ↔ 𝐼 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) ) )
17	1 11 16	pm5.21nii	⊢ ( 𝐼 ∈ ( TermO ‘ 𝐶 ) ↔ 𝐼 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )