Detailed syntax breakdown of Definition df-line3
Step | Hyp | Ref
| Expression |
1 | | cline3 38666 |
. 2
class
line3 |
2 | | c2o 7554 |
. . . . 5
class
2𝑜 |
3 | | vx |
. . . . . 6
setvar 𝑥 |
4 | 3 | cv 1482 |
. . . . 5
class 𝑥 |
5 | | cdom 7953 |
. . . . 5
class
≼ |
6 | 2, 4, 5 | wbr 4653 |
. . . 4
wff
2𝑜 ≼ 𝑥 |
7 | | vz |
. . . . . . . . 9
setvar 𝑧 |
8 | 7 | cv 1482 |
. . . . . . . 8
class 𝑧 |
9 | | vy |
. . . . . . . . 9
setvar 𝑦 |
10 | 9 | cv 1482 |
. . . . . . . 8
class 𝑦 |
11 | 8, 10 | wne 2794 |
. . . . . . 7
wff 𝑧 ≠ 𝑦 |
12 | 10, 8 | cptdfc 38664 |
. . . . . . . . 9
class
PtDf(𝑦, 𝑧) |
13 | 12 | crn 5115 |
. . . . . . . 8
class ran
PtDf(𝑦, 𝑧) |
14 | 13, 4 | wceq 1483 |
. . . . . . 7
wff ran
PtDf(𝑦, 𝑧) = 𝑥 |
15 | 11, 14 | wi 4 |
. . . . . 6
wff (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥) |
16 | 15, 7, 4 | wral 2912 |
. . . . 5
wff
∀𝑧 ∈
𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥) |
17 | 16, 9, 4 | wral 2912 |
. . . 4
wff
∀𝑦 ∈
𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥) |
18 | 6, 17 | wa 384 |
. . 3
wff
(2𝑜 ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥)) |
19 | | crr3c 38665 |
. . . 4
class
RR3 |
20 | 19 | cpw 4158 |
. . 3
class 𝒫
RR3 |
21 | 18, 3, 20 | crab 2916 |
. 2
class {𝑥 ∈ 𝒫 RR3 ∣
(2𝑜 ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))} |
22 | 1, 21 | wceq 1483 |
1
wff line3 =
{𝑥 ∈ 𝒫 RR3
∣ (2𝑜 ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))} |