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