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 ‘ 𝐷 ) ) )