Step | Hyp | Ref
| Expression |
1 | | oppcco.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
2 | | elfvex 6131 |
. . . . . 6
⊢ (𝑋 ∈ (Base‘𝐶) → 𝐶 ∈ V) |
3 | | oppcco.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
4 | 2, 3 | eleq2s 2706 |
. . . . 5
⊢ (𝑋 ∈ 𝐵 → 𝐶 ∈ V) |
5 | | eqid 2610 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
6 | | oppcco.c |
. . . . . 6
⊢ · =
(comp‘𝐶) |
7 | | oppcco.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) |
8 | 3, 5, 6, 7 | oppcval 16196 |
. . . . 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 6107 |
. . 3
⊢ (𝜑 → (comp‘𝑂) = (comp‘((𝐶 sSet 〈(Hom ‘ndx),
tpos (Hom ‘𝐶)〉)
sSet 〈(comp‘ndx), (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)))〉))) |
11 | | ovex 6577 |
. . . 4
⊢ (𝐶 sSet 〈(Hom ‘ndx),
tpos (Hom ‘𝐶)〉)
∈ V |
12 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
13 | 3, 12 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
14 | 13, 13 | xpex 6860 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
15 | 14, 13 | mpt2ex 7136 |
. . . 4
⊢ (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢))) ∈
V |
16 | | ccoid 15900 |
. . . . 5
⊢ comp =
Slot (comp‘ndx) |
17 | 16 | setsid 15742 |
. . . 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 704 |
. . 3
⊢ (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢))) =
(comp‘((𝐶 sSet
〈(Hom ‘ndx), tpos (Hom ‘𝐶)〉) sSet 〈(comp‘ndx), (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)))〉)) |
19 | 10, 18 | syl6eqr 2662 |
. 2
⊢ (𝜑 → (comp‘𝑂) = (𝑢 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)))) |
20 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑧 = 𝑍) |
21 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑢 = 〈𝑋, 𝑌〉) |
22 | 21 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘𝑢) = (2nd
‘〈𝑋, 𝑌〉)) |
23 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑋 ∈ 𝐵) |
24 | | oppcco.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 𝑌 ∈ 𝐵) |
26 | | op2ndg 7072 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
27 | 23, 25, 26 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
28 | 22, 27 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (2nd ‘𝑢) = 𝑌) |
29 | 20, 28 | opeq12d 4348 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → 〈𝑧, (2nd ‘𝑢)〉 = 〈𝑍, 𝑌〉) |
30 | 21 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (1st ‘𝑢) = (1st
‘〈𝑋, 𝑌〉)) |
31 | | op1stg 7071 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
32 | 23, 25, 31 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
33 | 30, 32 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (1st ‘𝑢) = 𝑋) |
34 | 29, 33 | oveq12d 6567 |
. . 3
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)) = (〈𝑍, 𝑌〉 · 𝑋)) |
35 | 34 | tposeqd 7242 |
. 2
⊢ ((𝜑 ∧ (𝑢 = 〈𝑋, 𝑌〉 ∧ 𝑧 = 𝑍)) → tpos (〈𝑧, (2nd ‘𝑢)〉 · (1st
‘𝑢)) = tpos
(〈𝑍, 𝑌〉 · 𝑋)) |
36 | | opelxpi 5072 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
37 | 1, 24, 36 | syl2anc 691 |
. 2
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
38 | | oppcco.z |
. 2
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
39 | | ovex 6577 |
. . . 4
⊢
(〈𝑍, 𝑌〉 · 𝑋) ∈ V |
40 | 39 | tposex 7273 |
. . 3
⊢ tpos
(〈𝑍, 𝑌〉 · 𝑋) ∈ V |
41 | 40 | a1i 11 |
. 2
⊢ (𝜑 → tpos (〈𝑍, 𝑌〉 · 𝑋) ∈ V) |
42 | 19, 35, 37, 38, 41 | ovmpt2d 6686 |
1
⊢ (𝜑 → (〈𝑋, 𝑌〉(comp‘𝑂)𝑍) = tpos (〈𝑍, 𝑌〉 · 𝑋)) |