This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐶 ) ) )