Step | Hyp | Ref
| Expression |
1 | | ltrelpr 7440 |
. . . . . 6
⊢
<P ⊆ (P ×
P) |
2 | 1 | brel 4653 |
. . . . 5
⊢ (𝐴<P
𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
3 | 2 | simpld 111 |
. . . 4
⊢ (𝐴<P
𝐵 → 𝐴 ∈ P) |
4 | | ltexprlem.1 |
. . . . 5
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd
‘𝐵))}〉 |
5 | 4 | ltexprlempr 7543 |
. . . 4
⊢ (𝐴<P
𝐵 → 𝐶 ∈ P) |
6 | | df-iplp 7403 |
. . . . 5
⊢
+P = (𝑧 ∈ P, 𝑦 ∈ P ↦ 〈{𝑓 ∈ Q ∣
∃𝑔 ∈
Q ∃ℎ
∈ Q (𝑔
∈ (1st ‘𝑧) ∧ ℎ ∈ (1st ‘𝑦) ∧ 𝑓 = (𝑔 +Q ℎ))}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ Q
∃ℎ ∈
Q (𝑔 ∈
(2nd ‘𝑧)
∧ ℎ ∈
(2nd ‘𝑦)
∧ 𝑓 = (𝑔 +Q
ℎ))}〉) |
7 | | addclnq 7310 |
. . . . 5
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
8 | 6, 7 | genpelvl 7447 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝑧 ∈
(1st ‘(𝐴
+P 𝐶)) ↔ ∃𝑤 ∈ (1st ‘𝐴)∃𝑢 ∈ (1st ‘𝐶)𝑧 = (𝑤 +Q 𝑢))) |
9 | 3, 5, 8 | syl2anc 409 |
. . 3
⊢ (𝐴<P
𝐵 → (𝑧 ∈ (1st
‘(𝐴
+P 𝐶)) ↔ ∃𝑤 ∈ (1st ‘𝐴)∃𝑢 ∈ (1st ‘𝐶)𝑧 = (𝑤 +Q 𝑢))) |
10 | | simprr 522 |
. . . . . 6
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → 𝑧 = (𝑤 +Q 𝑢)) |
11 | 4 | ltexprlemell 7533 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (1st
‘𝐶) ↔ (𝑢 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵)))) |
12 | 11 | biimpi 119 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (1st
‘𝐶) → (𝑢 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵)))) |
13 | 12 | ad2antlr 481 |
. . . . . . . . 9
⊢ (((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) → (𝑢 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵)))) |
14 | 13 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → (𝑢 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵)))) |
15 | 14 | simprd 113 |
. . . . . . 7
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) |
16 | | prop 7410 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
17 | 3, 16 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
18 | | prltlu 7422 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑤 ∈ (1st
‘𝐴) ∧ 𝑦 ∈ (2nd
‘𝐴)) → 𝑤 <Q
𝑦) |
19 | 17, 18 | syl3an1 1260 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ 𝑤 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴)) → 𝑤 <Q 𝑦) |
20 | 19 | 3adant2r 1222 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ (𝑤 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (1st ‘𝐶)) ∧ 𝑦 ∈ (2nd ‘𝐴)) → 𝑤 <Q 𝑦) |
21 | 20 | 3adant2r 1222 |
. . . . . . . . . 10
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ 𝑦 ∈ (2nd ‘𝐴)) → 𝑤 <Q 𝑦) |
22 | 21 | 3adant3r 1224 |
. . . . . . . . 9
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → 𝑤 <Q
𝑦) |
23 | | ltanqg 7335 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → (𝑓
<Q 𝑔 ↔ (ℎ +Q 𝑓) <Q
(ℎ
+Q 𝑔))) |
24 | 23 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) ∧ (𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q)) → (𝑓
<Q 𝑔 ↔ (ℎ +Q 𝑓) <Q
(ℎ
+Q 𝑔))) |
25 | | ltrelnq 7300 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
26 | 25 | brel 4653 |
. . . . . . . . . . . . 13
⊢ (𝑤 <Q
𝑦 → (𝑤 ∈ Q ∧
𝑦 ∈
Q)) |
27 | 22, 26 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → (𝑤 ∈ Q ∧
𝑦 ∈
Q)) |
28 | 27 | simpld 111 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → 𝑤 ∈
Q) |
29 | 27 | simprd 113 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → 𝑦 ∈
Q) |
30 | | prop 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ P →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P) |
31 | 5, 30 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈
P) |
32 | | elprnql 7416 |
. . . . . . . . . . . . . . 15
⊢
((〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈ P ∧ 𝑢 ∈ (1st
‘𝐶)) → 𝑢 ∈
Q) |
33 | 31, 32 | sylan 281 |
. . . . . . . . . . . . . 14
⊢ ((𝐴<P
𝐵 ∧ 𝑢 ∈ (1st ‘𝐶)) → 𝑢 ∈ Q) |
34 | 33 | adantrl 470 |
. . . . . . . . . . . . 13
⊢ ((𝐴<P
𝐵 ∧ (𝑤 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (1st ‘𝐶))) → 𝑢 ∈ Q) |
35 | 34 | adantrr 471 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → 𝑢 ∈ Q) |
36 | 35 | 3adant3 1006 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → 𝑢 ∈
Q) |
37 | | addcomnqg 7316 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
38 | 37 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) ∧ (𝑓 ∈ Q ∧
𝑔 ∈ Q))
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
39 | 24, 28, 29, 36, 38 | caovord2d 6005 |
. . . . . . . . . 10
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → (𝑤 <Q
𝑦 ↔ (𝑤 +Q
𝑢)
<Q (𝑦 +Q 𝑢))) |
40 | 2 | simprd 113 |
. . . . . . . . . . . . . 14
⊢ (𝐴<P
𝐵 → 𝐵 ∈ P) |
41 | | prop 7410 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
42 | 40, 41 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
43 | | prcdnql 7419 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ (𝑦 +Q
𝑢) ∈ (1st
‘𝐵)) → ((𝑤 +Q
𝑢)
<Q (𝑦 +Q 𝑢) → (𝑤 +Q 𝑢) ∈ (1st
‘𝐵))) |
44 | 42, 43 | sylan 281 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵)) → ((𝑤 +Q
𝑢)
<Q (𝑦 +Q 𝑢) → (𝑤 +Q 𝑢) ∈ (1st
‘𝐵))) |
45 | 44 | adantrl 470 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → ((𝑤 +Q
𝑢)
<Q (𝑦 +Q 𝑢) → (𝑤 +Q 𝑢) ∈ (1st
‘𝐵))) |
46 | 45 | 3adant2 1005 |
. . . . . . . . . 10
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → ((𝑤 +Q
𝑢)
<Q (𝑦 +Q 𝑢) → (𝑤 +Q 𝑢) ∈ (1st
‘𝐵))) |
47 | 39, 46 | sylbid 149 |
. . . . . . . . 9
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → (𝑤 <Q
𝑦 → (𝑤 +Q
𝑢) ∈ (1st
‘𝐵))) |
48 | 22, 47 | mpd 13 |
. . . . . . . 8
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → (𝑤 +Q
𝑢) ∈ (1st
‘𝐵)) |
49 | 48 | 3expa 1192 |
. . . . . . 7
⊢ (((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑢) ∈ (1st
‘𝐵))) → (𝑤 +Q
𝑢) ∈ (1st
‘𝐵)) |
50 | 15, 49 | exlimddv 1885 |
. . . . . 6
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → (𝑤 +Q 𝑢) ∈ (1st
‘𝐵)) |
51 | 10, 50 | eqeltrd 2241 |
. . . . 5
⊢ ((𝐴<P
𝐵 ∧ ((𝑤 ∈ (1st
‘𝐴) ∧ 𝑢 ∈ (1st
‘𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → 𝑧 ∈ (1st ‘𝐵)) |
52 | 51 | expr 373 |
. . . 4
⊢ ((𝐴<P
𝐵 ∧ (𝑤 ∈ (1st ‘𝐴) ∧ 𝑢 ∈ (1st ‘𝐶))) → (𝑧 = (𝑤 +Q 𝑢) → 𝑧 ∈ (1st ‘𝐵))) |
53 | 52 | rexlimdvva 2589 |
. . 3
⊢ (𝐴<P
𝐵 → (∃𝑤 ∈ (1st
‘𝐴)∃𝑢 ∈ (1st
‘𝐶)𝑧 = (𝑤 +Q 𝑢) → 𝑧 ∈ (1st ‘𝐵))) |
54 | 9, 53 | sylbid 149 |
. 2
⊢ (𝐴<P
𝐵 → (𝑧 ∈ (1st
‘(𝐴
+P 𝐶)) → 𝑧 ∈ (1st ‘𝐵))) |
55 | 54 | ssrdv 3146 |
1
⊢ (𝐴<P
𝐵 → (1st
‘(𝐴
+P 𝐶)) ⊆ (1st ‘𝐵)) |