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

Metamath Proof Explorer

Theorem oppcthin

Description: The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Hypothesis oppcthin.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion oppcthin ( 𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat )

Proof

Step Hyp Ref Expression
1 oppcthin.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3 1 2 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
4 3 a1i ⊢ ( 𝐶 ∈ ThinCat → ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 ) )
5 eqidd ⊢ ( 𝐶 ∈ ThinCat → ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 ) )
6 simpl ⊢ ( ( 𝐶 ∈ ThinCat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ ThinCat )
7 simprr ⊢ ( ( 𝐶 ∈ ThinCat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
8 simprl ⊢ ( ( 𝐶 ∈ ThinCat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
9 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10 6 7 8 2 9 thincmo ⊢ ( ( 𝐶 ∈ ThinCat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
11 9 1 oppchom ⊢ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 )
12 11 eleq2i ⊢ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ↔ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
13 12 mobii ⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
14 10 13 sylibr ⊢ ( ( 𝐶 ∈ ThinCat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) )
15 thincc ⊢ ( 𝐶 ∈ ThinCat → 𝐶 ∈ Cat )
16 1 oppccat ⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
17 15 16 syl ⊢ ( 𝐶 ∈ ThinCat → 𝑂 ∈ Cat )
18 4 5 14 17 isthincd ⊢ ( 𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat )