Step | Hyp | Ref
| Expression |
1 | | oppcco.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
2 | | elfvex 6221 |
. . . . . 6
⊢ (𝑋 ∈ (Base‘𝐶) → 𝐶 ∈ V) |
3 | | oppcco.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
4 | 2, 3 | eleq2s 2719 |
. . . . 5
⊢ (𝑋 ∈ 𝐵 → 𝐶 ∈ V) |
5 | | eqid 2622 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
6 | | oppcco.c |
. . . . . 6
⊢ · =
(comp‘𝐶) |
7 | | oppcco.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) |
8 | 3, 5, 6, 7 | oppcval 16373 |
. . . . 5
⊢ (𝐶 ∈ V → 𝑂 = ((𝐶 sSet 〈(Hom ‘ndx), tpos (Hom
‘𝐶)〉) sSet
〈(comp‘ndx), (𝑢
∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)))〉)) |
9 | 1, 4, 8 | 3syl 18 |
. . . 4
⊢ (𝜑 → 𝑂 = ((𝐶 sSet 〈(Hom ‘ndx), tpos (Hom
‘𝐶)〉) sSet
〈(comp‘ndx), (𝑢
∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)))〉)) |
10 | 9 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (comp‘𝑂) = (comp‘((𝐶 sSet 〈(Hom ‘ndx),
tpos (Hom ‘𝐶)〉)
sSet 〈(comp‘ndx), (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)))〉))) |
11 | | ovex 6678 |
. . . 4
⊢ (𝐶 sSet 〈(Hom ‘ndx),
tpos (Hom ‘𝐶)〉)
∈ V |
12 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
13 | 3, 12 | eqeltri 2697 |
. . . . . 6
⊢ 𝐵 ∈ V |
14 | 13, 13 | xpex 6962 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
15 | 14, 13 | mpt2ex 7247 |
. . . 4
⊢ (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢))) ∈
V |
16 | | ccoid 16077 |
. . . . 5
⊢ comp =
Slot (comp‘ndx) |
17 | 16 | setsid 15914 |
. . . 4
⊢ (((𝐶 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
‘𝑢)))〉))) |
18 | 11, 15, 17 | mp2an 708 |
. . 3
⊢ (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢))) =
(comp‘((𝐶 sSet
〈(Hom ‘ndx), tpos (Hom ‘𝐶)〉) sSet 〈(comp‘ndx), (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)))〉)) |
19 | 10, 18 | syl6eqr 2674 |
. 2
⊢ (𝜑 → (comp‘𝑂) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)))) |
20 | | simprr 796 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑧 = 𝑍) |
21 | | simprl 794 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑢 = 〈𝑋, 𝑌〉) |
22 | 21 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘𝑢) = (2nd
‘〈𝑋, 𝑌〉)) |
23 | 1 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑋 ∈ 𝐵) |
24 | | oppcco.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
25 | 24 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑌 ∈ 𝐵) |
26 | | op2ndg 7181 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
27 | 23, 25, 26 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
28 | 22, 27 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘𝑢) = 𝑌) |
29 | 20, 28 | opeq12d 4410 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 〈𝑧, (2nd ‘𝑢)〉 = 〈𝑍, 𝑌〉) |
30 | 21 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (1st ‘𝑢) = (1st
‘〈𝑋, 𝑌〉)) |
31 | | op1stg 7180 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
32 | 23, 25, 31 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
33 | 30, 32 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (1st ‘𝑢) = 𝑋) |
34 | 29, 33 | oveq12d 6668 |
. . 3
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)) = (〈𝑍, 𝑌〉 · 𝑋)) |
35 | 34 | tposeqd 7355 |
. 2
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)) = tpos
(〈𝑍, 𝑌〉 · 𝑋)) |
36 | | opelxpi 5148 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
37 | 1, 24, 36 | syl2anc 693 |
. 2
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
38 | | oppcco.z |
. 2
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
39 | | ovex 6678 |
. . . 4
⊢
(〈𝑍, 𝑌〉 · 𝑋) ∈ V |
40 | 39 | tposex 7386 |
. . 3
⊢ tpos
(〈𝑍, 𝑌〉 · 𝑋) ∈ V |
41 | 40 | a1i 11 |
. 2
⊢ (𝜑 → tpos (〈𝑍, 𝑌〉 · 𝑋) ∈ V) |
42 | 19, 35, 37, 38, 41 | ovmpt2d 6788 |
1
⊢ (𝜑 → (〈𝑋, 𝑌〉(comp‘𝑂)𝑍) = tpos (〈𝑍, 𝑌〉 · 𝑋)) |