Detailed syntax breakdown of Definition df-sup
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class 𝐴 |
2 | | cB |
. . 3
class 𝐵 |
3 | | cR |
. . 3
class 𝑅 |
4 | 1, 2, 3 | csup 8970 |
. 2
class sup(𝐴, 𝐵, 𝑅) |
5 | | vx |
. . . . . . . . 9
setvar 𝑥 |
6 | 5 | cv 1541 |
. . . . . . . 8
class 𝑥 |
7 | | vy |
. . . . . . . . 9
setvar 𝑦 |
8 | 7 | cv 1541 |
. . . . . . . 8
class 𝑦 |
9 | 6, 8, 3 | wbr 5027 |
. . . . . . 7
wff 𝑥𝑅𝑦 |
10 | 9 | wn 3 |
. . . . . 6
wff ¬
𝑥𝑅𝑦 |
11 | 10, 7, 1 | wral 3053 |
. . . . 5
wff
∀𝑦 ∈
𝐴 ¬ 𝑥𝑅𝑦 |
12 | 8, 6, 3 | wbr 5027 |
. . . . . . 7
wff 𝑦𝑅𝑥 |
13 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
14 | 13 | cv 1541 |
. . . . . . . . 9
class 𝑧 |
15 | 8, 14, 3 | wbr 5027 |
. . . . . . . 8
wff 𝑦𝑅𝑧 |
16 | 15, 13, 1 | wrex 3054 |
. . . . . . 7
wff
∃𝑧 ∈
𝐴 𝑦𝑅𝑧 |
17 | 12, 16 | wi 4 |
. . . . . 6
wff (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧) |
18 | 17, 7, 2 | wral 3053 |
. . . . 5
wff
∀𝑦 ∈
𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧) |
19 | 11, 18 | wa 399 |
. . . 4
wff
(∀𝑦 ∈
𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧)) |
20 | 19, 5, 2 | crab 3057 |
. . 3
class {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} |
21 | 20 | cuni 4793 |
. 2
class ∪ {𝑥
∈ 𝐵 ∣
(∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} |
22 | 4, 21 | wceq 1542 |
1
wff sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} |