Step | Hyp | Ref
| Expression |
1 | | addnqprlemrl 7556 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (1st ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩)) ⊆
(1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) |
2 | | ltsonq 7397 |
. . . . . . . . 9
⊢
<Q Or Q |
3 | | addclnq 7374 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
+Q 𝐵) ∈ Q) |
4 | | sonr 4318 |
. . . . . . . . 9
⊢ ((
<Q Or Q ∧ (𝐴 +Q 𝐵) ∈ Q) →
¬ (𝐴
+Q 𝐵) <Q (𝐴 +Q
𝐵)) |
5 | 2, 3, 4 | sylancr 414 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) <Q (𝐴 +Q
𝐵)) |
6 | | ltrelnq 7364 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
7 | 6 | brel 4679 |
. . . . . . . . . . 11
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → ((𝐴 +Q 𝐵) ∈ Q ∧
(𝐴
+Q 𝐵) ∈ Q)) |
8 | 7 | simpld 112 |
. . . . . . . . . 10
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → (𝐴 +Q 𝐵) ∈
Q) |
9 | | elex 2749 |
. . . . . . . . . 10
⊢ ((𝐴 +Q
𝐵) ∈ Q
→ (𝐴
+Q 𝐵) ∈ V) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵) → (𝐴 +Q 𝐵) ∈ V) |
11 | | breq1 4007 |
. . . . . . . . 9
⊢ (𝑙 = (𝐴 +Q 𝐵) → (𝑙 <Q (𝐴 +Q
𝐵) ↔ (𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵))) |
12 | 10, 11 | elab3 2890 |
. . . . . . . 8
⊢ ((𝐴 +Q
𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} ↔ (𝐴 +Q
𝐵)
<Q (𝐴 +Q 𝐵)) |
13 | 5, 12 | sylnibr 677 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}) |
14 | | ltnqex 7548 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} ∈
V |
15 | | gtnqex 7549 |
. . . . . . . . 9
⊢ {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢} ∈
V |
16 | 14, 15 | op1st 6147 |
. . . . . . . 8
⊢
(1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)} |
17 | 16 | eleq2i 2244 |
. . . . . . 7
⊢ ((𝐴 +Q
𝐵) ∈ (1st
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) ↔ (𝐴 +Q
𝐵) ∈ {𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}) |
18 | 13, 17 | sylnibr 677 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ ¬ (𝐴
+Q 𝐵) ∈ (1st ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩)) |
19 | 1, 18 | ssneldd 3159 |
. . . . 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 7546 |
. . . . . . . 8
⊢ (𝐴 ∈ Q →
⟨{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈
P) |
22 | | nqprlu 7546 |
. . . . . . . 8
⊢ (𝐵 ∈ Q →
⟨{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩ ∈
P) |
23 | | addclpr 7536 |
. . . . . . . 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 7474 |
. . . . . . 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 2741 |
. . . . . . . 8
⊢ 𝑟 ∈ V |
28 | | breq2 4008 |
. . . . . . . 8
⊢ (𝑢 = 𝑟 → ((𝐴 +Q 𝐵) <Q
𝑢 ↔ (𝐴 +Q 𝐵) <Q
𝑟)) |
29 | 14, 15 | op2nd 6148 |
. . . . . . . 8
⊢
(2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) = {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢} |
30 | 27, 28, 29 | elab2 2886 |
. . . . . . 7
⊢ (𝑟 ∈ (2nd
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) ↔ (𝐴 +Q
𝐵)
<Q 𝑟) |
31 | 30 | biimpi 120 |
. . . . . 6
⊢ (𝑟 ∈ (2nd
‘⟨{𝑙 ∣
𝑙
<Q (𝐴 +Q 𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) → (𝐴 +Q
𝐵)
<Q 𝑟) |
32 | | prloc 7490 |
. . . . . 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 729 |
. . . 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 1349 |
. . 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 3162 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘⟨{𝑙 ∣ 𝑙 <Q (𝐴 +Q
𝐵)}, {𝑢 ∣ (𝐴 +Q 𝐵) <Q
𝑢}⟩) ⊆
(2nd ‘(⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩
+P ⟨{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}⟩))) |