Step | Hyp | Ref
| Expression |
1 | | ltexprlem.1 |
. . . . 5
⊢ 𝐶 = 〈{x ∈
Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈
(1st ‘B))}, {x ∈
Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈
(2nd ‘B))}〉 |
2 | 1 | ltexprlemelu 6573 |
. . . 4
⊢ (𝑟 ∈ (2nd ‘𝐶) ↔ (𝑟 ∈
Q ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B)))) |
3 | 2 | simprbi 260 |
. . 3
⊢ (𝑟 ∈ (2nd ‘𝐶) → ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B))) |
4 | | 19.42v 1783 |
. . . . . . . 8
⊢ (∃y(A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ↔
(A<P B ∧ ∃y(𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B))))) |
5 | | 19.42v 1783 |
. . . . . . . . 9
⊢ (∃y(𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B))) ↔ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) |
6 | 5 | anbi2i 430 |
. . . . . . . 8
⊢
((A<P
B ∧ ∃y(𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ↔
(A<P B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B))))) |
7 | 4, 6 | bitri 173 |
. . . . . . 7
⊢ (∃y(A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ↔
(A<P B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B))))) |
8 | | ltrelpr 6488 |
. . . . . . . . . . . . . . 15
⊢
<P ⊆ (P ×
P) |
9 | 8 | brel 4335 |
. . . . . . . . . . . . . 14
⊢ (A<P B → (A
∈ P ∧ B ∈ P)) |
10 | 9 | simprd 107 |
. . . . . . . . . . . . 13
⊢ (A<P B → B ∈ P) |
11 | | prop 6458 |
. . . . . . . . . . . . 13
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
12 | 10, 11 | syl 14 |
. . . . . . . . . . . 12
⊢ (A<P B → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
13 | | prnminu 6472 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ (y
+Q 𝑟)
∈ (2nd ‘B)) → ∃𝑠 ∈ (2nd ‘B)𝑠
<Q (y
+Q 𝑟)) |
14 | 12, 13 | sylan 267 |
. . . . . . . . . . 11
⊢
((A<P
B ∧
(y +Q 𝑟) ∈ (2nd ‘B)) → ∃𝑠 ∈ (2nd ‘B)𝑠
<Q (y
+Q 𝑟)) |
15 | 14 | adantrl 447 |
. . . . . . . . . 10
⊢
((A<P
B ∧
(y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B))) → ∃𝑠 ∈
(2nd ‘B)𝑠 <Q (y +Q 𝑟)) |
16 | 15 | adantrl 447 |
. . . . . . . . 9
⊢
((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) → ∃𝑠 ∈
(2nd ‘B)𝑠 <Q (y +Q 𝑟)) |
17 | | ltdfpr 6489 |
. . . . . . . . . . . . . . 15
⊢
((A ∈ P ∧ B ∈ P) → (A<P B ↔ ∃𝑡 ∈ Q (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) |
18 | 17 | biimpd 132 |
. . . . . . . . . . . . . 14
⊢
((A ∈ P ∧ B ∈ P) → (A<P B → ∃𝑡 ∈ Q (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) |
19 | 9, 18 | mpcom 32 |
. . . . . . . . . . . . 13
⊢ (A<P B → ∃𝑡 ∈ Q (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B))) |
20 | 19 | ad2antrr 457 |
. . . . . . . . . . . 12
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → ∃𝑡 ∈
Q (𝑡 ∈ (2nd ‘A) ∧ 𝑡 ∈ (1st ‘B))) |
21 | 9 | simpld 105 |
. . . . . . . . . . . . . . . 16
⊢ (A<P B → A ∈ P) |
22 | 21 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → A ∈
P) |
23 | 22 | adantr 261 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → A
∈ P) |
24 | | simplrr 488 |
. . . . . . . . . . . . . . . 16
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → (y ∈
(1st ‘A) ∧ (y
+Q 𝑟)
∈ (2nd ‘B))) |
25 | 24 | simpld 105 |
. . . . . . . . . . . . . . 15
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → y ∈
(1st ‘A)) |
26 | 25 | adantr 261 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → y
∈ (1st ‘A)) |
27 | | simprrl 491 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → 𝑡 ∈
(2nd ‘A)) |
28 | | prop 6458 |
. . . . . . . . . . . . . . 15
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
29 | | prltlu 6470 |
. . . . . . . . . . . . . . 15
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ y ∈ (1st ‘A) ∧ 𝑡 ∈ (2nd ‘A)) → y
<Q 𝑡) |
30 | 28, 29 | syl3an1 1167 |
. . . . . . . . . . . . . 14
⊢
((A ∈ P ∧ y ∈ (1st ‘A) ∧ 𝑡 ∈ (2nd ‘A)) → y
<Q 𝑡) |
31 | 23, 26, 27, 30 | syl3anc 1134 |
. . . . . . . . . . . . 13
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → y
<Q 𝑡) |
32 | | simplll 485 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → A<P B) |
33 | | simprrr 492 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → 𝑡 ∈
(1st ‘B)) |
34 | | simplrl 487 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → 𝑠 ∈
(2nd ‘B)) |
35 | | prltlu 6470 |
. . . . . . . . . . . . . . 15
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ 𝑡
∈ (1st ‘B) ∧ 𝑠 ∈ (2nd ‘B)) → 𝑡 <Q 𝑠) |
36 | 12, 35 | syl3an1 1167 |
. . . . . . . . . . . . . 14
⊢
((A<P
B ∧ 𝑡 ∈ (1st ‘B) ∧ 𝑠 ∈ (2nd ‘B)) → 𝑡 <Q 𝑠) |
37 | 32, 33, 34, 36 | syl3anc 1134 |
. . . . . . . . . . . . 13
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → 𝑡 <Q 𝑠) |
38 | | ltsonq 6382 |
. . . . . . . . . . . . . 14
⊢
<Q Or Q |
39 | | ltrelnq 6349 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
40 | 38, 39 | sotri 4663 |
. . . . . . . . . . . . 13
⊢
((y <Q
𝑡 ∧ 𝑡
<Q 𝑠) → y <Q 𝑠) |
41 | 31, 37, 40 | syl2anc 391 |
. . . . . . . . . . . 12
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑡 ∈ Q ∧ (𝑡 ∈
(2nd ‘A) ∧ 𝑡
∈ (1st ‘B)))) → y
<Q 𝑠) |
42 | 20, 41 | rexlimddv 2431 |
. . . . . . . . . . 11
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → y <Q 𝑠) |
43 | | elprnql 6464 |
. . . . . . . . . . . . . 14
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ y ∈ (1st ‘A)) → y
∈ Q) |
44 | 28, 43 | sylan 267 |
. . . . . . . . . . . . 13
⊢
((A ∈ P ∧ y ∈ (1st ‘A)) → y
∈ Q) |
45 | 22, 25, 44 | syl2anc 391 |
. . . . . . . . . . . 12
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → y ∈
Q) |
46 | | elprnqu 6465 |
. . . . . . . . . . . . . 14
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ 𝑠
∈ (2nd ‘B)) → 𝑠 ∈
Q) |
47 | 12, 46 | sylan 267 |
. . . . . . . . . . . . 13
⊢
((A<P
B ∧ 𝑠 ∈ (2nd ‘B)) → 𝑠 ∈
Q) |
48 | 47 | ad2ant2r 478 |
. . . . . . . . . . . 12
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → 𝑠 ∈
Q) |
49 | | ltexnqq 6391 |
. . . . . . . . . . . 12
⊢
((y ∈ Q ∧ 𝑠
∈ Q) → (y <Q 𝑠 ↔ ∃𝑞 ∈
Q (y
+Q 𝑞)
= 𝑠)) |
50 | 45, 48, 49 | syl2anc 391 |
. . . . . . . . . . 11
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → (y <Q 𝑠 ↔ ∃𝑞 ∈
Q (y
+Q 𝑞)
= 𝑠)) |
51 | 42, 50 | mpbid 135 |
. . . . . . . . . 10
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → ∃𝑞 ∈
Q (y
+Q 𝑞)
= 𝑠) |
52 | | simprr 484 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → (y +Q 𝑞) = 𝑠) |
53 | | simplrr 488 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → 𝑠 <Q (y +Q 𝑟)) |
54 | 52, 53 | eqbrtrd 3775 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → (y +Q 𝑞) <Q (y +Q 𝑟)) |
55 | | simprl 483 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → 𝑞 ∈
Q) |
56 | | simplrl 487 |
. . . . . . . . . . . . . . . 16
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → 𝑟 ∈
Q) |
57 | 56 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → 𝑟 ∈
Q) |
58 | 45 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → y ∈
Q) |
59 | | ltanqg 6384 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ Q ∧ 𝑟
∈ Q ∧ y ∈ Q) → (𝑞 <Q 𝑟 ↔ (y +Q 𝑞) <Q (y +Q 𝑟))) |
60 | 55, 57, 58, 59 | syl3anc 1134 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → (𝑞 <Q 𝑟 ↔ (y +Q 𝑞) <Q (y +Q 𝑟))) |
61 | 54, 60 | mpbird 156 |
. . . . . . . . . . . . 13
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → 𝑞 <Q 𝑟) |
62 | 25 | adantr 261 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → y ∈
(1st ‘A)) |
63 | | simplrl 487 |
. . . . . . . . . . . . . . 15
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → 𝑠 ∈
(2nd ‘B)) |
64 | 52, 63 | eqeltrd 2111 |
. . . . . . . . . . . . . 14
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → (y +Q 𝑞) ∈
(2nd ‘B)) |
65 | 62, 64 | jca 290 |
. . . . . . . . . . . . 13
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → (y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B))) |
66 | 61, 55, 65 | jca32 293 |
. . . . . . . . . . . 12
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ (𝑞 ∈ Q ∧ (y
+Q 𝑞)
= 𝑠)) → (𝑞 <Q 𝑟 ∧
(𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
67 | 66 | expr 357 |
. . . . . . . . . . 11
⊢
((((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) ∧ 𝑞 ∈ Q) → ((y +Q 𝑞) = 𝑠 → (𝑞 <Q 𝑟 ∧
(𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B)))))) |
68 | 67 | reximdva 2415 |
. . . . . . . . . 10
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → (∃𝑞 ∈
Q (y
+Q 𝑞)
= 𝑠 → ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B)))))) |
69 | 51, 68 | mpd 13 |
. . . . . . . . 9
⊢
(((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) ∧ (𝑠 ∈
(2nd ‘B) ∧ 𝑠
<Q (y
+Q 𝑟))) → ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
70 | 16, 69 | rexlimddv 2431 |
. . . . . . . 8
⊢
((A<P
B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) → ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
71 | 70 | eximi 1488 |
. . . . . . 7
⊢ (∃y(A<P B ∧ (𝑟 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) → ∃y∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
72 | 7, 71 | sylbir 125 |
. . . . . 6
⊢
((A<P
B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) → ∃y∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
73 | | rexcom4 2571 |
. . . . . 6
⊢ (∃𝑞 ∈
Q ∃y(𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B)))) ↔ ∃y∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
74 | 72, 73 | sylibr 137 |
. . . . 5
⊢
((A<P
B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) → ∃𝑞 ∈
Q ∃y(𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
75 | | 19.42v 1783 |
. . . . . . 7
⊢ (∃y(𝑞 <Q
𝑟 ∧ (𝑞 ∈
Q ∧ (y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B)))) ↔ (𝑞 <Q 𝑟 ∧
∃y(𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
76 | | 19.42v 1783 |
. . . . . . . 8
⊢ (∃y(𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))) ↔ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B)))) |
77 | 76 | anbi2i 430 |
. . . . . . 7
⊢ ((𝑞 <Q
𝑟 ∧ ∃y(𝑞
∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B)))) ↔ (𝑞 <Q
𝑟 ∧ (𝑞 ∈
Q ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B))))) |
78 | 75, 77 | bitri 173 |
. . . . . 6
⊢ (∃y(𝑞 <Q
𝑟 ∧ (𝑞 ∈
Q ∧ (y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B)))) ↔ (𝑞 <Q 𝑟 ∧
(𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
79 | 78 | rexbii 2325 |
. . . . 5
⊢ (∃𝑞 ∈
Q ∃y(𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ (y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B)))) ↔ ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
80 | 74, 79 | sylib 127 |
. . . 4
⊢
((A<P
B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) → ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
81 | 1 | ltexprlemelu 6573 |
. . . . . 6
⊢ (𝑞 ∈ (2nd ‘𝐶) ↔ (𝑞 ∈
Q ∧ ∃y(y ∈
(1st ‘A) ∧ (y
+Q 𝑞)
∈ (2nd ‘B)))) |
82 | 81 | anbi2i 430 |
. . . . 5
⊢ ((𝑞 <Q
𝑟 ∧ 𝑞
∈ (2nd ‘𝐶)) ↔ (𝑞 <Q 𝑟 ∧
(𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
83 | 82 | rexbii 2325 |
. . . 4
⊢ (∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) ↔ ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ (𝑞 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑞) ∈
(2nd ‘B))))) |
84 | 80, 83 | sylibr 137 |
. . 3
⊢
((A<P
B ∧ (𝑟 ∈ Q ∧ ∃y(y ∈ (1st ‘A) ∧ (y +Q 𝑟) ∈
(2nd ‘B)))) → ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶))) |
85 | 3, 84 | sylanr2 385 |
. 2
⊢
((A<P
B ∧ (𝑟 ∈ Q ∧ 𝑟
∈ (2nd ‘𝐶))) → ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶))) |
86 | 85 | 3impb 1099 |
1
⊢
((A<P
B ∧ 𝑟 ∈ Q ∧ 𝑟
∈ (2nd ‘𝐶)) → ∃𝑞 ∈
Q (𝑞
<Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶))) |