Step | Hyp | Ref
| Expression |
1 | | cxpc 17205 |
. 2
class
×_{c} |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cvv 3398 |
. . 3
class
V |
5 | | vb |
. . . 4
setvar 𝑏 |
6 | 2 | cv 1600 |
. . . . . 6
class 𝑟 |
7 | | cbs 16266 |
. . . . . 6
class
Base |
8 | 6, 7 | cfv 6137 |
. . . . 5
class
(Base‘𝑟) |
9 | 3 | cv 1600 |
. . . . . 6
class 𝑠 |
10 | 9, 7 | cfv 6137 |
. . . . 5
class
(Base‘𝑠) |
11 | 8, 10 | cxp 5355 |
. . . 4
class
((Base‘𝑟)
× (Base‘𝑠)) |
12 | | vh |
. . . . 5
setvar ℎ |
13 | | vu |
. . . . . 6
setvar 𝑢 |
14 | | vv |
. . . . . 6
setvar 𝑣 |
15 | 5 | cv 1600 |
. . . . . 6
class 𝑏 |
16 | 13 | cv 1600 |
. . . . . . . . 9
class 𝑢 |
17 | | c1st 7445 |
. . . . . . . . 9
class
1^{st} |
18 | 16, 17 | cfv 6137 |
. . . . . . . 8
class
(1^{st} ‘𝑢) |
19 | 14 | cv 1600 |
. . . . . . . . 9
class 𝑣 |
20 | 19, 17 | cfv 6137 |
. . . . . . . 8
class
(1^{st} ‘𝑣) |
21 | | chom 16360 |
. . . . . . . . 9
class
Hom |
22 | 6, 21 | cfv 6137 |
. . . . . . . 8
class (Hom
‘𝑟) |
23 | 18, 20, 22 | co 6924 |
. . . . . . 7
class
((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) |
24 | | c2nd 7446 |
. . . . . . . . 9
class
2^{nd} |
25 | 16, 24 | cfv 6137 |
. . . . . . . 8
class
(2^{nd} ‘𝑢) |
26 | 19, 24 | cfv 6137 |
. . . . . . . 8
class
(2^{nd} ‘𝑣) |
27 | 9, 21 | cfv 6137 |
. . . . . . . 8
class (Hom
‘𝑠) |
28 | 25, 26, 27 | co 6924 |
. . . . . . 7
class
((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)) |
29 | 23, 28 | cxp 5355 |
. . . . . 6
class
(((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣))) |
30 | 13, 14, 15, 15, 29 | cmpt2 6926 |
. . . . 5
class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) |
31 | | cnx 16263 |
. . . . . . . 8
class
ndx |
32 | 31, 7 | cfv 6137 |
. . . . . . 7
class
(Base‘ndx) |
33 | 32, 15 | cop 4404 |
. . . . . 6
class
⟨(Base‘ndx), 𝑏⟩ |
34 | 31, 21 | cfv 6137 |
. . . . . . 7
class (Hom
‘ndx) |
35 | 12 | cv 1600 |
. . . . . . 7
class ℎ |
36 | 34, 35 | cop 4404 |
. . . . . 6
class
⟨(Hom ‘ndx), ℎ⟩ |
37 | | cco 16361 |
. . . . . . . 8
class
comp |
38 | 31, 37 | cfv 6137 |
. . . . . . 7
class
(comp‘ndx) |
39 | | vx |
. . . . . . . 8
setvar 𝑥 |
40 | | vy |
. . . . . . . 8
setvar 𝑦 |
41 | 15, 15 | cxp 5355 |
. . . . . . . 8
class (𝑏 × 𝑏) |
42 | | vg |
. . . . . . . . 9
setvar 𝑔 |
43 | | vf |
. . . . . . . . 9
setvar 𝑓 |
44 | 39 | cv 1600 |
. . . . . . . . . . 11
class 𝑥 |
45 | 44, 24 | cfv 6137 |
. . . . . . . . . 10
class
(2^{nd} ‘𝑥) |
46 | 40 | cv 1600 |
. . . . . . . . . 10
class 𝑦 |
47 | 45, 46, 35 | co 6924 |
. . . . . . . . 9
class
((2^{nd} ‘𝑥)ℎ𝑦) |
48 | 44, 35 | cfv 6137 |
. . . . . . . . 9
class (ℎ‘𝑥) |
49 | 42 | cv 1600 |
. . . . . . . . . . . 12
class 𝑔 |
50 | 49, 17 | cfv 6137 |
. . . . . . . . . . 11
class
(1^{st} ‘𝑔) |
51 | 43 | cv 1600 |
. . . . . . . . . . . 12
class 𝑓 |
52 | 51, 17 | cfv 6137 |
. . . . . . . . . . 11
class
(1^{st} ‘𝑓) |
53 | 44, 17 | cfv 6137 |
. . . . . . . . . . . . . 14
class
(1^{st} ‘𝑥) |
54 | 53, 17 | cfv 6137 |
. . . . . . . . . . . . 13
class
(1^{st} ‘(1^{st} ‘𝑥)) |
55 | 45, 17 | cfv 6137 |
. . . . . . . . . . . . 13
class
(1^{st} ‘(2^{nd} ‘𝑥)) |
56 | 54, 55 | cop 4404 |
. . . . . . . . . . . 12
class
⟨(1^{st} ‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ |
57 | 46, 17 | cfv 6137 |
. . . . . . . . . . . 12
class
(1^{st} ‘𝑦) |
58 | 6, 37 | cfv 6137 |
. . . . . . . . . . . 12
class
(comp‘𝑟) |
59 | 56, 57, 58 | co 6924 |
. . . . . . . . . . 11
class
(⟨(1^{st} ‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦)) |
60 | 50, 52, 59 | co 6924 |
. . . . . . . . . 10
class
((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) |
61 | 49, 24 | cfv 6137 |
. . . . . . . . . . 11
class
(2^{nd} ‘𝑔) |
62 | 51, 24 | cfv 6137 |
. . . . . . . . . . 11
class
(2^{nd} ‘𝑓) |
63 | 53, 24 | cfv 6137 |
. . . . . . . . . . . . 13
class
(2^{nd} ‘(1^{st} ‘𝑥)) |
64 | 45, 24 | cfv 6137 |
. . . . . . . . . . . . 13
class
(2^{nd} ‘(2^{nd} ‘𝑥)) |
65 | 63, 64 | cop 4404 |
. . . . . . . . . . . 12
class
⟨(2^{nd} ‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ |
66 | 46, 24 | cfv 6137 |
. . . . . . . . . . . 12
class
(2^{nd} ‘𝑦) |
67 | 9, 37 | cfv 6137 |
. . . . . . . . . . . 12
class
(comp‘𝑠) |
68 | 65, 66, 67 | co 6924 |
. . . . . . . . . . 11
class
(⟨(2^{nd} ‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦)) |
69 | 61, 62, 68 | co 6924 |
. . . . . . . . . 10
class
((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) |
70 | 60, 69 | cop 4404 |
. . . . . . . . 9
class
⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩ |
71 | 42, 43, 47, 48, 70 | cmpt2 6926 |
. . . . . . . 8
class (𝑔 ∈ ((2^{nd}
‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) |
72 | 39, 40, 41, 15, 71 | cmpt2 6926 |
. . . . . . 7
class (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) |
73 | 38, 72 | cop 4404 |
. . . . . 6
class
⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩ |
74 | 33, 36, 73 | ctp 4402 |
. . . . 5
class
{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx),
(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} |
75 | 12, 30, 74 | csb 3751 |
. . . 4
class
⦋(𝑢
∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} |
76 | 5, 11, 75 | csb 3751 |
. . 3
class
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} |
77 | 2, 3, 4, 4, 76 | cmpt2 6926 |
. 2
class (𝑟 ∈ V, 𝑠 ∈ V ↦
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩}) |
78 | 1, 77 | wceq 1601 |
1
wff
×_{c} = (𝑟 ∈ V, 𝑠 ∈ V ↦
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩}) |