Proof of Theorem ltexprlemlol
Step | Hyp | Ref
| Expression |
1 | | simplr 482 |
. . . . . 6
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) → 𝑞 ∈ Q) |
2 | | simprrr 492 |
. . . . . . 7
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
(y ∈
(2nd ‘A) ∧ (y
+Q 𝑟)
∈ (1st ‘B))) |
3 | 2 | simpld 105 |
. . . . . 6
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
y ∈
(2nd ‘A)) |
4 | | simprl 483 |
. . . . . . . 8
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) → 𝑞 <Q
𝑟) |
5 | | simpll 481 |
. . . . . . . . 9
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
A<P B) |
6 | | ltrelpr 6488 |
. . . . . . . . . . . 12
⊢
<P ⊆ (P ×
P) |
7 | 6 | brel 4335 |
. . . . . . . . . . 11
⊢ (A<P B → (A
∈ P ∧ B ∈ P)) |
8 | 7 | simpld 105 |
. . . . . . . . . 10
⊢ (A<P B → A ∈ P) |
9 | | prop 6458 |
. . . . . . . . . . 11
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
10 | | elprnqu 6465 |
. . . . . . . . . . 11
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ y ∈ (2nd ‘A)) → y
∈ Q) |
11 | 9, 10 | sylan 267 |
. . . . . . . . . 10
⊢
((A ∈ P ∧ y ∈ (2nd ‘A)) → y
∈ Q) |
12 | 8, 11 | sylan 267 |
. . . . . . . . 9
⊢
((A<P
B ∧
y ∈
(2nd ‘A)) → y ∈
Q) |
13 | 5, 3, 12 | syl2anc 391 |
. . . . . . . 8
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
y ∈
Q) |
14 | | ltanqi 6386 |
. . . . . . . 8
⊢ ((𝑞 <Q
𝑟 ∧ y ∈ Q) → (y +Q 𝑞) <Q (y +Q 𝑟)) |
15 | 4, 13, 14 | syl2anc 391 |
. . . . . . 7
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
(y +Q 𝑞) <Q
(y +Q 𝑟)) |
16 | 7 | simprd 107 |
. . . . . . . . 9
⊢ (A<P B → B ∈ P) |
17 | 5, 16 | syl 14 |
. . . . . . . 8
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
B ∈
P) |
18 | 2 | simprd 107 |
. . . . . . . 8
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
(y +Q 𝑟) ∈ (1st ‘B)) |
19 | | prop 6458 |
. . . . . . . . 9
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
20 | | prcdnql 6467 |
. . . . . . . . 9
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ (y
+Q 𝑟)
∈ (1st ‘B)) → ((y
+Q 𝑞)
<Q (y
+Q 𝑟)
→ (y +Q 𝑞) ∈ (1st ‘B))) |
21 | 19, 20 | sylan 267 |
. . . . . . . 8
⊢
((B ∈ P ∧ (y
+Q 𝑟)
∈ (1st ‘B)) → ((y
+Q 𝑞)
<Q (y
+Q 𝑟)
→ (y +Q 𝑞) ∈ (1st ‘B))) |
22 | 17, 18, 21 | syl2anc 391 |
. . . . . . 7
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
((y +Q 𝑞) <Q
(y +Q 𝑟) → (y +Q 𝑞) ∈
(1st ‘B))) |
23 | 15, 22 | mpd 13 |
. . . . . 6
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) →
(y +Q 𝑞) ∈ (1st ‘B)) |
24 | 1, 3, 23 | jca32 293 |
. . . . 5
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) → (𝑞 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)))) |
25 | 24 | eximi 1488 |
. . . 4
⊢ (∃y((A<P B ∧ 𝑞 ∈
Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) → ∃y(𝑞 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)))) |
26 | | ltexprlem.1 |
. . . . . . . . . 10
⊢ 𝐶 = 〈{x ∈
Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈
(1st ‘B))}, {x ∈
Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈
(2nd ‘B))}〉 |
27 | 26 | ltexprlemell 6572 |
. . . . . . . . 9
⊢ (𝑟 ∈ (1st ‘𝐶) ↔ (𝑟 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑟)
∈ (1st ‘B)))) |
28 | | 19.42v 1783 |
. . . . . . . . 9
⊢ (∃y(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B)))) |
29 | 27, 28 | bitr4i 176 |
. . . . . . . 8
⊢ (𝑟 ∈ (1st ‘𝐶) ↔ ∃y(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B)))) |
30 | 29 | anbi2i 430 |
. . . . . . 7
⊢ ((𝑞 <Q
𝑟 ∧ 𝑟
∈ (1st ‘𝐶)) ↔ (𝑞 <Q 𝑟 ∧
∃y(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) |
31 | | 19.42v 1783 |
. . . . . . 7
⊢ (∃y(𝑞 <Q
𝑟 ∧ (𝑟 ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑟)
∈ (1st ‘B)))) ↔ (𝑞 <Q 𝑟 ∧
∃y(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) |
32 | 30, 31 | bitr4i 176 |
. . . . . 6
⊢ ((𝑞 <Q
𝑟 ∧ 𝑟
∈ (1st ‘𝐶)) ↔ ∃y(𝑞 <Q
𝑟 ∧ (𝑟 ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑟)
∈ (1st ‘B))))) |
33 | 32 | anbi2i 430 |
. . . . 5
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
𝑟 ∈ (1st ‘𝐶))) ↔ ((A<P B ∧ 𝑞 ∈
Q) ∧ ∃y(𝑞 <Q
𝑟 ∧ (𝑟 ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑟)
∈ (1st ‘B)))))) |
34 | | 19.42v 1783 |
. . . . 5
⊢ (∃y((A<P B ∧ 𝑞 ∈
Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B))))) ↔
((A<P B ∧ 𝑞 ∈
Q) ∧ ∃y(𝑞 <Q
𝑟 ∧ (𝑟 ∈
Q ∧ (y ∈
(2nd ‘A) ∧ (y
+Q 𝑟)
∈ (1st ‘B)))))) |
35 | 33, 34 | bitr4i 176 |
. . . 4
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
𝑟 ∈ (1st ‘𝐶))) ↔ ∃y((A<P B ∧ 𝑞 ∈
Q) ∧ (𝑞 <Q 𝑟 ∧
(𝑟 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑟) ∈
(1st ‘B)))))) |
36 | 26 | ltexprlemell 6572 |
. . . . 5
⊢ (𝑞 ∈ (1st ‘𝐶) ↔ (𝑞 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑞)
∈ (1st ‘B)))) |
37 | | 19.42v 1783 |
. . . . 5
⊢ (∃y(𝑞 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B))) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)))) |
38 | 36, 37 | bitr4i 176 |
. . . 4
⊢ (𝑞 ∈ (1st ‘𝐶) ↔ ∃y(𝑞 ∈ Q ∧ (y ∈ (2nd ‘A) ∧ (y +Q 𝑞) ∈
(1st ‘B)))) |
39 | 25, 35, 38 | 3imtr4i 190 |
. . 3
⊢
(((A<P
B ∧ 𝑞 ∈ Q) ∧ (𝑞 <Q 𝑟 ∧
𝑟 ∈ (1st ‘𝐶))) → 𝑞 ∈
(1st ‘𝐶)) |
40 | 39 | ex 108 |
. 2
⊢
((A<P
B ∧ 𝑞 ∈ Q) → ((𝑞 <Q 𝑟 ∧
𝑟 ∈ (1st ‘𝐶)) → 𝑞 ∈
(1st ‘𝐶))) |
41 | 40 | rexlimdvw 2430 |
1
⊢
((A<P
B ∧ 𝑞 ∈ Q) → (∃𝑟 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)) → 𝑞 ∈
(1st ‘𝐶))) |