Theorem oppccatf

Description: oppCat restricted to Cat is a function from Cat to Cat . (Contributed by Zhi Wang, 29-Aug-2024)

	Ref	Expression
Assertion	oppccatf	⊢ ( oppCat ↾ Cat ) : Cat ⟶ Cat

Proof

Step	Hyp	Ref	Expression
1		df-oppc	⊢ oppCat = ( 𝑓 ∈ V ↦ ( ( 𝑓 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑓 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) , 𝑧 ∈ ( Base ‘ 𝑓 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
2	1	funmpt2	⊢ Fun oppCat
3		ffvresb	⊢ ( Fun oppCat → ( ( oppCat ↾ Cat ) : Cat ⟶ Cat ↔ ∀ 𝑐 ∈ Cat ( 𝑐 ∈ dom oppCat ∧ ( oppCat ‘ 𝑐 ) ∈ Cat ) ) )
4	2 3	ax-mp	⊢ ( ( oppCat ↾ Cat ) : Cat ⟶ Cat ↔ ∀ 𝑐 ∈ Cat ( 𝑐 ∈ dom oppCat ∧ ( oppCat ‘ 𝑐 ) ∈ Cat ) )
5		elex	⊢ ( 𝑐 ∈ Cat → 𝑐 ∈ V )
6		ovex	⊢ ( ( 𝑓 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑓 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) , 𝑧 ∈ ( Base ‘ 𝑓 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) ∈ V
7	6 1	dmmpti	⊢ dom oppCat = V
8	5 7	eleqtrrdi	⊢ ( 𝑐 ∈ Cat → 𝑐 ∈ dom oppCat )
9		eqid	⊢ ( oppCat ‘ 𝑐 ) = ( oppCat ‘ 𝑐 )
10	9	oppccat	⊢ ( 𝑐 ∈ Cat → ( oppCat ‘ 𝑐 ) ∈ Cat )
11	8 10	jca	⊢ ( 𝑐 ∈ Cat → ( 𝑐 ∈ dom oppCat ∧ ( oppCat ‘ 𝑐 ) ∈ Cat ) )
12	4 11	mprgbir	⊢ ( oppCat ↾ Cat ) : Cat ⟶ Cat