Theorem oppcinito

Description: Initial objects are terminal in the opposite category. (Contributed by Zhi Wang, 23-Oct-2025)

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

Proof

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