Step | Hyp | Ref
| Expression |
1 | | nqprlu 7498 |
. . . . . 6
⊢ (𝐴 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈
P) |
2 | | nqprlu 7498 |
. . . . . 6
⊢ (𝐵 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈
P) |
3 | | df-iplp 7419 |
. . . . . . 7
⊢
+P = (𝑥 ∈ P, 𝑦 ∈ P ↦ 〈{𝑓 ∈ Q ∣
∃𝑔 ∈
Q ∃ℎ
∈ Q (𝑔
∈ (1st ‘𝑥) ∧ ℎ ∈ (1st ‘𝑦) ∧ 𝑓 = (𝑔 +Q ℎ))}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ Q
∃ℎ ∈
Q (𝑔 ∈
(2nd ‘𝑥)
∧ ℎ ∈
(2nd ‘𝑦)
∧ 𝑓 = (𝑔 +Q
ℎ))}〉) |
4 | | addclnq 7326 |
. . . . . . 7
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
5 | 3, 4 | genpelvl 7463 |
. . . . . 6
⊢
((〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈ P
∧ 〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈ P)
→ (𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ↔ ∃𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)∃𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)𝑟 = (𝑠 +Q 𝑡))) |
6 | 1, 2, 5 | syl2an 287 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ↔ ∃𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)∃𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)𝑟 = (𝑠 +Q 𝑡))) |
7 | 6 | biimpa 294 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → ∃𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)∃𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)𝑟 = (𝑠 +Q 𝑡)) |
8 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑠 ∈ V |
9 | | breq1 3990 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑠 → (𝑙 <Q 𝐴 ↔ 𝑠 <Q 𝐴)) |
10 | | ltnqex 7500 |
. . . . . . . . . . . . . 14
⊢ {𝑙 ∣ 𝑙 <Q 𝐴} ∈ V |
11 | | gtnqex 7501 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∣ 𝐴 <Q 𝑢} ∈ V |
12 | 10, 11 | op1st 6123 |
. . . . . . . . . . . . 13
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) = {𝑙 ∣ 𝑙 <Q 𝐴} |
13 | 8, 9, 12 | elab2 2878 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ↔ 𝑠 <Q
𝐴) |
14 | 13 | biimpi 119 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) → 𝑠 <Q
𝐴) |
15 | 14 | ad2antrl 487 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → 𝑠 <Q
𝐴) |
16 | 15 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑠 <Q 𝐴) |
17 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑡 ∈ V |
18 | | breq1 3990 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑡 → (𝑙 <Q 𝐵 ↔ 𝑡 <Q 𝐵)) |
19 | | ltnqex 7500 |
. . . . . . . . . . . . . 14
⊢ {𝑙 ∣ 𝑙 <Q 𝐵} ∈ V |
20 | | gtnqex 7501 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∣ 𝐵 <Q 𝑢} ∈ V |
21 | 19, 20 | op1st 6123 |
. . . . . . . . . . . . 13
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) = {𝑙 ∣ 𝑙 <Q 𝐵} |
22 | 17, 18, 21 | elab2 2878 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ↔ 𝑡 <Q
𝐵) |
23 | 22 | biimpi 119 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) → 𝑡 <Q
𝐵) |
24 | 23 | ad2antll 488 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → 𝑡 <Q
𝐵) |
25 | 24 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑡 <Q 𝐵) |
26 | | ltrelnq 7316 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
27 | 26 | brel 4661 |
. . . . . . . . . . 11
⊢ (𝑠 <Q
𝐴 → (𝑠 ∈ Q ∧
𝐴 ∈
Q)) |
28 | 16, 27 | syl 14 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑠 ∈ Q ∧ 𝐴 ∈
Q)) |
29 | 26 | brel 4661 |
. . . . . . . . . . 11
⊢ (𝑡 <Q
𝐵 → (𝑡 ∈ Q ∧
𝐵 ∈
Q)) |
30 | 25, 29 | syl 14 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑡 ∈ Q ∧ 𝐵 ∈
Q)) |
31 | | lt2addnq 7355 |
. . . . . . . . . 10
⊢ (((𝑠 ∈ Q ∧
𝐴 ∈ Q)
∧ (𝑡 ∈
Q ∧ 𝐵
∈ Q)) → ((𝑠 <Q 𝐴 ∧ 𝑡 <Q 𝐵) → (𝑠 +Q 𝑡) <Q
(𝐴
+Q 𝐵))) |
32 | 28, 30, 31 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → ((𝑠 <Q 𝐴 ∧ 𝑡 <Q 𝐵) → (𝑠 +Q 𝑡) <Q
(𝐴
+Q 𝐵))) |
33 | 16, 25, 32 | mp2and 431 |
. . . . . . . 8
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑠 +Q 𝑡) <Q
(𝐴
+Q 𝐵)) |
34 | | breq1 3990 |
. . . . . . . . 9
⊢ (𝑟 = (𝑠 +Q 𝑡) → (𝑟 <Q (𝐴 +Q
𝐵) ↔ (𝑠 +Q
𝑡)
<Q (𝐴 +Q 𝐵))) |
35 | 34 | adantl 275 |
. . . . . . . 8
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑟 <Q (𝐴 +Q
𝐵) ↔ (𝑠 +Q
𝑡)
<Q (𝐴 +Q 𝐵))) |
36 | 33, 35 | mpbird 166 |
. . . . . . 7
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑟 <Q (𝐴 +Q
𝐵)) |
37 | | vex 2733 |
. . . . . . . 8
⊢ 𝑟 ∈ V |
38 | | breq1 3990 |
. . . . . . . 8
⊢ (𝑙 = 𝑟 → (𝑙 <Q (𝐴 +Q
𝐵) ↔ 𝑟 <Q
(𝐴
+Q 𝐵))) |
39 | | ltnqex 7500 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} ∈
V |
40 | | gtnqex 7501 |
. . . . . . . . 9
⊢ {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢} ∈
V |
41 | 39, 40 | op1st 6123 |
. . . . . . . 8
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) = {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} |
42 | 37, 38, 41 | elab2 2878 |
. . . . . . 7
⊢ (𝑟 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉) ↔ 𝑟 <Q
(𝐴
+Q 𝐵)) |
43 | 36, 42 | sylibr 133 |
. . . . . 6
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑟 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉)) |
44 | 43 | ex 114 |
. . . . 5
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → (𝑟 = (𝑠 +Q 𝑡) → 𝑟 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉))) |
45 | 44 | rexlimdvva 2595 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → (∃𝑠 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)∃𝑡 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)𝑟 = (𝑠 +Q 𝑡) → 𝑟 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉))) |
46 | 7, 45 | mpd 13 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → 𝑟 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉)) |
47 | 46 | ex 114 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) → 𝑟 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉))) |
48 | 47 | ssrdv 3153 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
+P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(1st ‘〈{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}〉)) |