Detailed syntax breakdown of Definition df-bj-fractemp
| Step | Hyp | Ref
| Expression |
| 1 | | cfractemp 37190 |
. 2
class
{R |
| 2 | | vx |
. . 3
setvar 𝑥 |
| 3 | | cnr 10901 |
. . 3
class
R |
| 4 | | vy |
. . . . . . . 8
setvar 𝑦 |
| 5 | 4 | cv 1539 |
. . . . . . 7
class 𝑦 |
| 6 | | c0r 10902 |
. . . . . . 7
class
0R |
| 7 | 5, 6 | wceq 1540 |
. . . . . 6
wff 𝑦 =
0R |
| 8 | | cltr 10907 |
. . . . . . . 8
class
<R |
| 9 | 6, 5, 8 | wbr 5141 |
. . . . . . 7
wff
0R <R 𝑦 |
| 10 | | c1r 10903 |
. . . . . . . 8
class
1R |
| 11 | 5, 10, 8 | wbr 5141 |
. . . . . . 7
wff 𝑦 <R
1R |
| 12 | 9, 11 | wa 395 |
. . . . . 6
wff
(0R <R 𝑦 ∧ 𝑦 <R
1R) |
| 13 | 7, 12 | wo 848 |
. . . . 5
wff (𝑦 = 0R
∨ (0R <R 𝑦 ∧ 𝑦 <R
1R)) |
| 14 | | vz |
. . . . . . . . . . . . 13
setvar 𝑧 |
| 15 | 14 | cv 1539 |
. . . . . . . . . . . 12
class 𝑧 |
| 16 | | vn |
. . . . . . . . . . . . . . 15
setvar 𝑛 |
| 17 | 16 | cv 1539 |
. . . . . . . . . . . . . 14
class 𝑛 |
| 18 | 17 | csuc 6384 |
. . . . . . . . . . . . 13
class suc 𝑛 |
| 19 | | c1o 8495 |
. . . . . . . . . . . . 13
class
1o |
| 20 | 18, 19 | cop 4630 |
. . . . . . . . . . . 12
class 〈suc
𝑛,
1o〉 |
| 21 | | cltq 10894 |
. . . . . . . . . . . 12
class
<Q |
| 22 | 15, 20, 21 | wbr 5141 |
. . . . . . . . . . 11
wff 𝑧 <Q
〈suc 𝑛,
1o〉 |
| 23 | | cnq 10888 |
. . . . . . . . . . 11
class
Q |
| 24 | 22, 14, 23 | crab 3435 |
. . . . . . . . . 10
class {𝑧 ∈ Q ∣
𝑧
<Q 〈suc 𝑛, 1o〉} |
| 25 | | c1p 10896 |
. . . . . . . . . 10
class
1P |
| 26 | 24, 25 | cop 4630 |
. . . . . . . . 9
class
〈{𝑧 ∈
Q ∣ 𝑧
<Q 〈suc 𝑛, 1o〉},
1P〉 |
| 27 | | cer 10900 |
. . . . . . . . 9
class
~R |
| 28 | 26, 27 | cec 8739 |
. . . . . . . 8
class
[〈{𝑧 ∈
Q ∣ 𝑧
<Q 〈suc 𝑛, 1o〉},
1P〉] ~R |
| 29 | | cplr 10905 |
. . . . . . . 8
class
+R |
| 30 | 28, 5, 29 | co 7429 |
. . . . . . 7
class
([〈{𝑧 ∈
Q ∣ 𝑧
<Q 〈suc 𝑛, 1o〉},
1P〉] ~R
+R 𝑦) |
| 31 | 2 | cv 1539 |
. . . . . . 7
class 𝑥 |
| 32 | 30, 31 | wceq 1540 |
. . . . . 6
wff
([〈{𝑧 ∈
Q ∣ 𝑧
<Q 〈suc 𝑛, 1o〉},
1P〉] ~R
+R 𝑦) = 𝑥 |
| 33 | | com 7883 |
. . . . . 6
class
ω |
| 34 | 32, 16, 33 | wrex 3069 |
. . . . 5
wff
∃𝑛 ∈
ω ([〈{𝑧 ∈
Q ∣ 𝑧
<Q 〈suc 𝑛, 1o〉},
1P〉] ~R
+R 𝑦) = 𝑥 |
| 35 | 13, 34 | wa 395 |
. . . 4
wff ((𝑦 = 0R
∨ (0R <R 𝑦 ∧ 𝑦 <R
1R)) ∧ ∃𝑛 ∈ ω ([〈{𝑧 ∈ Q ∣ 𝑧 <Q
〈suc 𝑛,
1o〉}, 1P〉]
~R +R 𝑦) = 𝑥) |
| 36 | 35, 4, 3 | crio 7385 |
. . 3
class
(℩𝑦
∈ R ((𝑦
= 0R ∨ (0R
<R 𝑦 ∧ 𝑦 <R
1R)) ∧ ∃𝑛 ∈ ω ([〈{𝑧 ∈ Q ∣ 𝑧 <Q
〈suc 𝑛,
1o〉}, 1P〉]
~R +R 𝑦) = 𝑥)) |
| 37 | 2, 3, 36 | cmpt 5223 |
. 2
class (𝑥 ∈ R ↦
(℩𝑦 ∈
R ((𝑦 =
0R ∨ (0R
<R 𝑦 ∧ 𝑦 <R
1R)) ∧ ∃𝑛 ∈ ω ([〈{𝑧 ∈ Q ∣ 𝑧 <Q
〈suc 𝑛,
1o〉}, 1P〉]
~R +R 𝑦) = 𝑥))) |
| 38 | 1, 37 | wceq 1540 |
1
wff
{R = (𝑥 ∈ R ↦
(℩𝑦 ∈
R ((𝑦 =
0R ∨ (0R
<R 𝑦 ∧ 𝑦 <R
1R)) ∧ ∃𝑛 ∈ ω ([〈{𝑧 ∈ Q ∣ 𝑧 <Q
〈suc 𝑛,
1o〉}, 1P〉]
~R +R 𝑦) = 𝑥))) |