Metamath Proof Explorer

Theorem 2oppccomf

Description: The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion 2oppccomf ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3 1 2 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
4 eqid ⊢ ( comp ‘ 𝑂 ) = ( comp ‘ 𝑂 )
5 eqid ⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
6 simpr1 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
7 simpr2 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
8 simpr3 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
9 3 4 5 6 7 8 oppcco ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝑂 ) ) 𝑧 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑥 ) 𝑔 ) )
10 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11 2 10 1 8 7 6 oppcco ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑥 ) 𝑔 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
12 9 11 eqtr2d ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝑂 ) ) 𝑧 ) 𝑓 ) )
13 12 ralrimivw ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝑂 ) ) 𝑧 ) 𝑓 ) )
14 13 ralrimivw ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝑂 ) ) 𝑧 ) 𝑓 ) )
15 14 ralrimivvva ⊢ ( ⊤ → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝑂 ) ) 𝑧 ) 𝑓 ) )
16 eqid ⊢ ( comp ‘ ( oppCat ‘ 𝑂 ) ) = ( comp ‘ ( oppCat ‘ 𝑂 ) )
17 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
18 eqidd ⊢ ( ⊤ → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) )
19 1 2 2oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( oppCat ‘ 𝑂 ) )
20 19 a1i ⊢ ( ⊤ → ( Base ‘ 𝐶 ) = ( Base ‘ ( oppCat ‘ 𝑂 ) ) )
21 1 2oppchomf ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
22 21 a1i ⊢ ( ⊤ → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
23 10 16 17 18 20 22 comfeq ⊢ ( ⊤ → ( ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝑂 ) ) 𝑧 ) 𝑓 ) ) )
24 15 23 mpbird ⊢ ( ⊤ → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
25 24 mptru ⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )