Step |
Hyp |
Ref |
Expression |
1 |
|
oppcco.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
2 |
|
oppcco.c |
⊢ · = ( comp ‘ 𝐶 ) |
3 |
|
oppcco.o |
⊢ 𝑂 = ( oppCat ‘ 𝐶 ) |
4 |
|
oppcco.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
5 |
|
oppcco.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
6 |
|
oppcco.z |
⊢ ( 𝜑 → 𝑍 ∈ 𝐵 ) |
7 |
|
elfvex |
⊢ ( 𝑋 ∈ ( Base ‘ 𝐶 ) → 𝐶 ∈ V ) |
8 |
7 1
|
eleq2s |
⊢ ( 𝑋 ∈ 𝐵 → 𝐶 ∈ V ) |
9 |
|
eqid |
⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) |
10 |
1 9 2 3
|
oppcval |
⊢ ( 𝐶 ∈ V → 𝑂 = ( ( 𝐶 sSet 〈 ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) 〉 ) sSet 〈 ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) 〉 ) ) |
11 |
4 8 10
|
3syl |
⊢ ( 𝜑 → 𝑂 = ( ( 𝐶 sSet 〈 ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) 〉 ) sSet 〈 ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) 〉 ) ) |
12 |
11
|
fveq2d |
⊢ ( 𝜑 → ( comp ‘ 𝑂 ) = ( comp ‘ ( ( 𝐶 sSet 〈 ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) 〉 ) sSet 〈 ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) 〉 ) ) ) |
13 |
|
ovex |
⊢ ( 𝐶 sSet 〈 ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) 〉 ) ∈ V |
14 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
15 |
14 14
|
xpex |
⊢ ( 𝐵 × 𝐵 ) ∈ V |
16 |
15 14
|
mpoex |
⊢ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) ∈ V |
17 |
|
ccoid |
⊢ comp = Slot ( comp ‘ ndx ) |
18 |
17
|
setsid |
⊢ ( ( ( 𝐶 sSet 〈 ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) 〉 ) ∈ V ∧ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) ∈ V ) → ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) = ( comp ‘ ( ( 𝐶 sSet 〈 ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) 〉 ) sSet 〈 ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) 〉 ) ) ) |
19 |
13 16 18
|
mp2an |
⊢ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) = ( comp ‘ ( ( 𝐶 sSet 〈 ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) 〉 ) sSet 〈 ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) 〉 ) ) |
20 |
12 19
|
eqtr4di |
⊢ ( 𝜑 → ( comp ‘ 𝑂 ) = ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) ) ) |
21 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 ) |
22 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → 𝑢 = 〈 𝑋 , 𝑌 〉 ) |
23 |
22
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑢 ) = ( 2nd ‘ 〈 𝑋 , 𝑌 〉 ) ) |
24 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → 𝑌 ∈ 𝐵 ) |
25 |
|
op2ndg |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 2nd ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑌 ) |
26 |
4 24 25
|
syl2an2r |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑌 ) |
27 |
23 26
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑢 ) = 𝑌 ) |
28 |
21 27
|
opeq12d |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 = 〈 𝑍 , 𝑌 〉 ) |
29 |
22
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑢 ) = ( 1st ‘ 〈 𝑋 , 𝑌 〉 ) ) |
30 |
|
op1stg |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1st ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑋 ) |
31 |
4 24 30
|
syl2an2r |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑋 ) |
32 |
29 31
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑢 ) = 𝑋 ) |
33 |
28 32
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) = ( 〈 𝑍 , 𝑌 〉 · 𝑋 ) ) |
34 |
33
|
tposeqd |
⊢ ( ( 𝜑 ∧ ( 𝑢 = 〈 𝑋 , 𝑌 〉 ∧ 𝑧 = 𝑍 ) ) → tpos ( 〈 𝑧 , ( 2nd ‘ 𝑢 ) 〉 · ( 1st ‘ 𝑢 ) ) = tpos ( 〈 𝑍 , 𝑌 〉 · 𝑋 ) ) |
35 |
4 5
|
opelxpd |
⊢ ( 𝜑 → 〈 𝑋 , 𝑌 〉 ∈ ( 𝐵 × 𝐵 ) ) |
36 |
|
ovex |
⊢ ( 〈 𝑍 , 𝑌 〉 · 𝑋 ) ∈ V |
37 |
36
|
tposex |
⊢ tpos ( 〈 𝑍 , 𝑌 〉 · 𝑋 ) ∈ V |
38 |
37
|
a1i |
⊢ ( 𝜑 → tpos ( 〈 𝑍 , 𝑌 〉 · 𝑋 ) ∈ V ) |
39 |
20 34 35 6 38
|
ovmpod |
⊢ ( 𝜑 → ( 〈 𝑋 , 𝑌 〉 ( comp ‘ 𝑂 ) 𝑍 ) = tpos ( 〈 𝑍 , 𝑌 〉 · 𝑋 ) ) |