Metamath Proof Explorer

Theorem oppccomfpropd

Description: If two categories have the same hom-sets and composition, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses oppchomfpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
oppccomfpropd.1 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
Assertion oppccomfpropd ( 𝜑 → ( compf ‘ ( oppCat ‘ 𝐶 ) ) = ( compf ‘ ( oppCat ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 oppchomfpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2 oppccomfpropd.1 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
4 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
5 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
6 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
7 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
8 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
9 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
10 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
11 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
12 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) )
13 eqid ⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
14 4 13 oppchom ⊢ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑦 )
15 12 14 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑦 ) )
16 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) )
17 4 13 oppchom ⊢ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 )
18 16 17 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
19 3 4 5 6 7 8 9 10 11 15 18 comfeqval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑔 ) )
20 3 5 13 11 10 9 oppcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) )
21 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
22 eqid ⊢ ( oppCat ‘ 𝐷 ) = ( oppCat ‘ 𝐷 )
23 1 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
25 11 24 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐷 ) )
26 10 24 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
27 9 24 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
28 21 6 22 25 26 27 oppcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐷 ) ) 𝑧 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑥 ) 𝑔 ) )
29 19 20 28 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐷 ) ) 𝑧 ) 𝑓 ) )
30 29 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐷 ) ) 𝑧 ) 𝑓 ) )
31 30 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐷 ) ) 𝑧 ) 𝑓 ) )
32 eqid ⊢ ( comp ‘ ( oppCat ‘ 𝐶 ) ) = ( comp ‘ ( oppCat ‘ 𝐶 ) )
33 eqid ⊢ ( comp ‘ ( oppCat ‘ 𝐷 ) ) = ( comp ‘ ( oppCat ‘ 𝐷 ) )
34 eqid ⊢ ( Hom ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom ‘ ( oppCat ‘ 𝐶 ) )
35 13 3 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( oppCat ‘ 𝐶 ) )
36 35 a1i ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ ( oppCat ‘ 𝐶 ) ) )
37 22 21 oppcbas ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ ( oppCat ‘ 𝐷 ) )
38 23 37 eqtrdi ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ ( oppCat ‘ 𝐷 ) ) )
39 1 oppchomfpropd ⊢ ( 𝜑 → ( Homf ‘ ( oppCat ‘ 𝐶 ) ) = ( Homf ‘ ( oppCat ‘ 𝐷 ) ) )
40 32 33 34 36 38 39 comfeq ⊢ ( 𝜑 → ( ( compf ‘ ( oppCat ‘ 𝐶 ) ) = ( compf ‘ ( oppCat ‘ 𝐷 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ 𝐷 ) ) 𝑧 ) 𝑓 ) ) )
41 31 40 mpbird ⊢ ( 𝜑 → ( compf ‘ ( oppCat ‘ 𝐶 ) ) = ( compf ‘ ( oppCat ‘ 𝐷 ) ) )