Detailed syntax breakdown of Definition df-imp
Step | Hyp | Ref
| Expression |
1 | | cmp 6278 |
. 2
class
·P |
2 | | vx |
. . 3
setvar x |
3 | | vy |
. . 3
setvar y |
4 | | cnp 6275 |
. . 3
class
P |
5 | | vr |
. . . . . . . . . 10
setvar 𝑟 |
6 | 5 | cv 1241 |
. . . . . . . . 9
class 𝑟 |
7 | 2 | cv 1241 |
. . . . . . . . . 10
class x |
8 | | c1st 5707 |
. . . . . . . . . 10
class
1st |
9 | 7, 8 | cfv 4845 |
. . . . . . . . 9
class (1st
‘x) |
10 | 6, 9 | wcel 1390 |
. . . . . . . 8
wff 𝑟 ∈
(1st ‘x) |
11 | | vs |
. . . . . . . . . 10
setvar 𝑠 |
12 | 11 | cv 1241 |
. . . . . . . . 9
class 𝑠 |
13 | 3 | cv 1241 |
. . . . . . . . . 10
class y |
14 | 13, 8 | cfv 4845 |
. . . . . . . . 9
class (1st
‘y) |
15 | 12, 14 | wcel 1390 |
. . . . . . . 8
wff 𝑠 ∈
(1st ‘y) |
16 | | vq |
. . . . . . . . . 10
setvar 𝑞 |
17 | 16 | cv 1241 |
. . . . . . . . 9
class 𝑞 |
18 | | cmq 6267 |
. . . . . . . . . 10
class
·Q |
19 | 6, 12, 18 | co 5455 |
. . . . . . . . 9
class (𝑟 ·Q 𝑠) |
20 | 17, 19 | wceq 1242 |
. . . . . . . 8
wff 𝑞 = (𝑟 ·Q 𝑠) |
21 | 10, 15, 20 | w3a 884 |
. . . . . . 7
wff (𝑟 ∈
(1st ‘x) ∧ 𝑠
∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠)) |
22 | | cnq 6264 |
. . . . . . 7
class
Q |
23 | 21, 11, 22 | wrex 2301 |
. . . . . 6
wff ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠)) |
24 | 23, 5, 22 | wrex 2301 |
. . . . 5
wff ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠)) |
25 | 24, 16, 22 | crab 2304 |
. . . 4
class {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))} |
26 | | c2nd 5708 |
. . . . . . . . . 10
class
2nd |
27 | 7, 26 | cfv 4845 |
. . . . . . . . 9
class (2nd
‘x) |
28 | 6, 27 | wcel 1390 |
. . . . . . . 8
wff 𝑟 ∈
(2nd ‘x) |
29 | 13, 26 | cfv 4845 |
. . . . . . . . 9
class (2nd
‘y) |
30 | 12, 29 | wcel 1390 |
. . . . . . . 8
wff 𝑠 ∈
(2nd ‘y) |
31 | 28, 30, 20 | w3a 884 |
. . . . . . 7
wff (𝑟 ∈
(2nd ‘x) ∧ 𝑠
∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠)) |
32 | 31, 11, 22 | wrex 2301 |
. . . . . 6
wff ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠)) |
33 | 32, 5, 22 | wrex 2301 |
. . . . 5
wff ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠)) |
34 | 33, 16, 22 | crab 2304 |
. . . 4
class {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))} |
35 | 25, 34 | cop 3370 |
. . 3
class 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}〉 |
36 | 2, 3, 4, 4, 35 | cmpt2 5457 |
. 2
class (x ∈
P, y ∈ P ↦ 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}〉) |
37 | 1, 36 | wceq 1242 |
1
wff
·P = (x
∈ P, y ∈
P ↦ 〈{𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈
Q ∣ ∃𝑟 ∈
Q ∃𝑠 ∈
Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}〉) |