Step | Hyp | Ref
| Expression |
1 | | df-1 7818 |
. 2
⊢ 1 =
⟨1R,
0R⟩ |
2 | | df-1r 7730 |
. . . 4
⊢
1R = [⟨(1P
+P 1P),
1P⟩] ~R |
3 | | df-i1p 7465 |
. . . . . . . 8
⊢
1P = ⟨{𝑙 ∣ 𝑙 <Q
1Q}, {𝑢 ∣ 1Q
<Q 𝑢}⟩ |
4 | | df-1nqqs 7349 |
. . . . . . . . . . 11
⊢
1Q = [⟨1o, 1o⟩]
~Q |
5 | 4 | breq2i 4011 |
. . . . . . . . . 10
⊢ (𝑙 <Q
1Q ↔ 𝑙 <Q
[⟨1o, 1o⟩] ~Q
) |
6 | 5 | abbii 2293 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q
1Q} = {𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q
} |
7 | 4 | breq1i 4010 |
. . . . . . . . . 10
⊢
(1Q <Q 𝑢 ↔ [⟨1o,
1o⟩] ~Q <Q
𝑢) |
8 | 7 | abbii 2293 |
. . . . . . . . 9
⊢ {𝑢 ∣
1Q <Q 𝑢} = {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢} |
9 | 6, 8 | opeq12i 3783 |
. . . . . . . 8
⊢
⟨{𝑙 ∣
𝑙
<Q 1Q}, {𝑢 ∣
1Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ |
10 | 3, 9 | eqtri 2198 |
. . . . . . 7
⊢
1P = ⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ |
11 | 10 | oveq1i 5884 |
. . . . . 6
⊢
(1P +P
1P) = (⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P) |
12 | 11 | opeq1i 3781 |
. . . . 5
⊢
⟨(1P +P
1P), 1P⟩ =
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨1o, 1o⟩]
~Q }, {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩ |
13 | | eceq1 6569 |
. . . . 5
⊢
(⟨(1P +P
1P), 1P⟩ =
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨1o, 1o⟩]
~Q }, {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩ → [⟨(1P
+P 1P),
1P⟩] ~R =
[⟨(⟨{𝑙 ∣
𝑙
<Q [⟨1o, 1o⟩]
~Q }, {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R
) |
14 | 12, 13 | ax-mp 5 |
. . . 4
⊢
[⟨(1P +P
1P), 1P⟩]
~R = [⟨(⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R |
15 | 2, 14 | eqtri 2198 |
. . 3
⊢
1R = [⟨(⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R |
16 | 15 | opeq1i 3781 |
. 2
⊢
⟨1R, 0R⟩ =
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨1o, 1o⟩]
~Q }, {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩ |
17 | 1, 16 | eqtr2i 2199 |
1
⊢
⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
1 |