Detailed syntax breakdown of Definition df-padd
| Step | Hyp | Ref
| Expression |
| 1 | | cpadd 39797 |
. 2
class
+𝑃 |
| 2 | | vl |
. . 3
setvar 𝑙 |
| 3 | | cvv 3480 |
. . 3
class
V |
| 4 | | vm |
. . . 4
setvar 𝑚 |
| 5 | | vn |
. . . 4
setvar 𝑛 |
| 6 | 2 | cv 1539 |
. . . . . 6
class 𝑙 |
| 7 | | catm 39264 |
. . . . . 6
class
Atoms |
| 8 | 6, 7 | cfv 6561 |
. . . . 5
class
(Atoms‘𝑙) |
| 9 | 8 | cpw 4600 |
. . . 4
class 𝒫
(Atoms‘𝑙) |
| 10 | 4 | cv 1539 |
. . . . . 6
class 𝑚 |
| 11 | 5 | cv 1539 |
. . . . . 6
class 𝑛 |
| 12 | 10, 11 | cun 3949 |
. . . . 5
class (𝑚 ∪ 𝑛) |
| 13 | | vp |
. . . . . . . . . 10
setvar 𝑝 |
| 14 | 13 | cv 1539 |
. . . . . . . . 9
class 𝑝 |
| 15 | | vq |
. . . . . . . . . . 11
setvar 𝑞 |
| 16 | 15 | cv 1539 |
. . . . . . . . . 10
class 𝑞 |
| 17 | | vr |
. . . . . . . . . . 11
setvar 𝑟 |
| 18 | 17 | cv 1539 |
. . . . . . . . . 10
class 𝑟 |
| 19 | | cjn 18357 |
. . . . . . . . . . 11
class
join |
| 20 | 6, 19 | cfv 6561 |
. . . . . . . . . 10
class
(join‘𝑙) |
| 21 | 16, 18, 20 | co 7431 |
. . . . . . . . 9
class (𝑞(join‘𝑙)𝑟) |
| 22 | | cple 17304 |
. . . . . . . . . 10
class
le |
| 23 | 6, 22 | cfv 6561 |
. . . . . . . . 9
class
(le‘𝑙) |
| 24 | 14, 21, 23 | wbr 5143 |
. . . . . . . 8
wff 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟) |
| 25 | 24, 17, 11 | wrex 3070 |
. . . . . . 7
wff
∃𝑟 ∈
𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟) |
| 26 | 25, 15, 10 | wrex 3070 |
. . . . . 6
wff
∃𝑞 ∈
𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟) |
| 27 | 26, 13, 8 | crab 3436 |
. . . . 5
class {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)} |
| 28 | 12, 27 | cun 3949 |
. . . 4
class ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}) |
| 29 | 4, 5, 9, 9, 28 | cmpo 7433 |
. . 3
class (𝑚 ∈ 𝒫
(Atoms‘𝑙), 𝑛 ∈ 𝒫
(Atoms‘𝑙) ↦
((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})) |
| 30 | 2, 3, 29 | cmpt 5225 |
. 2
class (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫
(Atoms‘𝑙), 𝑛 ∈ 𝒫
(Atoms‘𝑙) ↦
((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))) |
| 31 | 1, 30 | wceq 1540 |
1
wff
+𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)}))) |