Detailed syntax breakdown of Definition df-com2
Step | Hyp | Ref
| Expression |
1 | | ccm2 35759 |
. 2
class
Com2 |
2 | | va |
. . . . . . . 8
setvar 𝑎 |
3 | 2 | cv 1541 |
. . . . . . 7
class 𝑎 |
4 | | vb |
. . . . . . . 8
setvar 𝑏 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑏 |
6 | | vh |
. . . . . . . 8
setvar ℎ |
7 | 6 | cv 1541 |
. . . . . . 7
class ℎ |
8 | 3, 5, 7 | co 7164 |
. . . . . 6
class (𝑎ℎ𝑏) |
9 | 5, 3, 7 | co 7164 |
. . . . . 6
class (𝑏ℎ𝑎) |
10 | 8, 9 | wceq 1542 |
. . . . 5
wff (𝑎ℎ𝑏) = (𝑏ℎ𝑎) |
11 | | vg |
. . . . . . 7
setvar 𝑔 |
12 | 11 | cv 1541 |
. . . . . 6
class 𝑔 |
13 | 12 | crn 5520 |
. . . . 5
class ran 𝑔 |
14 | 10, 4, 13 | wral 3053 |
. . . 4
wff
∀𝑏 ∈ ran
𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎) |
15 | 14, 2, 13 | wral 3053 |
. . 3
wff
∀𝑎 ∈ ran
𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎) |
16 | 15, 11, 6 | copab 5089 |
. 2
class
{〈𝑔, ℎ〉 ∣ ∀𝑎 ∈ ran 𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)} |
17 | 1, 16 | wceq 1542 |
1
wff Com2 =
{〈𝑔, ℎ〉 ∣ ∀𝑎 ∈ ran 𝑔∀𝑏 ∈ ran 𝑔(𝑎ℎ𝑏) = (𝑏ℎ𝑎)} |