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		thinccat	⊢ ( 𝐶 ∈ ThinCat → 𝐶 ∈ Cat )
16	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
17	15 16	syl	⊢ ( 𝐶 ∈ ThinCat → 𝑂 ∈ Cat )
18	4 5 14 17	isthincd	⊢ ( 𝐶 ∈ ThinCat → 𝑂 ∈ ThinCat )