Step | Hyp | Ref
| Expression |
1 | | addnqprlemrl 7508 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉)) |
2 | | ltsonq 7349 |
. . . . . . . . 9
⊢
<Q Or Q |
3 | | addclnq 7326 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
+Q 𝐵) ∈ Q) |
4 | | sonr 4300 |
. . . . . . . . 9
⊢ ((
<Q Or Q ∧ (𝐴 +Q 𝐵) ∈ Q) →
¬ (𝐴
+Q 𝐵) <Q (𝐴 +Q
𝐵)) |
5 | 2, 3, 4 | sylancr 412 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) <Q (𝐴 +Q
𝐵)) |
6 | | ltrelnq 7316 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 4661 |
. . . . . . . . . . 11
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → ((𝐴 +Q 𝐵) ∈ Q ∧
(𝐴
+Q 𝐵) ∈ Q)) |
8 | 7 | simpld 111 |
. . . . . . . . . 10
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → (𝐴 +Q 𝐵) ∈
Q) |
9 | | elex 2741 |
. . . . . . . . . 10
⊢ ((𝐴 +Q
𝐵) ∈ Q
→ (𝐴
+Q 𝐵) ∈ V) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → (𝐴 +Q 𝐵) ∈ V) |
11 | | breq1 3990 |
. . . . . . . . 9
⊢ (𝑙 = (𝐴 +Q 𝐵) → (𝑙 <Q (𝐴 +Q
𝐵) ↔ (𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵))) |
12 | 10, 11 | elab3 2882 |
. . . . . . . 8
⊢ ((𝐴 +Q
𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} ↔ (𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵)) |
13 | 5, 12 | sylnibr 672 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}) |
14 | | ltnqex 7500 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} ∈
V |
15 | | gtnqex 7501 |
. . . . . . . . 9
⊢ {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢} ∈
V |
16 | 14, 15 | op1st 6123 |
. . . . . . . 8
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) = {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} |
17 | 16 | eleq2i 2237 |
. . . . . . 7
⊢ ((𝐴 +Q
𝐵) ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) ↔ (𝐴 +Q
𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}) |
18 | 13, 17 | sylnibr 672 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉)) |
19 | 1, 18 | ssneldd 3150 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) ∈ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
20 | 19 | adantr 274 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉)) → ¬
(𝐴
+Q 𝐵) ∈ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
21 | | nqprlu 7498 |
. . . . . . . 8
⊢ (𝐴 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈
P) |
22 | | nqprlu 7498 |
. . . . . . . 8
⊢ (𝐵 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈
P) |
23 | | addclpr 7488 |
. . . . . . . 8
⊢
((〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈ P
∧ 〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈ P)
→ (〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ∈
P) |
24 | 21, 22, 23 | syl2an 287 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ∈
P) |
25 | | prop 7426 |
. . . . . . 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 2733 |
. . . . . . . 8
⊢ 𝑟 ∈ V |
28 | | breq2 3991 |
. . . . . . . 8
⊢ (𝑢 = 𝑟 → ((𝐴 +Q 𝐵) <Q
𝑢 ↔ (𝐴 +Q 𝐵) <Q
𝑟)) |
29 | 14, 15 | op2nd 6124 |
. . . . . . . 8
⊢
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) = {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢} |
30 | 27, 28, 29 | elab2 2878 |
. . . . . . 7
⊢ (𝑟 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) ↔ (𝐴 +Q
𝐵)
<Q 𝑟) |
31 | 30 | biimpi 119 |
. . . . . 6
⊢ (𝑟 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) → (𝐴 +Q
𝐵)
<Q 𝑟) |
32 | | prloc 7442 |
. . . . . 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 287 |
. . . . 5
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉)) → ((𝐴 +Q
𝐵) ∈ (1st
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ∨ 𝑟 ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)))) |
34 | 33 | orcomd 724 |
. . . 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 1344 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉)) → 𝑟 ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |
36 | 35 | ex 114 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝑟 ∈
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) → 𝑟 ∈ (2nd
‘(〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)))) |
37 | 36 | ssrdv 3153 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) ⊆
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) |