Detailed syntax breakdown of Definition df-xpc
| Step | Hyp | Ref
| Expression |
| 1 | | cxpc 18213 |
. 2
class
×c |
| 2 | | vr |
. . 3
setvar 𝑟 |
| 3 | | vs |
. . 3
setvar 𝑠 |
| 4 | | cvv 3480 |
. . 3
class
V |
| 5 | | vb |
. . . 4
setvar 𝑏 |
| 6 | 2 | cv 1539 |
. . . . . 6
class 𝑟 |
| 7 | | cbs 17247 |
. . . . . 6
class
Base |
| 8 | 6, 7 | cfv 6561 |
. . . . 5
class
(Base‘𝑟) |
| 9 | 3 | cv 1539 |
. . . . . 6
class 𝑠 |
| 10 | 9, 7 | cfv 6561 |
. . . . 5
class
(Base‘𝑠) |
| 11 | 8, 10 | cxp 5683 |
. . . 4
class
((Base‘𝑟)
× (Base‘𝑠)) |
| 12 | | vh |
. . . . 5
setvar ℎ |
| 13 | | vu |
. . . . . 6
setvar 𝑢 |
| 14 | | vv |
. . . . . 6
setvar 𝑣 |
| 15 | 5 | cv 1539 |
. . . . . 6
class 𝑏 |
| 16 | 13 | cv 1539 |
. . . . . . . . 9
class 𝑢 |
| 17 | | c1st 8012 |
. . . . . . . . 9
class
1st |
| 18 | 16, 17 | cfv 6561 |
. . . . . . . 8
class
(1st ‘𝑢) |
| 19 | 14 | cv 1539 |
. . . . . . . . 9
class 𝑣 |
| 20 | 19, 17 | cfv 6561 |
. . . . . . . 8
class
(1st ‘𝑣) |
| 21 | | chom 17308 |
. . . . . . . . 9
class
Hom |
| 22 | 6, 21 | cfv 6561 |
. . . . . . . 8
class (Hom
‘𝑟) |
| 23 | 18, 20, 22 | co 7431 |
. . . . . . 7
class
((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) |
| 24 | | c2nd 8013 |
. . . . . . . . 9
class
2nd |
| 25 | 16, 24 | cfv 6561 |
. . . . . . . 8
class
(2nd ‘𝑢) |
| 26 | 19, 24 | cfv 6561 |
. . . . . . . 8
class
(2nd ‘𝑣) |
| 27 | 9, 21 | cfv 6561 |
. . . . . . . 8
class (Hom
‘𝑠) |
| 28 | 25, 26, 27 | co 7431 |
. . . . . . 7
class
((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)) |
| 29 | 23, 28 | cxp 5683 |
. . . . . 6
class
(((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣))) |
| 30 | 13, 14, 15, 15, 29 | cmpo 7433 |
. . . . 5
class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) |
| 31 | | cnx 17230 |
. . . . . . . 8
class
ndx |
| 32 | 31, 7 | cfv 6561 |
. . . . . . 7
class
(Base‘ndx) |
| 33 | 32, 15 | cop 4632 |
. . . . . 6
class
〈(Base‘ndx), 𝑏〉 |
| 34 | 31, 21 | cfv 6561 |
. . . . . . 7
class (Hom
‘ndx) |
| 35 | 12 | cv 1539 |
. . . . . . 7
class ℎ |
| 36 | 34, 35 | cop 4632 |
. . . . . 6
class
〈(Hom ‘ndx), ℎ〉 |
| 37 | | cco 17309 |
. . . . . . . 8
class
comp |
| 38 | 31, 37 | cfv 6561 |
. . . . . . 7
class
(comp‘ndx) |
| 39 | | vx |
. . . . . . . 8
setvar 𝑥 |
| 40 | | vy |
. . . . . . . 8
setvar 𝑦 |
| 41 | 15, 15 | cxp 5683 |
. . . . . . . 8
class (𝑏 × 𝑏) |
| 42 | | vg |
. . . . . . . . 9
setvar 𝑔 |
| 43 | | vf |
. . . . . . . . 9
setvar 𝑓 |
| 44 | 39 | cv 1539 |
. . . . . . . . . . 11
class 𝑥 |
| 45 | 44, 24 | cfv 6561 |
. . . . . . . . . 10
class
(2nd ‘𝑥) |
| 46 | 40 | cv 1539 |
. . . . . . . . . 10
class 𝑦 |
| 47 | 45, 46, 35 | co 7431 |
. . . . . . . . 9
class
((2nd ‘𝑥)ℎ𝑦) |
| 48 | 44, 35 | cfv 6561 |
. . . . . . . . 9
class (ℎ‘𝑥) |
| 49 | 42 | cv 1539 |
. . . . . . . . . . . 12
class 𝑔 |
| 50 | 49, 17 | cfv 6561 |
. . . . . . . . . . 11
class
(1st ‘𝑔) |
| 51 | 43 | cv 1539 |
. . . . . . . . . . . 12
class 𝑓 |
| 52 | 51, 17 | cfv 6561 |
. . . . . . . . . . 11
class
(1st ‘𝑓) |
| 53 | 44, 17 | cfv 6561 |
. . . . . . . . . . . . . 14
class
(1st ‘𝑥) |
| 54 | 53, 17 | cfv 6561 |
. . . . . . . . . . . . 13
class
(1st ‘(1st ‘𝑥)) |
| 55 | 45, 17 | cfv 6561 |
. . . . . . . . . . . . 13
class
(1st ‘(2nd ‘𝑥)) |
| 56 | 54, 55 | cop 4632 |
. . . . . . . . . . . 12
class
〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 |
| 57 | 46, 17 | cfv 6561 |
. . . . . . . . . . . 12
class
(1st ‘𝑦) |
| 58 | 6, 37 | cfv 6561 |
. . . . . . . . . . . 12
class
(comp‘𝑟) |
| 59 | 56, 57, 58 | co 7431 |
. . . . . . . . . . 11
class
(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦)) |
| 60 | 50, 52, 59 | co 7431 |
. . . . . . . . . 10
class
((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)) |
| 61 | 49, 24 | cfv 6561 |
. . . . . . . . . . 11
class
(2nd ‘𝑔) |
| 62 | 51, 24 | cfv 6561 |
. . . . . . . . . . 11
class
(2nd ‘𝑓) |
| 63 | 53, 24 | cfv 6561 |
. . . . . . . . . . . . 13
class
(2nd ‘(1st ‘𝑥)) |
| 64 | 45, 24 | cfv 6561 |
. . . . . . . . . . . . 13
class
(2nd ‘(2nd ‘𝑥)) |
| 65 | 63, 64 | cop 4632 |
. . . . . . . . . . . 12
class
〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 |
| 66 | 46, 24 | cfv 6561 |
. . . . . . . . . . . 12
class
(2nd ‘𝑦) |
| 67 | 9, 37 | cfv 6561 |
. . . . . . . . . . . 12
class
(comp‘𝑠) |
| 68 | 65, 66, 67 | co 7431 |
. . . . . . . . . . 11
class
(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦)) |
| 69 | 61, 62, 68 | co 7431 |
. . . . . . . . . 10
class
((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓)) |
| 70 | 60, 69 | cop 4632 |
. . . . . . . . 9
class
〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉 |
| 71 | 42, 43, 47, 48, 70 | cmpo 7433 |
. . . . . . . 8
class (𝑔 ∈ ((2nd
‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉) |
| 72 | 39, 40, 41, 15, 71 | cmpo 7433 |
. . . . . . 7
class (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉)) |
| 73 | 38, 72 | cop 4632 |
. . . . . 6
class
〈(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉 |
| 74 | 33, 36, 73 | ctp 4630 |
. . . . 5
class
{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx), ℎ〉, 〈(comp‘ndx),
(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} |
| 75 | 12, 30, 74 | csb 3899 |
. . . 4
class
⦋(𝑢
∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} |
| 76 | 5, 11, 75 | csb 3899 |
. . 3
class
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} |
| 77 | 2, 3, 4, 4, 76 | cmpo 7433 |
. 2
class (𝑟 ∈ V, 𝑠 ∈ V ↦
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉}) |
| 78 | 1, 77 | wceq 1540 |
1
wff
×c = (𝑟 ∈ V, 𝑠 ∈ V ↦
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉}) |