Step | Hyp | Ref
| Expression |
1 | | nqprlu 6530 |
. . . . . 6
⊢ (A ∈
Q → 〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 ∈
P) |
2 | | nqprlu 6530 |
. . . . . 6
⊢ (B ∈
Q → 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉 ∈
P) |
3 | | df-iplp 6451 |
. . . . . . 7
⊢
+P = (x ∈ P, y ∈
P ↦ 〈{f ∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(1st ‘x) ∧ ℎ
∈ (1st ‘y) ∧ f = (g
+Q ℎ))}, {f
∈ Q ∣ ∃g ∈ Q ∃ℎ
∈ Q (g ∈
(2nd ‘x) ∧ ℎ
∈ (2nd ‘y) ∧ f = (g
+Q ℎ))}〉) |
4 | | addclnq 6359 |
. . . . . . 7
⊢
((g ∈ Q ∧ ℎ
∈ Q) → (g +Q ℎ) ∈
Q) |
5 | 3, 4 | genpelvl 6495 |
. . . . . 6
⊢
((〈{𝑙 ∣
𝑙
<Q A},
{u ∣ A <Q u}〉 ∈
P ∧ 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉 ∈
P) → (𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉)) ↔ ∃𝑠 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉)∃𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉)𝑟 = (𝑠 +Q 𝑡))) |
6 | 1, 2, 5 | syl2an 273 |
. . . . 5
⊢
((A ∈ Q ∧ B ∈ Q) → (𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉)) ↔ ∃𝑠 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉)∃𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉)𝑟 = (𝑠 +Q 𝑡))) |
7 | 6 | biimpa 280 |
. . . 4
⊢
(((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) → ∃𝑠 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉)∃𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉)𝑟 = (𝑠 +Q 𝑡)) |
8 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ 𝑠 ∈ V |
9 | | breq1 3758 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑠 → (𝑙 <Q A ↔ 𝑠 <Q A)) |
10 | | ltnqex 6531 |
. . . . . . . . . . . . . 14
⊢ {𝑙 ∣ 𝑙 <Q A} ∈
V |
11 | | gtnqex 6532 |
. . . . . . . . . . . . . 14
⊢ {u ∣ A
<Q u} ∈ V |
12 | 10, 11 | op1st 5715 |
. . . . . . . . . . . . 13
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) = {𝑙 ∣ 𝑙 <Q A} |
13 | 8, 9, 12 | elab2 2684 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ↔ 𝑠 <Q A) |
14 | 13 | biimpi 113 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) → 𝑠 <Q A) |
15 | 14 | ad2antrl 459 |
. . . . . . . . . 10
⊢
((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) → 𝑠 <Q A) |
16 | 15 | adantr 261 |
. . . . . . . . 9
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑠 <Q A) |
17 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ 𝑡 ∈ V |
18 | | breq1 3758 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑡 → (𝑙 <Q B ↔ 𝑡 <Q B)) |
19 | | ltnqex 6531 |
. . . . . . . . . . . . . 14
⊢ {𝑙 ∣ 𝑙 <Q B} ∈
V |
20 | | gtnqex 6532 |
. . . . . . . . . . . . . 14
⊢ {u ∣ B
<Q u} ∈ V |
21 | 19, 20 | op1st 5715 |
. . . . . . . . . . . . 13
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉) = {𝑙 ∣ 𝑙 <Q B} |
22 | 17, 18, 21 | elab2 2684 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉) ↔ 𝑡 <Q B) |
23 | 22 | biimpi 113 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉) → 𝑡 <Q B) |
24 | 23 | ad2antll 460 |
. . . . . . . . . 10
⊢
((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) → 𝑡 <Q B) |
25 | 24 | adantr 261 |
. . . . . . . . 9
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑡 <Q B) |
26 | | ltrelnq 6349 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
27 | 26 | brel 4335 |
. . . . . . . . . . 11
⊢ (𝑠 <Q
A → (𝑠 ∈
Q ∧ A ∈
Q)) |
28 | 16, 27 | syl 14 |
. . . . . . . . . 10
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑠 ∈
Q ∧ A ∈
Q)) |
29 | 26 | brel 4335 |
. . . . . . . . . . 11
⊢ (𝑡 <Q
B → (𝑡 ∈
Q ∧ B ∈
Q)) |
30 | 25, 29 | syl 14 |
. . . . . . . . . 10
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑡 ∈
Q ∧ B ∈
Q)) |
31 | | lt2addnq 6388 |
. . . . . . . . . 10
⊢ (((𝑠 ∈ Q ∧ A ∈ Q) ∧ (𝑡 ∈
Q ∧ B ∈
Q)) → ((𝑠
<Q A ∧ 𝑡
<Q B) →
(𝑠 +Q
𝑡)
<Q (A
+Q B))) |
32 | 28, 30, 31 | syl2anc 391 |
. . . . . . . . 9
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → ((𝑠 <Q A ∧ 𝑡 <Q B) → (𝑠 +Q 𝑡) <Q (A +Q B))) |
33 | 16, 25, 32 | mp2and 409 |
. . . . . . . 8
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑠 +Q 𝑡) <Q (A +Q B)) |
34 | | breq1 3758 |
. . . . . . . . 9
⊢ (𝑟 = (𝑠 +Q 𝑡) → (𝑟 <Q (A +Q B) ↔ (𝑠 +Q 𝑡) <Q (A +Q B))) |
35 | 34 | adantl 262 |
. . . . . . . 8
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → (𝑟 <Q (A +Q B) ↔ (𝑠 +Q 𝑡) <Q (A +Q B))) |
36 | 33, 35 | mpbird 156 |
. . . . . . 7
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑟 <Q (A +Q B)) |
37 | | vex 2554 |
. . . . . . . 8
⊢ 𝑟 ∈ V |
38 | | breq1 3758 |
. . . . . . . 8
⊢ (𝑙 = 𝑟 → (𝑙 <Q (A +Q B) ↔ 𝑟 <Q (A +Q B))) |
39 | | ltnqex 6531 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q (A +Q B)} ∈
V |
40 | | gtnqex 6532 |
. . . . . . . . 9
⊢ {u ∣ (A
+Q B)
<Q u} ∈ V |
41 | 39, 40 | op1st 5715 |
. . . . . . . 8
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣
(A +Q B) <Q u}〉) = {𝑙 ∣ 𝑙 <Q (A +Q B)} |
42 | 37, 38, 41 | elab2 2684 |
. . . . . . 7
⊢ (𝑟 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣
(A +Q B) <Q u}〉) ↔ 𝑟 <Q (A +Q B)) |
43 | 36, 42 | sylibr 137 |
. . . . . 6
⊢
(((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧ 𝑟 = (𝑠 +Q 𝑡)) → 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣
(A +Q B) <Q u}〉)) |
44 | 43 | ex 108 |
. . . . 5
⊢
((((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) ∧
(𝑠 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉) ∧ 𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) → (𝑟 = (𝑠 +Q 𝑡) → 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣
(A +Q B) <Q u}〉))) |
45 | 44 | rexlimdvva 2434 |
. . . 4
⊢
(((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) → (∃𝑠 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉)∃𝑡 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉)𝑟 = (𝑠 +Q 𝑡) → 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣
(A +Q B) <Q u}〉))) |
46 | 7, 45 | mpd 13 |
. . 3
⊢
(((A ∈ Q ∧ B ∈ Q) ∧ 𝑟
∈ (1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉))) → 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣
(A +Q B) <Q u}〉)) |
47 | 46 | ex 108 |
. 2
⊢
((A ∈ Q ∧ B ∈ Q) → (𝑟 ∈
(1st ‘(〈{𝑙 ∣ 𝑙 <Q A}, {u ∣
A <Q u}〉 +P 〈{𝑙 ∣ 𝑙 <Q B}, {u ∣
B <Q u}〉)) → 𝑟 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q (A +Q B)}, {u ∣
(A +Q B) <Q u}〉))) |
48 | 47 | ssrdv 2945 |
1
⊢
((A ∈ Q ∧ B ∈ Q) → (1st
‘(〈{𝑙 ∣ 𝑙 <Q
A}, {u
∣ A <Q
u}〉 +P
〈{𝑙 ∣ 𝑙 <Q
B}, {u
∣ B <Q
u}〉)) ⊆ (1st
‘〈{𝑙 ∣ 𝑙 <Q
(A +Q B)}, {u ∣
(A +Q B) <Q u}〉)) |