Detailed syntax breakdown of Definition df-gru
Step | Hyp | Ref
| Expression |
1 | | cgru 10293 |
. 2
class
Univ |
2 | | vu |
. . . . . 6
setvar 𝑢 |
3 | 2 | cv 1541 |
. . . . 5
class 𝑢 |
4 | 3 | wtr 5137 |
. . . 4
wff Tr 𝑢 |
5 | | vx |
. . . . . . . . 9
setvar 𝑥 |
6 | 5 | cv 1541 |
. . . . . . . 8
class 𝑥 |
7 | 6 | cpw 4489 |
. . . . . . 7
class 𝒫
𝑥 |
8 | 7, 3 | wcel 2114 |
. . . . . 6
wff 𝒫
𝑥 ∈ 𝑢 |
9 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
10 | 9 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
11 | 6, 10 | cpr 4519 |
. . . . . . . 8
class {𝑥, 𝑦} |
12 | 11, 3 | wcel 2114 |
. . . . . . 7
wff {𝑥, 𝑦} ∈ 𝑢 |
13 | 12, 9, 3 | wral 3054 |
. . . . . 6
wff
∀𝑦 ∈
𝑢 {𝑥, 𝑦} ∈ 𝑢 |
14 | 10 | crn 5527 |
. . . . . . . . 9
class ran 𝑦 |
15 | 14 | cuni 4797 |
. . . . . . . 8
class ∪ ran 𝑦 |
16 | 15, 3 | wcel 2114 |
. . . . . . 7
wff ∪ ran 𝑦 ∈ 𝑢 |
17 | | cmap 8440 |
. . . . . . . 8
class
↑m |
18 | 3, 6, 17 | co 7173 |
. . . . . . 7
class (𝑢 ↑m 𝑥) |
19 | 16, 9, 18 | wral 3054 |
. . . . . 6
wff
∀𝑦 ∈
(𝑢 ↑m 𝑥)∪
ran 𝑦 ∈ 𝑢 |
20 | 8, 13, 19 | w3a 1088 |
. . . . 5
wff (𝒫
𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) |
21 | 20, 5, 3 | wral 3054 |
. . . 4
wff
∀𝑥 ∈
𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢) |
22 | 4, 21 | wa 399 |
. . 3
wff (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢)) |
23 | 22, 2 | cab 2717 |
. 2
class {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))} |
24 | 1, 23 | wceq 1542 |
1
wff Univ =
{𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))} |