Step | Hyp | Ref
| Expression |
1 | | supsrlem.2 |
. . . . . . 7
⊢ 𝐶 ∈
R |
2 | | 0idsr 9797 |
. . . . . . 7
⊢ (𝐶 ∈ R →
(𝐶
+R 0R) = 𝐶) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → (𝐶 +R
0R) = 𝐶) |
4 | | simpl 472 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → 𝐶 ∈ 𝐴) |
5 | 3, 4 | eqeltrd 2688 |
. . . . 5
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → (𝐶 +R
0R) ∈ 𝐴) |
6 | | 1pr 9716 |
. . . . . . 7
⊢
1P ∈ P |
7 | 6 | elexi 3186 |
. . . . . 6
⊢
1P ∈ V |
8 | | opeq1 4340 |
. . . . . . . . . 10
⊢ (𝑤 = 1P
→ 〈𝑤,
1P〉 = 〈1P,
1P〉) |
9 | 8 | eceq1d 7670 |
. . . . . . . . 9
⊢ (𝑤 = 1P
→ [〈𝑤,
1P〉] ~R =
[〈1P, 1P〉]
~R ) |
10 | | df-0r 9761 |
. . . . . . . . 9
⊢
0R = [〈1P,
1P〉] ~R |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑤 = 1P
→ [〈𝑤,
1P〉] ~R =
0R) |
12 | 11 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑤 = 1P
→ (𝐶
+R [〈𝑤, 1P〉]
~R ) = (𝐶 +R
0R)) |
13 | 12 | eleq1d 2672 |
. . . . . 6
⊢ (𝑤 = 1P
→ ((𝐶
+R [〈𝑤, 1P〉]
~R ) ∈ 𝐴 ↔ (𝐶 +R
0R) ∈ 𝐴)) |
14 | | supsrlem.1 |
. . . . . 6
⊢ 𝐵 = {𝑤 ∣ (𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴} |
15 | 7, 13, 14 | elab2 3323 |
. . . . 5
⊢
(1P ∈ 𝐵 ↔ (𝐶 +R
0R) ∈ 𝐴) |
16 | 5, 15 | sylibr 223 |
. . . 4
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) →
1P ∈ 𝐵) |
17 | | ne0i 3880 |
. . . 4
⊢
(1P ∈ 𝐵 → 𝐵 ≠ ∅) |
18 | 16, 17 | syl 17 |
. . 3
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → 𝐵 ≠ ∅) |
19 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑦 = 𝐶 → (𝑦 <R 𝑥 ↔ 𝐶 <R 𝑥)) |
20 | 19 | rspccv 3279 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (𝐶 ∈ 𝐴 → 𝐶 <R 𝑥)) |
21 | | 0lt1sr 9795 |
. . . . . . . . . . . . 13
⊢
0R <R
1R |
22 | | m1r 9782 |
. . . . . . . . . . . . . 14
⊢
-1R ∈ R |
23 | | ltasr 9800 |
. . . . . . . . . . . . . 14
⊢
(-1R ∈ R →
(0R <R
1R ↔ (-1R
+R 0R)
<R (-1R
+R 1R))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(0R <R
1R ↔ (-1R
+R 0R)
<R (-1R
+R 1R)) |
25 | 21, 24 | mpbi 219 |
. . . . . . . . . . . 12
⊢
(-1R +R
0R) <R
(-1R +R
1R) |
26 | | 0idsr 9797 |
. . . . . . . . . . . . 13
⊢
(-1R ∈ R →
(-1R +R
0R) = -1R) |
27 | 22, 26 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(-1R +R
0R) = -1R |
28 | | m1p1sr 9792 |
. . . . . . . . . . . 12
⊢
(-1R +R
1R) = 0R |
29 | 25, 27, 28 | 3brtr3i 4612 |
. . . . . . . . . . 11
⊢
-1R <R
0R |
30 | | ltasr 9800 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ R →
(-1R <R
0R ↔ (𝐶 +R
-1R) <R (𝐶 +R
0R))) |
31 | 1, 30 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(-1R <R
0R ↔ (𝐶 +R
-1R) <R (𝐶 +R
0R)) |
32 | 29, 31 | mpbi 219 |
. . . . . . . . . 10
⊢ (𝐶 +R
-1R) <R (𝐶 +R
0R) |
33 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝐶 +R
0R) = 𝐶 |
34 | 32, 33 | breqtri 4608 |
. . . . . . . . 9
⊢ (𝐶 +R
-1R) <R 𝐶 |
35 | | ltsosr 9794 |
. . . . . . . . . 10
⊢
<R Or R |
36 | | ltrelsr 9768 |
. . . . . . . . . 10
⊢
<R ⊆ (R ×
R) |
37 | 35, 36 | sotri 5442 |
. . . . . . . . 9
⊢ (((𝐶 +R
-1R) <R 𝐶 ∧ 𝐶 <R 𝑥) → (𝐶 +R
-1R) <R 𝑥) |
38 | 34, 37 | mpan 702 |
. . . . . . . 8
⊢ (𝐶 <R
𝑥 → (𝐶 +R
-1R) <R 𝑥) |
39 | 1 | map2psrpr 9810 |
. . . . . . . 8
⊢ ((𝐶 +R
-1R) <R 𝑥 ↔ ∃𝑣 ∈ P (𝐶 +R [〈𝑣,
1P〉] ~R ) = 𝑥) |
40 | 38, 39 | sylib 207 |
. . . . . . 7
⊢ (𝐶 <R
𝑥 → ∃𝑣 ∈ P (𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥) |
41 | 20, 40 | syl6 34 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (𝐶 ∈ 𝐴 → ∃𝑣 ∈ P (𝐶 +R [〈𝑣,
1P〉] ~R ) = 𝑥)) |
42 | | breq2 4587 |
. . . . . . . . . 10
⊢ ((𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) ↔ 𝑦 <R
𝑥)) |
43 | 42 | ralbidv 2969 |
. . . . . . . . 9
⊢ ((𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) ↔
∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)) |
44 | 14 | abeq2i 2722 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐵 ↔ (𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴) |
45 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐶 +R [〈𝑤,
1P〉] ~R ) → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) ↔ (𝐶 +R [〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R
))) |
46 | 45 | rspccv 3279 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) → ((𝐶 +R
[〈𝑤,
1P〉] ~R ) ∈ 𝐴 → (𝐶 +R [〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R
))) |
47 | 1 | ltpsrpr 9809 |
. . . . . . . . . . . 12
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑤<P
𝑣) |
48 | 46, 47 | syl6ib 240 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) → ((𝐶 +R
[〈𝑤,
1P〉] ~R ) ∈ 𝐴 → 𝑤<P 𝑣)) |
49 | 44, 48 | syl5bi 231 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) → (𝑤 ∈ 𝐵 → 𝑤<P 𝑣)) |
50 | 49 | ralrimiv 2948 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∀𝑤 ∈ 𝐵 𝑤<P 𝑣) |
51 | 43, 50 | syl6bir 243 |
. . . . . . . 8
⊢ ((𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
52 | 51 | com12 32 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → ((𝐶 +R [〈𝑣,
1P〉] ~R ) = 𝑥 → ∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
53 | 52 | reximdv 2999 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (∃𝑣 ∈ P (𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥 → ∃𝑣 ∈ P
∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
54 | 41, 53 | syld 46 |
. . . . 5
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (𝐶 ∈ 𝐴 → ∃𝑣 ∈ P ∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
55 | 54 | rexlimivw 3011 |
. . . 4
⊢
(∃𝑥 ∈
R ∀𝑦
∈ 𝐴 𝑦 <R 𝑥 → (𝐶 ∈ 𝐴 → ∃𝑣 ∈ P ∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
56 | 55 | impcom 445 |
. . 3
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑣 ∈ P
∀𝑤 ∈ 𝐵 𝑤<P 𝑣) |
57 | | supexpr 9755 |
. . 3
⊢ ((𝐵 ≠ ∅ ∧ ∃𝑣 ∈ P
∀𝑤 ∈ 𝐵 𝑤<P 𝑣) → ∃𝑣 ∈ P
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))) |
58 | 18, 56, 57 | syl2anc 691 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑣 ∈ P
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))) |
59 | 1 | mappsrpr 9808 |
. . . . . . 7
⊢ ((𝐶 +R
-1R) <R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑣 ∈
P) |
60 | 36 | brel 5090 |
. . . . . . 7
⊢ ((𝐶 +R
-1R) <R (𝐶 +R [〈𝑣,
1P〉] ~R ) → ((𝐶 +R
-1R) ∈ R ∧ (𝐶 +R [〈𝑣,
1P〉] ~R ) ∈
R)) |
61 | 59, 60 | sylbir 224 |
. . . . . 6
⊢ (𝑣 ∈ P →
((𝐶
+R -1R) ∈
R ∧ (𝐶
+R [〈𝑣, 1P〉]
~R ) ∈ R)) |
62 | 61 | simprd 478 |
. . . . 5
⊢ (𝑣 ∈ P →
(𝐶
+R [〈𝑣, 1P〉]
~R ) ∈ R) |
63 | 62 | adantl 481 |
. . . 4
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) → (𝐶 +R
[〈𝑣,
1P〉] ~R ) ∈
R) |
64 | 35, 36 | sotri 5442 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 +R
-1R) <R (𝐶 +R [〈𝑣,
1P〉] ~R ) ∧ (𝐶 +R
[〈𝑣,
1P〉] ~R )
<R 𝑦) → (𝐶 +R
-1R) <R 𝑦) |
65 | 59, 64 | sylanbr 489 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ P ∧
(𝐶
+R [〈𝑣, 1P〉]
~R ) <R 𝑦) → (𝐶 +R
-1R) <R 𝑦) |
66 | 1 | map2psrpr 9810 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 +R
-1R) <R 𝑦 ↔ ∃𝑤 ∈ P (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) |
67 | 65, 66 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ P ∧
(𝐶
+R [〈𝑣, 1P〉]
~R ) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) |
68 | | rexex 2985 |
. . . . . . . . . . . . 13
⊢
(∃𝑤 ∈
P (𝐶
+R [〈𝑤, 1P〉]
~R ) = 𝑦 → ∃𝑤(𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) |
69 | | df-ral 2901 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑤(𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤)) |
70 | | 19.29 1789 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑤(𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ ∃𝑤(𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → ∃𝑤((𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦)) |
71 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
72 | 44, 71 | syl5bb 271 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐴)) |
73 | 1 | ltpsrpr 9809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 +R
[〈𝑣,
1P〉] ~R )
<R (𝐶 +R [〈𝑤,
1P〉] ~R ) ↔ 𝑣<P
𝑤) |
74 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝐶 +R [〈𝑣,
1P〉] ~R )
<R (𝐶 +R [〈𝑤,
1P〉] ~R ) ↔ (𝐶 +R
[〈𝑣,
1P〉] ~R )
<R 𝑦)) |
75 | 73, 74 | syl5bbr 273 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (𝑣<P 𝑤 ↔ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
76 | 75 | notbid 307 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (¬ 𝑣<P
𝑤 ↔ ¬ (𝐶 +R
[〈𝑣,
1P〉] ~R )
<R 𝑦)) |
77 | 72, 76 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ↔ (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦))) |
78 | 77 | biimpac 502 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
79 | 78 | exlimiv 1845 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑤((𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
80 | 70, 79 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑤(𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ ∃𝑤(𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
81 | 69, 80 | sylanb 488 |
. . . . . . . . . . . . . 14
⊢
((∀𝑤 ∈
𝐵 ¬ 𝑣<P 𝑤 ∧ ∃𝑤(𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
82 | 81 | expcom 450 |
. . . . . . . . . . . . 13
⊢
(∃𝑤(𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦))) |
83 | 67, 68, 82 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ P ∧
(𝐶
+R [〈𝑣, 1P〉]
~R ) <R 𝑦) → (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦))) |
84 | 83 | impd 446 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ P ∧
(𝐶
+R [〈𝑣, 1P〉]
~R ) <R 𝑦) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ 𝑦 ∈ 𝐴) → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
85 | 84 | impancom 455 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ P ∧
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ 𝑦 ∈ 𝐴)) → ((𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
86 | 85 | pm2.01d 180 |
. . . . . . . . 9
⊢ ((𝑣 ∈ P ∧
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ 𝑦 ∈ 𝐴)) → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦) |
87 | 86 | expr 641 |
. . . . . . . 8
⊢ ((𝑣 ∈ P ∧
∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
88 | 87 | ralrimiv 2948 |
. . . . . . 7
⊢ ((𝑣 ∈ P ∧
∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤) → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦) |
89 | 88 | ex 449 |
. . . . . 6
⊢ (𝑣 ∈ P →
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
90 | 89 | adantl 481 |
. . . . 5
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) →
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
91 | | r19.29 3054 |
. . . . . . . . . . . . . 14
⊢
((∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ ∃𝑤 ∈ P (𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦) → ∃𝑤 ∈ P ((𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦)) |
92 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝐶 +R [〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ))) |
93 | 47, 92 | syl5bbr 273 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (𝑤<P 𝑣 ↔ 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
))) |
94 | 93 | biimprd 237 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) → 𝑤<P
𝑣)) |
95 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑢 ∈ V |
96 | | opeq1 4340 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑢 → 〈𝑤, 1P〉 =
〈𝑢,
1P〉) |
97 | 96 | eceq1d 7670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑢 → [〈𝑤, 1P〉]
~R = [〈𝑢, 1P〉]
~R ) |
98 | 97 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑢 → (𝐶 +R [〈𝑤,
1P〉] ~R ) = (𝐶 +R
[〈𝑢,
1P〉] ~R
)) |
99 | 98 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑢 → ((𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴 ↔ (𝐶 +R [〈𝑢,
1P〉] ~R ) ∈ 𝐴)) |
100 | 95, 99, 14 | elab2 3323 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ 𝐵 ↔ (𝐶 +R [〈𝑢,
1P〉] ~R ) ∈ 𝐴) |
101 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝐶 +R [〈𝑢,
1P〉] ~R ) → ((𝐶 +R
[〈𝑤,
1P〉] ~R )
<R 𝑧 ↔ (𝐶 +R [〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑢,
1P〉] ~R
))) |
102 | 1 | ltpsrpr 9809 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑢,
1P〉] ~R ) ↔ 𝑤<P
𝑢) |
103 | 101, 102 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝐶 +R [〈𝑢,
1P〉] ~R ) → ((𝐶 +R
[〈𝑤,
1P〉] ~R )
<R 𝑧 ↔ 𝑤<P 𝑢)) |
104 | 103 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 +R
[〈𝑢,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑤<P 𝑢) → ∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧) |
105 | 100, 104 | sylanb 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ 𝐵 ∧ 𝑤<P 𝑢) → ∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧) |
106 | 105 | rexlimiva 3010 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢 ∈
𝐵 𝑤<P 𝑢 → ∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧) |
107 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧 ↔ 𝑦 <R 𝑧)) |
108 | 107 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧 ↔ ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
109 | 106, 108 | syl5ib 233 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (∃𝑢 ∈ 𝐵 𝑤<P 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
110 | 94, 109 | imim12d 79 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
111 | 110 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
112 | 111 | rexlimivw 3011 |
. . . . . . . . . . . . . 14
⊢
(∃𝑤 ∈
P ((𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
113 | 91, 112 | syl 17 |
. . . . . . . . . . . . 13
⊢
((∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ ∃𝑤 ∈ P (𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
114 | 66, 113 | sylan2b 491 |
. . . . . . . . . . . 12
⊢
((∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ (𝐶 +R
-1R) <R 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
115 | 114 | ex 449 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → ((𝐶 +R
-1R) <R 𝑦 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
116 | 115 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ((𝐶 +R
-1R) <R 𝑦 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
117 | 116 | a1dd 48 |
. . . . . . . . 9
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ((𝐶 +R
-1R) <R 𝑦 → (𝑦 ∈ R → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
118 | 35, 36 | sotri2 5444 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ R ∧
¬ (𝐶
+R -1R)
<R 𝑦 ∧ (𝐶 +R
-1R) <R 𝐶) → 𝑦 <R 𝐶) |
119 | 34, 118 | mp3an3 1405 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ R ∧
¬ (𝐶
+R -1R)
<R 𝑦) → 𝑦 <R 𝐶) |
120 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝐶 → (𝑦 <R 𝑧 ↔ 𝑦 <R 𝐶)) |
121 | 120 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) |
122 | 121 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝐴 → (𝑦 <R 𝐶 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
123 | 122 | a1dd 48 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝐴 → (𝑦 <R 𝐶 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
124 | 119, 123 | syl5 33 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝐴 → ((𝑦 ∈ R ∧ ¬ (𝐶 +R
-1R) <R 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
125 | 124 | expcomd 453 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝐴 → (¬ (𝐶 +R
-1R) <R 𝑦 → (𝑦 ∈ R → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
126 | 125 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → (¬ (𝐶 +R
-1R) <R 𝑦 → (𝑦 ∈ R → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
127 | 117, 126 | pm2.61d 169 |
. . . . . . . 8
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → (𝑦 ∈ R → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
128 | 127 | ralrimiv 2948 |
. . . . . . 7
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∀𝑦 ∈ R (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
129 | 128 | ex 449 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) →
(∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → ∀𝑦 ∈ R (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
130 | 129 | adantlr 747 |
. . . . 5
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) →
(∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → ∀𝑦 ∈ R (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
131 | 90, 130 | anim12d 584 |
. . . 4
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) →
((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
132 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → (𝑥 <R
𝑦 ↔ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
133 | 132 | notbid 307 |
. . . . . . 7
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → (¬
𝑥
<R 𝑦 ↔ ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
134 | 133 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
135 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → (𝑦 <R
𝑥 ↔ 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
))) |
136 | 135 | imbi1d 330 |
. . . . . . 7
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → ((𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) ↔ (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
137 | 136 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
(∀𝑦 ∈
R (𝑦
<R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) ↔ ∀𝑦 ∈ R (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
138 | 134, 137 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
((∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
139 | 138 | rspcev 3282 |
. . . 4
⊢ (((𝐶 +R
[〈𝑣,
1P〉] ~R ) ∈
R ∧ (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
140 | 63, 131, 139 | syl6an 566 |
. . 3
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) →
((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
141 | 140 | rexlimdva 3013 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → (∃𝑣 ∈ P
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
142 | 58, 141 | mpd 15 |
1
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |