Step | Hyp | Ref
| Expression |
1 | | ltrelpr 7456 |
. . . . . . . . 9
⊢
<P ⊆ (P ×
P) |
2 | 1 | brel 4661 |
. . . . . . . 8
⊢ (𝐴<P
𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
3 | | ltdfpr 7457 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴<P 𝐵 ↔ ∃𝑦 ∈ Q (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (1st
‘𝐵)))) |
4 | 3 | biimpd 143 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴<P 𝐵 → ∃𝑦 ∈ Q (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (1st
‘𝐵)))) |
5 | 2, 4 | mpcom 36 |
. . . . . . 7
⊢ (𝐴<P
𝐵 → ∃𝑦 ∈ Q (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (1st
‘𝐵))) |
6 | | simprrl 534 |
. . . . . . . . . 10
⊢ ((𝐴<P
𝐵 ∧ (𝑦 ∈ Q ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (1st
‘𝐵)))) → 𝑦 ∈ (2nd
‘𝐴)) |
7 | 2 | simprd 113 |
. . . . . . . . . . . . 13
⊢ (𝐴<P
𝐵 → 𝐵 ∈ P) |
8 | | prop 7426 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
9 | | prnmaxl 7439 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑦 ∈ (1st
‘𝐵)) →
∃𝑤 ∈
(1st ‘𝐵)𝑦 <Q 𝑤) |
10 | 8, 9 | sylan 281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ P ∧
𝑦 ∈ (1st
‘𝐵)) →
∃𝑤 ∈
(1st ‘𝐵)𝑦 <Q 𝑤) |
11 | | ltexnqi 7360 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 <Q
𝑤 → ∃𝑞 ∈ Q (𝑦 +Q
𝑞) = 𝑤) |
12 | 11 | reximi 2567 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑤 ∈
(1st ‘𝐵)𝑦 <Q 𝑤 → ∃𝑤 ∈ (1st
‘𝐵)∃𝑞 ∈ Q (𝑦 +Q
𝑞) = 𝑤) |
13 | 10, 12 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ P ∧
𝑦 ∈ (1st
‘𝐵)) →
∃𝑤 ∈
(1st ‘𝐵)∃𝑞 ∈ Q (𝑦 +Q 𝑞) = 𝑤) |
14 | | df-rex 2454 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑤 ∈
(1st ‘𝐵)∃𝑞 ∈ Q (𝑦 +Q 𝑞) = 𝑤 ↔ ∃𝑤(𝑤 ∈ (1st ‘𝐵) ∧ ∃𝑞 ∈ Q (𝑦 +Q
𝑞) = 𝑤)) |
15 | 13, 14 | sylib 121 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ P ∧
𝑦 ∈ (1st
‘𝐵)) →
∃𝑤(𝑤 ∈ (1st ‘𝐵) ∧ ∃𝑞 ∈ Q (𝑦 +Q
𝑞) = 𝑤)) |
16 | | r19.42v 2627 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑞 ∈
Q (𝑤 ∈
(1st ‘𝐵)
∧ (𝑦
+Q 𝑞) = 𝑤) ↔ (𝑤 ∈ (1st ‘𝐵) ∧ ∃𝑞 ∈ Q (𝑦 +Q
𝑞) = 𝑤)) |
17 | 16 | exbii 1598 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑤∃𝑞 ∈ Q (𝑤 ∈ (1st ‘𝐵) ∧ (𝑦 +Q 𝑞) = 𝑤) ↔ ∃𝑤(𝑤 ∈ (1st ‘𝐵) ∧ ∃𝑞 ∈ Q (𝑦 +Q
𝑞) = 𝑤)) |
18 | 15, 17 | sylibr 133 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ P ∧
𝑦 ∈ (1st
‘𝐵)) →
∃𝑤∃𝑞 ∈ Q (𝑤 ∈ (1st
‘𝐵) ∧ (𝑦 +Q
𝑞) = 𝑤)) |
19 | | eleq1 2233 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 +Q
𝑞) = 𝑤 → ((𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ↔ 𝑤 ∈ (1st
‘𝐵))) |
20 | 19 | biimparc 297 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ (1st
‘𝐵) ∧ (𝑦 +Q
𝑞) = 𝑤) → (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) |
21 | 20 | reximi 2567 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑞 ∈
Q (𝑤 ∈
(1st ‘𝐵)
∧ (𝑦
+Q 𝑞) = 𝑤) → ∃𝑞 ∈ Q (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) |
22 | 21 | exlimiv 1591 |
. . . . . . . . . . . . . 14
⊢
(∃𝑤∃𝑞 ∈ Q (𝑤 ∈ (1st ‘𝐵) ∧ (𝑦 +Q 𝑞) = 𝑤) → ∃𝑞 ∈ Q (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) |
23 | 18, 22 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ P ∧
𝑦 ∈ (1st
‘𝐵)) →
∃𝑞 ∈
Q (𝑦
+Q 𝑞) ∈ (1st ‘𝐵)) |
24 | 7, 23 | sylan 281 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ 𝑦 ∈ (1st ‘𝐵)) → ∃𝑞 ∈ Q (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) |
25 | 24 | adantrl 475 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ 𝑦 ∈ (1st ‘𝐵))) → ∃𝑞 ∈ Q (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) |
26 | 25 | adantrl 475 |
. . . . . . . . . 10
⊢ ((𝐴<P
𝐵 ∧ (𝑦 ∈ Q ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (1st
‘𝐵)))) →
∃𝑞 ∈
Q (𝑦
+Q 𝑞) ∈ (1st ‘𝐵)) |
27 | 6, 26 | jca 304 |
. . . . . . . . 9
⊢ ((𝐴<P
𝐵 ∧ (𝑦 ∈ Q ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (1st
‘𝐵)))) → (𝑦 ∈ (2nd
‘𝐴) ∧
∃𝑞 ∈
Q (𝑦
+Q 𝑞) ∈ (1st ‘𝐵))) |
28 | 27 | expr 373 |
. . . . . . . 8
⊢ ((𝐴<P
𝐵 ∧ 𝑦 ∈ Q) → ((𝑦 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (1st
‘𝐵)) → (𝑦 ∈ (2nd
‘𝐴) ∧
∃𝑞 ∈
Q (𝑦
+Q 𝑞) ∈ (1st ‘𝐵)))) |
29 | 28 | reximdva 2572 |
. . . . . . 7
⊢ (𝐴<P
𝐵 → (∃𝑦 ∈ Q (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑦 ∈ (1st
‘𝐵)) →
∃𝑦 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ ∃𝑞 ∈
Q (𝑦
+Q 𝑞) ∈ (1st ‘𝐵)))) |
30 | 5, 29 | mpd 13 |
. . . . . 6
⊢ (𝐴<P
𝐵 → ∃𝑦 ∈ Q (𝑦 ∈ (2nd
‘𝐴) ∧
∃𝑞 ∈
Q (𝑦
+Q 𝑞) ∈ (1st ‘𝐵))) |
31 | | r19.42v 2627 |
. . . . . . 7
⊢
(∃𝑞 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ (𝑦
+Q 𝑞) ∈ (1st ‘𝐵)) ↔ (𝑦 ∈ (2nd ‘𝐴) ∧ ∃𝑞 ∈ Q (𝑦 +Q
𝑞) ∈ (1st
‘𝐵))) |
32 | 31 | rexbii 2477 |
. . . . . 6
⊢
(∃𝑦 ∈
Q ∃𝑞
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ↔
∃𝑦 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ ∃𝑞 ∈
Q (𝑦
+Q 𝑞) ∈ (1st ‘𝐵))) |
33 | 30, 32 | sylibr 133 |
. . . . 5
⊢ (𝐴<P
𝐵 → ∃𝑦 ∈ Q
∃𝑞 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ (𝑦
+Q 𝑞) ∈ (1st ‘𝐵))) |
34 | | rexcom 2634 |
. . . . 5
⊢
(∃𝑦 ∈
Q ∃𝑞
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ↔
∃𝑞 ∈
Q ∃𝑦
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) |
35 | 33, 34 | sylib 121 |
. . . 4
⊢ (𝐴<P
𝐵 → ∃𝑞 ∈ Q
∃𝑦 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ (𝑦
+Q 𝑞) ∈ (1st ‘𝐵))) |
36 | 2 | simpld 111 |
. . . . . . . . . . . 12
⊢ (𝐴<P
𝐵 → 𝐴 ∈ P) |
37 | | prop 7426 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
38 | | elprnqu 7433 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑦 ∈ (2nd
‘𝐴)) → 𝑦 ∈
Q) |
39 | 37, 38 | sylan 281 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
𝑦 ∈ (2nd
‘𝐴)) → 𝑦 ∈
Q) |
40 | 36, 39 | sylan 281 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ 𝑦 ∈ (2nd ‘𝐴)) → 𝑦 ∈ Q) |
41 | 40 | ex 114 |
. . . . . . . . . 10
⊢ (𝐴<P
𝐵 → (𝑦 ∈ (2nd
‘𝐴) → 𝑦 ∈
Q)) |
42 | 41 | pm4.71rd 392 |
. . . . . . . . 9
⊢ (𝐴<P
𝐵 → (𝑦 ∈ (2nd
‘𝐴) ↔ (𝑦 ∈ Q ∧
𝑦 ∈ (2nd
‘𝐴)))) |
43 | 42 | anbi1d 462 |
. . . . . . . 8
⊢ (𝐴<P
𝐵 → ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ↔ ((𝑦 ∈ Q ∧
𝑦 ∈ (2nd
‘𝐴)) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)))) |
44 | | anass 399 |
. . . . . . . 8
⊢ (((𝑦 ∈ Q ∧
𝑦 ∈ (2nd
‘𝐴)) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ↔ (𝑦 ∈ Q ∧
(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)))) |
45 | 43, 44 | bitrdi 195 |
. . . . . . 7
⊢ (𝐴<P
𝐵 → ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ↔ (𝑦 ∈ Q ∧
(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵))))) |
46 | 45 | exbidv 1818 |
. . . . . 6
⊢ (𝐴<P
𝐵 → (∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ↔
∃𝑦(𝑦 ∈ Q ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵))))) |
47 | 46 | rexbidv 2471 |
. . . . 5
⊢ (𝐴<P
𝐵 → (∃𝑞 ∈ Q
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ↔
∃𝑞 ∈
Q ∃𝑦(𝑦 ∈ Q ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵))))) |
48 | | df-rex 2454 |
. . . . . 6
⊢
(∃𝑦 ∈
Q (𝑦 ∈
(2nd ‘𝐴)
∧ (𝑦
+Q 𝑞) ∈ (1st ‘𝐵)) ↔ ∃𝑦(𝑦 ∈ Q ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)))) |
49 | 48 | rexbii 2477 |
. . . . 5
⊢
(∃𝑞 ∈
Q ∃𝑦
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ↔
∃𝑞 ∈
Q ∃𝑦(𝑦 ∈ Q ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)))) |
50 | 47, 49 | bitr4di 197 |
. . . 4
⊢ (𝐴<P
𝐵 → (∃𝑞 ∈ Q
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ↔
∃𝑞 ∈
Q ∃𝑦
∈ Q (𝑦
∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)))) |
51 | 35, 50 | mpbird 166 |
. . 3
⊢ (𝐴<P
𝐵 → ∃𝑞 ∈ Q
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) |
52 | | ltexprlem.1 |
. . . . . 6
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd
‘𝐵))}〉 |
53 | 52 | ltexprlemell 7549 |
. . . . 5
⊢ (𝑞 ∈ (1st
‘𝐶) ↔ (𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)))) |
54 | 53 | rexbii 2477 |
. . . 4
⊢
(∃𝑞 ∈
Q 𝑞 ∈
(1st ‘𝐶)
↔ ∃𝑞 ∈
Q (𝑞 ∈
Q ∧ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)))) |
55 | | ssid 3167 |
. . . . 5
⊢
Q ⊆ Q |
56 | | rexss 3214 |
. . . . 5
⊢
(Q ⊆ Q → (∃𝑞 ∈ Q
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ↔
∃𝑞 ∈
Q (𝑞 ∈
Q ∧ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))))) |
57 | 55, 56 | ax-mp 5 |
. . . 4
⊢
(∃𝑞 ∈
Q ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ↔
∃𝑞 ∈
Q (𝑞 ∈
Q ∧ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)))) |
58 | 54, 57 | bitr4i 186 |
. . 3
⊢
(∃𝑞 ∈
Q 𝑞 ∈
(1st ‘𝐶)
↔ ∃𝑞 ∈
Q ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) |
59 | 51, 58 | sylibr 133 |
. 2
⊢ (𝐴<P
𝐵 → ∃𝑞 ∈ Q 𝑞 ∈ (1st
‘𝐶)) |
60 | | nfv 1521 |
. . 3
⊢
Ⅎ𝑟 𝐴<P
𝐵 |
61 | | nfre1 2513 |
. . 3
⊢
Ⅎ𝑟∃𝑟 ∈ Q 𝑟 ∈ (2nd
‘𝐶) |
62 | | prmu 7429 |
. . . . 5
⊢
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P →
∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐵)) |
63 | | rexex 2516 |
. . . . 5
⊢
(∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐵)
→ ∃𝑟 𝑟 ∈ (2nd
‘𝐵)) |
64 | 62, 63 | syl 14 |
. . . 4
⊢
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P →
∃𝑟 𝑟 ∈ (2nd ‘𝐵)) |
65 | 7, 8, 64 | 3syl 17 |
. . 3
⊢ (𝐴<P
𝐵 → ∃𝑟 𝑟 ∈ (2nd ‘𝐵)) |
66 | | elprnqu 7433 |
. . . . . . 7
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑟 ∈ (2nd
‘𝐵)) → 𝑟 ∈
Q) |
67 | 8, 66 | sylan 281 |
. . . . . 6
⊢ ((𝐵 ∈ P ∧
𝑟 ∈ (2nd
‘𝐵)) → 𝑟 ∈
Q) |
68 | 7, 67 | sylan 281 |
. . . . 5
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵)) → 𝑟 ∈ Q) |
69 | | prml 7428 |
. . . . . . . . 9
⊢
(〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P →
∃𝑦 ∈
Q 𝑦 ∈
(1st ‘𝐴)) |
70 | 37, 69 | syl 14 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
∃𝑦 ∈
Q 𝑦 ∈
(1st ‘𝐴)) |
71 | | rexex 2516 |
. . . . . . . 8
⊢
(∃𝑦 ∈
Q 𝑦 ∈
(1st ‘𝐴)
→ ∃𝑦 𝑦 ∈ (1st
‘𝐴)) |
72 | 36, 70, 71 | 3syl 17 |
. . . . . . 7
⊢ (𝐴<P
𝐵 → ∃𝑦 𝑦 ∈ (1st ‘𝐴)) |
73 | 72 | adantr 274 |
. . . . . 6
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵)) → ∃𝑦 𝑦 ∈ (1st ‘𝐴)) |
74 | 68 | 3adant3 1012 |
. . . . . . . . 9
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → 𝑟 ∈ Q) |
75 | | simp3 994 |
. . . . . . . . . 10
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → 𝑦 ∈ (1st ‘𝐴)) |
76 | | elprnql 7432 |
. . . . . . . . . . . . . . 15
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑦 ∈ (1st
‘𝐴)) → 𝑦 ∈
Q) |
77 | 37, 76 | sylan 281 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝑦 ∈ (1st
‘𝐴)) → 𝑦 ∈
Q) |
78 | 36, 77 | sylan 281 |
. . . . . . . . . . . . 13
⊢ ((𝐴<P
𝐵 ∧ 𝑦 ∈ (1st ‘𝐴)) → 𝑦 ∈ Q) |
79 | 78 | 3adant2 1011 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → 𝑦 ∈ Q) |
80 | | addcomnqg 7332 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑟
+Q 𝑦) = (𝑦 +Q 𝑟)) |
81 | 74, 79, 80 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → (𝑟 +Q 𝑦) = (𝑦 +Q 𝑟)) |
82 | | ltaddnq 7358 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ Q ∧
𝑦 ∈ Q)
→ 𝑟
<Q (𝑟 +Q 𝑦)) |
83 | 74, 79, 82 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → 𝑟 <Q (𝑟 +Q
𝑦)) |
84 | | prcunqu 7436 |
. . . . . . . . . . . . . . 15
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑟 ∈ (2nd
‘𝐵)) → (𝑟 <Q
(𝑟
+Q 𝑦) → (𝑟 +Q 𝑦) ∈ (2nd
‘𝐵))) |
85 | 8, 84 | sylan 281 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ P ∧
𝑟 ∈ (2nd
‘𝐵)) → (𝑟 <Q
(𝑟
+Q 𝑦) → (𝑟 +Q 𝑦) ∈ (2nd
‘𝐵))) |
86 | 7, 85 | sylan 281 |
. . . . . . . . . . . . 13
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵)) → (𝑟 <Q (𝑟 +Q
𝑦) → (𝑟 +Q
𝑦) ∈ (2nd
‘𝐵))) |
87 | 86 | 3adant3 1012 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → (𝑟 <Q (𝑟 +Q
𝑦) → (𝑟 +Q
𝑦) ∈ (2nd
‘𝐵))) |
88 | 83, 87 | mpd 13 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → (𝑟 +Q 𝑦) ∈ (2nd
‘𝐵)) |
89 | 81, 88 | eqeltrrd 2248 |
. . . . . . . . . 10
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵)) |
90 | | 19.8a 1583 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑟) ∈ (2nd
‘𝐵)) →
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵))) |
91 | 75, 89, 90 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵))) |
92 | 74, 91 | jca 304 |
. . . . . . . 8
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵)))) |
93 | 52 | ltexprlemelu 7550 |
. . . . . . . 8
⊢ (𝑟 ∈ (2nd
‘𝐶) ↔ (𝑟 ∈ Q ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑟) ∈ (2nd
‘𝐵)))) |
94 | 92, 93 | sylibr 133 |
. . . . . . 7
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵) ∧ 𝑦 ∈ (1st ‘𝐴)) → 𝑟 ∈ (2nd ‘𝐶)) |
95 | 94 | 3expa 1198 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵)) ∧ 𝑦 ∈ (1st ‘𝐴)) → 𝑟 ∈ (2nd ‘𝐶)) |
96 | 73, 95 | exlimddv 1891 |
. . . . 5
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵)) → 𝑟 ∈ (2nd ‘𝐶)) |
97 | | 19.8a 1583 |
. . . . 5
⊢ ((𝑟 ∈ Q ∧
𝑟 ∈ (2nd
‘𝐶)) →
∃𝑟(𝑟 ∈ Q ∧ 𝑟 ∈ (2nd
‘𝐶))) |
98 | 68, 96, 97 | syl2anc 409 |
. . . 4
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵)) → ∃𝑟(𝑟 ∈ Q ∧ 𝑟 ∈ (2nd
‘𝐶))) |
99 | | df-rex 2454 |
. . . 4
⊢
(∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐶)
↔ ∃𝑟(𝑟 ∈ Q ∧
𝑟 ∈ (2nd
‘𝐶))) |
100 | 98, 99 | sylibr 133 |
. . 3
⊢ ((𝐴<P
𝐵 ∧ 𝑟 ∈ (2nd ‘𝐵)) → ∃𝑟 ∈ Q 𝑟 ∈ (2nd
‘𝐶)) |
101 | 60, 61, 65, 100 | exlimdd 1865 |
. 2
⊢ (𝐴<P
𝐵 → ∃𝑟 ∈ Q 𝑟 ∈ (2nd
‘𝐶)) |
102 | 59, 101 | jca 304 |
1
⊢ (𝐴<P
𝐵 → (∃𝑞 ∈ Q 𝑞 ∈ (1st
‘𝐶) ∧
∃𝑟 ∈
Q 𝑟 ∈
(2nd ‘𝐶))) |