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

Metamath Proof Explorer

Theorem fucoppccic

Description: The opposite category of functors is isomorphic to the category of opposite functors. (Contributed by Zhi Wang, 18-Nov-2025)

Ref Expression
Hypotheses fucoppccic.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
fucoppccic.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
fucoppccic.x ⊢ 𝑋 = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
fucoppccic.y ⊢ 𝑌 = ( ( oppCat ‘ 𝐷 ) FuncCat ( oppCat ‘ 𝐸 ) )
fucoppccic.xb ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
fucoppccic.yb ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
fucoppccic.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
fucoppccic.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
Assertion fucoppccic ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )

Proof

Step Hyp Ref Expression
1 fucoppccic.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 fucoppccic.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 fucoppccic.x ⊢ 𝑋 = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
4 fucoppccic.y ⊢ 𝑌 = ( ( oppCat ‘ 𝐷 ) FuncCat ( oppCat ‘ 𝐸 ) )
5 fucoppccic.xb ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 fucoppccic.yb ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 fucoppccic.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
8 fucoppccic.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
9 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
10 1 2 elbasfv ⊢ ( 𝑋 ∈ 𝐵 → 𝑈 ∈ V )
11 1 catccat ⊢ ( 𝑈 ∈ V → 𝐶 ∈ Cat )
12 5 10 11 3syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
13 eqid ⊢ ( oppCat ‘ 𝐷 ) = ( oppCat ‘ 𝐷 )
14 eqid ⊢ ( oppCat ‘ 𝐸 ) = ( oppCat ‘ 𝐸 )
15 eqid ⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
16 eqid ⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
17 eqidd ⊢ ( 𝜑 → ( oppFunc ↾ ( 𝐷 Func 𝐸 ) ) = ( oppFunc ↾ ( 𝐷 Func 𝐸 ) ) )
18 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐸 ) 𝑓 ) ) ) = ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐸 ) 𝑓 ) ) ) )
19 13 14 15 3 4 16 17 18 1 2 9 7 8 5 6 fucoppc ⊢ ( 𝜑 → ( oppFunc ↾ ( 𝐷 Func 𝐸 ) ) ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐸 ) 𝑓 ) ) ) )
20 df-br ⊢ ( ( oppFunc ↾ ( 𝐷 Func 𝐸 ) ) ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐸 ) 𝑓 ) ) ) ↔ ⟨ ( oppFunc ↾ ( 𝐷 Func 𝐸 ) ) , ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐸 ) 𝑓 ) ) ) ⟩ ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
21 19 20 sylib ⊢ ( 𝜑 → ⟨ ( oppFunc ↾ ( 𝐷 Func 𝐸 ) ) , ( 𝑓 ∈ ( 𝐷 Func 𝐸 ) , 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( I ↾ ( 𝑔 ( 𝐷 Nat 𝐸 ) 𝑓 ) ) ) ⟩ ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
22 9 2 12 5 6 21 brcici ⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )