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

Metamath Proof Explorer

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