Step | Hyp | Ref
| Expression |
1 | | ltrelpr 6488 |
. . . . . . . 8
⊢
<P ⊆ (P ×
P) |
2 | 1 | brel 4335 |
. . . . . . 7
⊢ (A<P B → (A
∈ P ∧ B ∈ P)) |
3 | 2 | simprd 107 |
. . . . . 6
⊢ (A<P B → B ∈ P) |
4 | | prop 6458 |
. . . . . 6
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
5 | 3, 4 | syl 14 |
. . . . 5
⊢ (A<P B → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
6 | | prnmaddl 6473 |
. . . . 5
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ w ∈ (1st ‘B)) → ∃v ∈ Q (w +Q v) ∈
(1st ‘B)) |
7 | 5, 6 | sylan 267 |
. . . 4
⊢
((A<P
B ∧
w ∈
(1st ‘B)) → ∃v ∈ Q (w +Q v) ∈
(1st ‘B)) |
8 | 2 | simpld 105 |
. . . . . . . 8
⊢ (A<P B → A ∈ P) |
9 | | prop 6458 |
. . . . . . . 8
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
10 | 8, 9 | syl 14 |
. . . . . . 7
⊢ (A<P B → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
11 | | prarloc 6486 |
. . . . . . 7
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ v ∈ Q) → ∃z ∈ (1st ‘A)∃u ∈
(2nd ‘A)u <Q (z +Q v)) |
12 | 10, 11 | sylan 267 |
. . . . . 6
⊢
((A<P
B ∧
v ∈
Q) → ∃z ∈
(1st ‘A)∃u ∈ (2nd ‘A)u
<Q (z
+Q v)) |
13 | 12 | ad2ant2r 478 |
. . . . 5
⊢
(((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) → ∃z ∈ (1st ‘A)∃u ∈
(2nd ‘A)u <Q (z +Q v)) |
14 | | simplll 485 |
. . . . . . . . . . 11
⊢
((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) → A<P B) |
15 | 14 | adantr 261 |
. . . . . . . . . 10
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → A<P B) |
16 | | simplrl 487 |
. . . . . . . . . 10
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → z
∈ (1st ‘A)) |
17 | | elprnql 6464 |
. . . . . . . . . . 11
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (1st ‘A)) → z
∈ Q) |
18 | 10, 17 | sylan 267 |
. . . . . . . . . 10
⊢
((A<P
B ∧
z ∈
(1st ‘A)) → z ∈
Q) |
19 | 15, 16, 18 | syl2anc 391 |
. . . . . . . . 9
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → z
∈ Q) |
20 | | elprnql 6464 |
. . . . . . . . . . 11
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ w ∈ (1st ‘B)) → w
∈ Q) |
21 | 5, 20 | sylan 267 |
. . . . . . . . . 10
⊢
((A<P
B ∧
w ∈
(1st ‘B)) → w ∈
Q) |
22 | 21 | ad3antrrr 461 |
. . . . . . . . 9
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → w
∈ Q) |
23 | | nqtri3or 6380 |
. . . . . . . . 9
⊢
((z ∈ Q ∧ w ∈ Q) → (z <Q w ∨ z = w ∨ w
<Q z)) |
24 | 19, 22, 23 | syl2anc 391 |
. . . . . . . 8
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → (z
<Q w ∨ z = w ∨ w <Q z)) |
25 | | ltexnqq 6391 |
. . . . . . . . . . . . 13
⊢
((z ∈ Q ∧ w ∈ Q) → (z <Q w ↔ ∃𝑠 ∈ Q (z +Q 𝑠) = w)) |
26 | 19, 22, 25 | syl2anc 391 |
. . . . . . . . . . . 12
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → (z
<Q w ↔
∃𝑠 ∈
Q (z
+Q 𝑠)
= w)) |
27 | 26 | biimpa 280 |
. . . . . . . . . . 11
⊢
((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) → ∃𝑠 ∈ Q (z +Q 𝑠) = w) |
28 | | simprr 484 |
. . . . . . . . . . . 12
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → (z +Q 𝑠) = w) |
29 | 16 | ad2antrr 457 |
. . . . . . . . . . . . 13
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → z ∈
(1st ‘A)) |
30 | | simprl 483 |
. . . . . . . . . . . . . 14
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → 𝑠 ∈
Q) |
31 | | simpr 103 |
. . . . . . . . . . . . . . . . 17
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → u
<Q (z
+Q v)) |
32 | | simplrr 488 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → u
∈ (2nd ‘A)) |
33 | | prcunqu 6468 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ u ∈ (2nd ‘A)) → (u
<Q (z
+Q v) →
(z +Q v) ∈
(2nd ‘A))) |
34 | 10, 33 | sylan 267 |
. . . . . . . . . . . . . . . . . 18
⊢
((A<P
B ∧
u ∈
(2nd ‘A)) → (u <Q (z +Q v) → (z
+Q v) ∈ (2nd ‘A))) |
35 | 15, 32, 34 | syl2anc 391 |
. . . . . . . . . . . . . . . . 17
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → (u
<Q (z
+Q v) →
(z +Q v) ∈
(2nd ‘A))) |
36 | 31, 35 | mpd 13 |
. . . . . . . . . . . . . . . 16
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → (z
+Q v) ∈ (2nd ‘A)) |
37 | 36 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → (z +Q v) ∈
(2nd ‘A)) |
38 | 19 | ad2antrr 457 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → z ∈
Q) |
39 | | simplrl 487 |
. . . . . . . . . . . . . . . . . 18
⊢
((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) → v
∈ Q) |
40 | 39 | ad3antrrr 461 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → v ∈
Q) |
41 | | addcomnqg 6365 |
. . . . . . . . . . . . . . . . . 18
⊢
((f ∈ Q ∧ g ∈ Q) → (f +Q g) = (g
+Q f)) |
42 | 41 | adantl 262 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) ∧
(f ∈
Q ∧ g ∈
Q)) → (f
+Q g) = (g +Q f)) |
43 | | addassnqg 6366 |
. . . . . . . . . . . . . . . . . 18
⊢
((f ∈ Q ∧ g ∈ Q ∧ ℎ
∈ Q) → ((f +Q g) +Q ℎ) = (f
+Q (g
+Q ℎ))) |
44 | 43 | adantl 262 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) ∧
(f ∈
Q ∧ g ∈
Q ∧ ℎ ∈
Q)) → ((f
+Q g)
+Q ℎ)
= (f +Q (g +Q ℎ))) |
45 | 38, 40, 30, 42, 44 | caov32d 5623 |
. . . . . . . . . . . . . . . 16
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → ((z +Q v) +Q 𝑠) = ((z
+Q 𝑠)
+Q v)) |
46 | | simplrr 488 |
. . . . . . . . . . . . . . . . . 18
⊢
((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) → (w
+Q v) ∈ (1st ‘B)) |
47 | 46 | ad3antrrr 461 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → (w +Q v) ∈
(1st ‘B)) |
48 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . . 19
⊢
((z +Q
𝑠) = w → ((z
+Q 𝑠)
+Q v) = (w +Q v)) |
49 | 48 | eleq1d 2103 |
. . . . . . . . . . . . . . . . . 18
⊢
((z +Q
𝑠) = w → (((z
+Q 𝑠)
+Q v) ∈ (1st ‘B) ↔ (w
+Q v) ∈ (1st ‘B))) |
50 | 28, 49 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → (((z +Q 𝑠) +Q v) ∈
(1st ‘B) ↔ (w +Q v) ∈
(1st ‘B))) |
51 | 47, 50 | mpbird 156 |
. . . . . . . . . . . . . . . 16
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → ((z +Q 𝑠) +Q v) ∈
(1st ‘B)) |
52 | 45, 51 | eqeltrd 2111 |
. . . . . . . . . . . . . . 15
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → ((z +Q v) +Q 𝑠) ∈
(1st ‘B)) |
53 | | eleq1 2097 |
. . . . . . . . . . . . . . . . . 18
⊢ (y = (z
+Q v) →
(y ∈
(2nd ‘A) ↔ (z +Q v) ∈
(2nd ‘A))) |
54 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . . 19
⊢ (y = (z
+Q v) →
(y +Q 𝑠) = ((z +Q v) +Q 𝑠)) |
55 | 54 | eleq1d 2103 |
. . . . . . . . . . . . . . . . . 18
⊢ (y = (z
+Q v) →
((y +Q 𝑠) ∈ (1st ‘B) ↔ ((z
+Q v)
+Q 𝑠)
∈ (1st ‘B))) |
56 | 53, 55 | anbi12d 442 |
. . . . . . . . . . . . . . . . 17
⊢ (y = (z
+Q v) →
((y ∈
(2nd ‘A) ∧ (y
+Q 𝑠)
∈ (1st ‘B)) ↔ ((z
+Q v) ∈ (2nd ‘A) ∧ ((z +Q v) +Q 𝑠) ∈
(1st ‘B)))) |
57 | 56 | spcegv 2635 |
. . . . . . . . . . . . . . . 16
⊢
((z +Q
v) ∈
(2nd ‘A) →
(((z +Q v) ∈
(2nd ‘A) ∧ ((z
+Q v)
+Q 𝑠)
∈ (1st ‘B)) → ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑠)
∈ (1st ‘B)))) |
58 | 57 | anabsi5 513 |
. . . . . . . . . . . . . . 15
⊢
(((z +Q
v) ∈
(2nd ‘A) ∧ ((z
+Q v)
+Q 𝑠)
∈ (1st ‘B)) → ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑠)
∈ (1st ‘B))) |
59 | 37, 52, 58 | syl2anc 391 |
. . . . . . . . . . . . . 14
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑠)
∈ (1st ‘B))) |
60 | | ltexprlem.1 |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = 〈{x ∈
Q ∣ ∃y(y ∈ (2nd ‘A) ∧ (y +Q x) ∈
(1st ‘B))}, {x ∈
Q ∣ ∃y(y ∈ (1st ‘A) ∧ (y +Q x) ∈
(2nd ‘B))}〉 |
61 | 60 | ltexprlemell 6572 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (1st ‘𝐶) ↔ (𝑠 ∈
Q ∧ ∃y(y ∈
(2nd ‘A) ∧ (y
+Q 𝑠)
∈ (1st ‘B)))) |
62 | 30, 59, 61 | sylanbrc 394 |
. . . . . . . . . . . . 13
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → 𝑠 ∈
(1st ‘𝐶)) |
63 | 15, 8 | syl 14 |
. . . . . . . . . . . . . . 15
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → A
∈ P) |
64 | 63 | ad2antrr 457 |
. . . . . . . . . . . . . 14
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → A ∈
P) |
65 | 60 | ltexprlempr 6582 |
. . . . . . . . . . . . . . . 16
⊢ (A<P B → 𝐶 ∈
P) |
66 | 15, 65 | syl 14 |
. . . . . . . . . . . . . . 15
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → 𝐶 ∈
P) |
67 | 66 | ad2antrr 457 |
. . . . . . . . . . . . . 14
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → 𝐶 ∈
P) |
68 | | df-iplp 6451 |
. . . . . . . . . . . . . . 15
⊢
+P = (x ∈ P, w ∈
P ↦ 〈{z ∈ Q ∣ ∃f ∈ Q ∃v ∈ Q (f ∈
(1st ‘x) ∧ v ∈ (1st ‘w) ∧ z = (f
+Q v))}, {z ∈
Q ∣ ∃f ∈
Q ∃v ∈
Q (f ∈ (2nd ‘x) ∧ v ∈
(2nd ‘w) ∧ z = (f +Q v))}〉) |
69 | | addclnq 6359 |
. . . . . . . . . . . . . . 15
⊢
((f ∈ Q ∧ v ∈ Q) → (f +Q v) ∈
Q) |
70 | 68, 69 | genpprecll 6497 |
. . . . . . . . . . . . . 14
⊢
((A ∈ P ∧ 𝐶 ∈
P) → ((z ∈ (1st ‘A) ∧ 𝑠 ∈ (1st ‘𝐶)) → (z +Q 𝑠) ∈
(1st ‘(A
+P 𝐶)))) |
71 | 64, 67, 70 | syl2anc 391 |
. . . . . . . . . . . . 13
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → ((z ∈
(1st ‘A) ∧ 𝑠
∈ (1st ‘𝐶)) → (z +Q 𝑠) ∈
(1st ‘(A
+P 𝐶)))) |
72 | 29, 62, 71 | mp2and 409 |
. . . . . . . . . . . 12
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → (z +Q 𝑠) ∈
(1st ‘(A
+P 𝐶))) |
73 | 28, 72 | eqeltrrd 2112 |
. . . . . . . . . . 11
⊢
(((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) ∧ (𝑠 ∈ Q ∧ (z
+Q 𝑠)
= w)) → w ∈
(1st ‘(A
+P 𝐶))) |
74 | 27, 73 | rexlimddv 2431 |
. . . . . . . . . 10
⊢
((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z <Q w) → w
∈ (1st ‘(A +P 𝐶))) |
75 | 74 | ex 108 |
. . . . . . . . 9
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → (z
<Q w →
w ∈
(1st ‘(A
+P 𝐶)))) |
76 | 14 | ad2antrr 457 |
. . . . . . . . . . 11
⊢
((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z = w) →
A<P B) |
77 | | simpr 103 |
. . . . . . . . . . . 12
⊢
((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z = w) →
z = w) |
78 | 16 | adantr 261 |
. . . . . . . . . . . 12
⊢
((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z = w) →
z ∈
(1st ‘A)) |
79 | 77, 78 | eqeltrrd 2112 |
. . . . . . . . . . 11
⊢
((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z = w) →
w ∈
(1st ‘A)) |
80 | | ltaddpr 6571 |
. . . . . . . . . . . . 13
⊢
((A ∈ P ∧ 𝐶 ∈
P) → A<P (A +P 𝐶)) |
81 | 8, 65, 80 | syl2anc 391 |
. . . . . . . . . . . 12
⊢ (A<P B → A<P (A +P 𝐶)) |
82 | | ltprordil 6565 |
. . . . . . . . . . . . 13
⊢ (A<P (A +P 𝐶) → (1st ‘A) ⊆ (1st ‘(A +P 𝐶))) |
83 | 82 | sseld 2938 |
. . . . . . . . . . . 12
⊢ (A<P (A +P 𝐶) → (w ∈
(1st ‘A) → w ∈
(1st ‘(A
+P 𝐶)))) |
84 | 81, 83 | syl 14 |
. . . . . . . . . . 11
⊢ (A<P B → (w
∈ (1st ‘A) → w
∈ (1st ‘(A +P 𝐶)))) |
85 | 76, 79, 84 | sylc 56 |
. . . . . . . . . 10
⊢
((((((A<P B ∧ w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) ∧ z = w) →
w ∈
(1st ‘(A
+P 𝐶))) |
86 | 85 | ex 108 |
. . . . . . . . 9
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → (z =
w → w ∈
(1st ‘(A
+P 𝐶)))) |
87 | | prcdnql 6467 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (1st ‘A)) → (w
<Q z →
w ∈
(1st ‘A))) |
88 | 10, 87 | sylan 267 |
. . . . . . . . . . 11
⊢
((A<P
B ∧
z ∈
(1st ‘A)) → (w <Q z → w ∈ (1st ‘A))) |
89 | 15, 16, 88 | syl2anc 391 |
. . . . . . . . . 10
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → (w
<Q z →
w ∈
(1st ‘A))) |
90 | 15, 89, 84 | sylsyld 52 |
. . . . . . . . 9
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → (w
<Q z →
w ∈
(1st ‘(A
+P 𝐶)))) |
91 | 75, 86, 90 | 3jaod 1198 |
. . . . . . . 8
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → ((z
<Q w ∨ z = w ∨ w <Q z) → w
∈ (1st ‘(A +P 𝐶)))) |
92 | 24, 91 | mpd 13 |
. . . . . . 7
⊢
(((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) ∧ u <Q (z +Q v)) → w
∈ (1st ‘(A +P 𝐶))) |
93 | 92 | ex 108 |
. . . . . 6
⊢
((((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) ∧ (z ∈
(1st ‘A) ∧ u ∈ (2nd ‘A))) → (u
<Q (z
+Q v) →
w ∈
(1st ‘(A
+P 𝐶)))) |
94 | 93 | rexlimdvva 2434 |
. . . . 5
⊢
(((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) → (∃z ∈ (1st ‘A)∃u ∈
(2nd ‘A)u <Q (z +Q v) → w
∈ (1st ‘(A +P 𝐶)))) |
95 | 13, 94 | mpd 13 |
. . . 4
⊢
(((A<P
B ∧
w ∈
(1st ‘B)) ∧ (v ∈ Q ∧ (w
+Q v) ∈ (1st ‘B))) → w
∈ (1st ‘(A +P 𝐶))) |
96 | 7, 95 | rexlimddv 2431 |
. . 3
⊢
((A<P
B ∧
w ∈
(1st ‘B)) → w ∈
(1st ‘(A
+P 𝐶))) |
97 | 96 | ex 108 |
. 2
⊢ (A<P B → (w
∈ (1st ‘B) → w
∈ (1st ‘(A +P 𝐶)))) |
98 | 97 | ssrdv 2945 |
1
⊢ (A<P B → (1st ‘B) ⊆ (1st ‘(A +P 𝐶))) |