Step | Hyp | Ref
| Expression |
1 | | addnqprlemrl 7570 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ⊆
(1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) |
2 | | ltsonq 7411 |
. . . . . . . . 9
⊢
<Q Or Q |
3 | | addclnq 7388 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
+Q 𝐵) ∈ Q) |
4 | | sonr 4329 |
. . . . . . . . 9
⊢ ((
<Q Or Q ∧ (𝐴 +Q 𝐵) ∈ Q) →
¬ (𝐴
+Q 𝐵) <Q (𝐴 +Q
𝐵)) |
5 | 2, 3, 4 | sylancr 414 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) <Q (𝐴 +Q
𝐵)) |
6 | | ltrelnq 7378 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 4690 |
. . . . . . . . . . 11
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → ((𝐴 +Q 𝐵) ∈ Q ∧
(𝐴
+Q 𝐵) ∈ Q)) |
8 | 7 | simpld 112 |
. . . . . . . . . 10
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → (𝐴 +Q 𝐵) ∈
Q) |
9 | | elex 2760 |
. . . . . . . . . 10
⊢ ((𝐴 +Q
𝐵) ∈ Q
→ (𝐴
+Q 𝐵) ∈ V) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → (𝐴 +Q 𝐵) ∈ V) |
11 | | breq1 4018 |
. . . . . . . . 9
⊢ (𝑙 = (𝐴 +Q 𝐵) → (𝑙 <Q (𝐴 +Q
𝐵) ↔ (𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵))) |
12 | 10, 11 | elab3 2901 |
. . . . . . . 8
⊢ ((𝐴 +Q
𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} ↔ (𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵)) |
13 | 5, 12 | sylnibr 678 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}) |
14 | | ltnqex 7562 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} ∈
V |
15 | | gtnqex 7563 |
. . . . . . . . 9
⊢ {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢} ∈
V |
16 | 14, 15 | op1st 6161 |
. . . . . . . 8
⊢
(1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} |
17 | 16 | eleq2i 2254 |
. . . . . . 7
⊢ ((𝐴 +Q
𝐵) ∈ (1st
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) ↔ (𝐴 +Q
𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}) |
18 | 13, 17 | sylnibr 678 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) ∈ (1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) |
19 | 1, 18 | ssneldd 3170 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) ∈ (1st
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |
20 | 19 | adantr 276 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) → ¬
(𝐴
+Q 𝐵) ∈ (1st
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |
21 | | nqprlu 7560 |
. . . . . . . 8
⊢ (𝐴 ∈ Q →
⟨{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈
P) |
22 | | nqprlu 7560 |
. . . . . . . 8
⊢ (𝐵 ∈ Q →
⟨{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩ ∈
P) |
23 | | addclpr 7550 |
. . . . . . . 8
⊢
((⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈ P
∧ ⟨{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩ ∈ P)
→ (⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩) ∈
P) |
24 | 21, 22, 23 | syl2an 289 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩) ∈
P) |
25 | | prop 7488 |
. . . . . . 7
⊢
((⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩) ∈ P
→ ⟨(1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)), (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))⟩ ∈
P) |
26 | 24, 25 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ⟨(1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)), (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))⟩ ∈
P) |
27 | | vex 2752 |
. . . . . . . 8
⊢ 𝑟 ∈ V |
28 | | breq2 4019 |
. . . . . . . 8
⊢ (𝑢 = 𝑟 → ((𝐴 +Q 𝐵) <Q
𝑢 ↔ (𝐴 +Q 𝐵) <Q
𝑟)) |
29 | 14, 15 | op2nd 6162 |
. . . . . . . 8
⊢
(2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢} |
30 | 27, 28, 29 | elab2 2897 |
. . . . . . 7
⊢ (𝑟 ∈ (2nd
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) ↔ (𝐴 +Q
𝐵)
<Q 𝑟) |
31 | 30 | biimpi 120 |
. . . . . 6
⊢ (𝑟 ∈ (2nd
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) → (𝐴 +Q
𝐵)
<Q 𝑟) |
32 | | prloc 7504 |
. . . . . 6
⊢
((⟨(1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)), (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))⟩ ∈
P ∧ (𝐴
+Q 𝐵) <Q 𝑟) → ((𝐴 +Q 𝐵) ∈ (1st
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ∨ 𝑟 ∈ (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)))) |
33 | 26, 31, 32 | syl2an 289 |
. . . . 5
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) → ((𝐴 +Q
𝐵) ∈ (1st
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ∨ 𝑟 ∈ (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)))) |
34 | 33 | orcomd 730 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) → (𝑟 ∈ (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ∨ (𝐴 +Q
𝐵) ∈ (1st
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)))) |
35 | 20, 34 | ecased 1359 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) → 𝑟 ∈ (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |
36 | 35 | ex 115 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝑟 ∈
(2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) → 𝑟 ∈ (2nd
‘(⟨{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)))) |
37 | 36 | ssrdv 3173 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) ⊆
(2nd ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |