Step | Hyp | Ref
| Expression |
1 | | supsrlem.2 |
. . . . . . 7
⊢ 𝐶 ∈
R |
2 | | 0idsr 10853 |
. . . . . . 7
⊢ (𝐶 ∈ R →
(𝐶
+R 0R) = 𝐶) |
3 | 1, 2 | mp1i 13 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → (𝐶 +R
0R) = 𝐶) |
4 | | simpl 483 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → 𝐶 ∈ 𝐴) |
5 | 3, 4 | eqeltrd 2839 |
. . . . 5
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → (𝐶 +R
0R) ∈ 𝐴) |
6 | | 1pr 10771 |
. . . . . . 7
⊢
1P ∈ P |
7 | 6 | elexi 3451 |
. . . . . 6
⊢
1P ∈ V |
8 | | opeq1 4804 |
. . . . . . . . . 10
⊢ (𝑤 = 1P
→ 〈𝑤,
1P〉 = 〈1P,
1P〉) |
9 | 8 | eceq1d 8537 |
. . . . . . . . 9
⊢ (𝑤 = 1P
→ [〈𝑤,
1P〉] ~R =
[〈1P, 1P〉]
~R ) |
10 | | df-0r 10816 |
. . . . . . . . 9
⊢
0R = [〈1P,
1P〉] ~R |
11 | 9, 10 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑤 = 1P
→ [〈𝑤,
1P〉] ~R =
0R) |
12 | 11 | oveq2d 7291 |
. . . . . . 7
⊢ (𝑤 = 1P
→ (𝐶
+R [〈𝑤, 1P〉]
~R ) = (𝐶 +R
0R)) |
13 | 12 | eleq1d 2823 |
. . . . . 6
⊢ (𝑤 = 1P
→ ((𝐶
+R [〈𝑤, 1P〉]
~R ) ∈ 𝐴 ↔ (𝐶 +R
0R) ∈ 𝐴)) |
14 | | supsrlem.1 |
. . . . . 6
⊢ 𝐵 = {𝑤 ∣ (𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴} |
15 | 7, 13, 14 | elab2 3613 |
. . . . 5
⊢
(1P ∈ 𝐵 ↔ (𝐶 +R
0R) ∈ 𝐴) |
16 | 5, 15 | sylibr 233 |
. . . 4
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) →
1P ∈ 𝐵) |
17 | 16 | ne0d 4269 |
. . 3
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → 𝐵 ≠ ∅) |
18 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑦 = 𝐶 → (𝑦 <R 𝑥 ↔ 𝐶 <R 𝑥)) |
19 | 18 | rspccv 3558 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (𝐶 ∈ 𝐴 → 𝐶 <R 𝑥)) |
20 | | 0lt1sr 10851 |
. . . . . . . . . . . . 13
⊢
0R <R
1R |
21 | | m1r 10838 |
. . . . . . . . . . . . . 14
⊢
-1R ∈ R |
22 | | ltasr 10856 |
. . . . . . . . . . . . . 14
⊢
(-1R ∈ R →
(0R <R
1R ↔ (-1R
+R 0R)
<R (-1R
+R 1R))) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(0R <R
1R ↔ (-1R
+R 0R)
<R (-1R
+R 1R)) |
24 | 20, 23 | mpbi 229 |
. . . . . . . . . . . 12
⊢
(-1R +R
0R) <R
(-1R +R
1R) |
25 | | 0idsr 10853 |
. . . . . . . . . . . . 13
⊢
(-1R ∈ R →
(-1R +R
0R) = -1R) |
26 | 21, 25 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(-1R +R
0R) = -1R |
27 | | m1p1sr 10848 |
. . . . . . . . . . . 12
⊢
(-1R +R
1R) = 0R |
28 | 24, 26, 27 | 3brtr3i 5103 |
. . . . . . . . . . 11
⊢
-1R <R
0R |
29 | | ltasr 10856 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ R →
(-1R <R
0R ↔ (𝐶 +R
-1R) <R (𝐶 +R
0R))) |
30 | 1, 29 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(-1R <R
0R ↔ (𝐶 +R
-1R) <R (𝐶 +R
0R)) |
31 | 28, 30 | mpbi 229 |
. . . . . . . . . 10
⊢ (𝐶 +R
-1R) <R (𝐶 +R
0R) |
32 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝐶 +R
0R) = 𝐶 |
33 | 31, 32 | breqtri 5099 |
. . . . . . . . 9
⊢ (𝐶 +R
-1R) <R 𝐶 |
34 | | ltsosr 10850 |
. . . . . . . . . 10
⊢
<R Or R |
35 | | ltrelsr 10824 |
. . . . . . . . . 10
⊢
<R ⊆ (R ×
R) |
36 | 34, 35 | sotri 6032 |
. . . . . . . . 9
⊢ (((𝐶 +R
-1R) <R 𝐶 ∧ 𝐶 <R 𝑥) → (𝐶 +R
-1R) <R 𝑥) |
37 | 33, 36 | mpan 687 |
. . . . . . . 8
⊢ (𝐶 <R
𝑥 → (𝐶 +R
-1R) <R 𝑥) |
38 | 1 | map2psrpr 10866 |
. . . . . . . 8
⊢ ((𝐶 +R
-1R) <R 𝑥 ↔ ∃𝑣 ∈ P (𝐶 +R [〈𝑣,
1P〉] ~R ) = 𝑥) |
39 | 37, 38 | sylib 217 |
. . . . . . 7
⊢ (𝐶 <R
𝑥 → ∃𝑣 ∈ P (𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥) |
40 | 19, 39 | syl6 35 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (𝐶 ∈ 𝐴 → ∃𝑣 ∈ P (𝐶 +R [〈𝑣,
1P〉] ~R ) = 𝑥)) |
41 | | breq2 5078 |
. . . . . . . . . 10
⊢ ((𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) ↔ 𝑦 <R
𝑥)) |
42 | 41 | ralbidv 3112 |
. . . . . . . . 9
⊢ ((𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) ↔
∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)) |
43 | 14 | abeq2i 2875 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐵 ↔ (𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴) |
44 | | breq1 5077 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐶 +R [〈𝑤,
1P〉] ~R ) → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) ↔ (𝐶 +R [〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R
))) |
45 | 44 | rspccv 3558 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) → ((𝐶 +R
[〈𝑤,
1P〉] ~R ) ∈ 𝐴 → (𝐶 +R [〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R
))) |
46 | 1 | ltpsrpr 10865 |
. . . . . . . . . . . 12
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑤<P
𝑣) |
47 | 45, 46 | syl6ib 250 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) → ((𝐶 +R
[〈𝑤,
1P〉] ~R ) ∈ 𝐴 → 𝑤<P 𝑣)) |
48 | 43, 47 | syl5bi 241 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) → (𝑤 ∈ 𝐵 → 𝑤<P 𝑣)) |
49 | 48 | ralrimiv 3102 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝐴 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∀𝑤 ∈ 𝐵 𝑤<P 𝑣) |
50 | 42, 49 | syl6bir 253 |
. . . . . . . 8
⊢ ((𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
51 | 50 | com12 32 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → ((𝐶 +R [〈𝑣,
1P〉] ~R ) = 𝑥 → ∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
52 | 51 | reximdv 3202 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (∃𝑣 ∈ P (𝐶 +R
[〈𝑣,
1P〉] ~R ) = 𝑥 → ∃𝑣 ∈ P
∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
53 | 40, 52 | syld 47 |
. . . . 5
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (𝐶 ∈ 𝐴 → ∃𝑣 ∈ P ∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
54 | 53 | rexlimivw 3211 |
. . . 4
⊢
(∃𝑥 ∈
R ∀𝑦
∈ 𝐴 𝑦 <R 𝑥 → (𝐶 ∈ 𝐴 → ∃𝑣 ∈ P ∀𝑤 ∈ 𝐵 𝑤<P 𝑣)) |
55 | 54 | impcom 408 |
. . 3
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑣 ∈ P
∀𝑤 ∈ 𝐵 𝑤<P 𝑣) |
56 | | supexpr 10810 |
. . 3
⊢ ((𝐵 ≠ ∅ ∧ ∃𝑣 ∈ P
∀𝑤 ∈ 𝐵 𝑤<P 𝑣) → ∃𝑣 ∈ P
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))) |
57 | 17, 55, 56 | syl2anc 584 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑣 ∈ P
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢))) |
58 | 1 | mappsrpr 10864 |
. . . . . . 7
⊢ ((𝐶 +R
-1R) <R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑣 ∈
P) |
59 | 35 | brel 5652 |
. . . . . . 7
⊢ ((𝐶 +R
-1R) <R (𝐶 +R [〈𝑣,
1P〉] ~R ) → ((𝐶 +R
-1R) ∈ R ∧ (𝐶 +R [〈𝑣,
1P〉] ~R ) ∈
R)) |
60 | 58, 59 | sylbir 234 |
. . . . . 6
⊢ (𝑣 ∈ P →
((𝐶
+R -1R) ∈
R ∧ (𝐶
+R [〈𝑣, 1P〉]
~R ) ∈ R)) |
61 | 60 | simprd 496 |
. . . . 5
⊢ (𝑣 ∈ P →
(𝐶
+R [〈𝑣, 1P〉]
~R ) ∈ R) |
62 | 61 | adantl 482 |
. . . 4
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) → (𝐶 +R
[〈𝑣,
1P〉] ~R ) ∈
R) |
63 | 34, 35 | sotri 6032 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 +R
-1R) <R (𝐶 +R [〈𝑣,
1P〉] ~R ) ∧ (𝐶 +R
[〈𝑣,
1P〉] ~R )
<R 𝑦) → (𝐶 +R
-1R) <R 𝑦) |
64 | 58, 63 | sylanbr 582 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ P ∧
(𝐶
+R [〈𝑣, 1P〉]
~R ) <R 𝑦) → (𝐶 +R
-1R) <R 𝑦) |
65 | 1 | map2psrpr 10866 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 +R
-1R) <R 𝑦 ↔ ∃𝑤 ∈ P (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) |
66 | 64, 65 | sylib 217 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ P ∧
(𝐶
+R [〈𝑣, 1P〉]
~R ) <R 𝑦) → ∃𝑤 ∈ P (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) |
67 | | rexex 3171 |
. . . . . . . . . . . . 13
⊢
(∃𝑤 ∈
P (𝐶
+R [〈𝑤, 1P〉]
~R ) = 𝑦 → ∃𝑤(𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) |
68 | | df-ral 3069 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝐵 ¬ 𝑣<P 𝑤 ↔ ∀𝑤(𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤)) |
69 | | 19.29 1876 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑤(𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ ∃𝑤(𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → ∃𝑤((𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦)) |
70 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
71 | 43, 70 | bitrid 282 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐴)) |
72 | 1 | ltpsrpr 10865 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 +R
[〈𝑣,
1P〉] ~R )
<R (𝐶 +R [〈𝑤,
1P〉] ~R ) ↔ 𝑣<P
𝑤) |
73 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝐶 +R [〈𝑣,
1P〉] ~R )
<R (𝐶 +R [〈𝑤,
1P〉] ~R ) ↔ (𝐶 +R
[〈𝑣,
1P〉] ~R )
<R 𝑦)) |
74 | 72, 73 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (𝑣<P 𝑤 ↔ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
75 | 74 | notbid 318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (¬ 𝑣<P
𝑤 ↔ ¬ (𝐶 +R
[〈𝑣,
1P〉] ~R )
<R 𝑦)) |
76 | 71, 75 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ↔ (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦))) |
77 | 76 | biimpac 479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
78 | 77 | exlimiv 1933 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑤((𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
79 | 69, 78 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑤(𝑤 ∈ 𝐵 → ¬ 𝑣<P 𝑤) ∧ ∃𝑤(𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
80 | 68, 79 | sylanb 581 |
. . . . . . . . . . . . . 14
⊢
((∀𝑤 ∈
𝐵 ¬ 𝑣<P 𝑤 ∧ ∃𝑤(𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
81 | 80 | expcom 414 |
. . . . . . . . . . . . 13
⊢
(∃𝑤(𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦))) |
82 | 66, 67, 81 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ P ∧
(𝐶
+R [〈𝑣, 1P〉]
~R ) <R 𝑦) → (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦))) |
83 | 82 | impd 411 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ P ∧
(𝐶
+R [〈𝑣, 1P〉]
~R ) <R 𝑦) → ((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ 𝑦 ∈ 𝐴) → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
84 | 83 | impancom 452 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ P ∧
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ 𝑦 ∈ 𝐴)) → ((𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
85 | 84 | pm2.01d 189 |
. . . . . . . . 9
⊢ ((𝑣 ∈ P ∧
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ 𝑦 ∈ 𝐴)) → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦) |
86 | 85 | expr 457 |
. . . . . . . 8
⊢ ((𝑣 ∈ P ∧
∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤) → (𝑦 ∈ 𝐴 → ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
87 | 86 | ralrimiv 3102 |
. . . . . . 7
⊢ ((𝑣 ∈ P ∧
∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤) → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦) |
88 | 87 | ex 413 |
. . . . . 6
⊢ (𝑣 ∈ P →
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
89 | 88 | adantl 482 |
. . . . 5
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) →
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 → ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
90 | | r19.29 3184 |
. . . . . . . . . . . . . 14
⊢
((∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ ∃𝑤 ∈ P (𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦) → ∃𝑤 ∈ P ((𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦)) |
91 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝐶 +R [〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ))) |
92 | 46, 91 | bitr3id 285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (𝑤<P 𝑣 ↔ 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
))) |
93 | 92 | biimprd 247 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) → 𝑤<P
𝑣)) |
94 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑢 ∈ V |
95 | | opeq1 4804 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑢 → 〈𝑤, 1P〉 =
〈𝑢,
1P〉) |
96 | 95 | eceq1d 8537 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑢 → [〈𝑤, 1P〉]
~R = [〈𝑢, 1P〉]
~R ) |
97 | 96 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑢 → (𝐶 +R [〈𝑤,
1P〉] ~R ) = (𝐶 +R
[〈𝑢,
1P〉] ~R
)) |
98 | 97 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑢 → ((𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴 ↔ (𝐶 +R [〈𝑢,
1P〉] ~R ) ∈ 𝐴)) |
99 | 94, 98, 14 | elab2 3613 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ 𝐵 ↔ (𝐶 +R [〈𝑢,
1P〉] ~R ) ∈ 𝐴) |
100 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝐶 +R [〈𝑢,
1P〉] ~R ) → ((𝐶 +R
[〈𝑤,
1P〉] ~R )
<R 𝑧 ↔ (𝐶 +R [〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑢,
1P〉] ~R
))) |
101 | 1 | ltpsrpr 10865 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R )
<R (𝐶 +R [〈𝑢,
1P〉] ~R ) ↔ 𝑤<P
𝑢) |
102 | 100, 101 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝐶 +R [〈𝑢,
1P〉] ~R ) → ((𝐶 +R
[〈𝑤,
1P〉] ~R )
<R 𝑧 ↔ 𝑤<P 𝑢)) |
103 | 102 | rspcev 3561 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 +R
[〈𝑢,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑤<P 𝑢) → ∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧) |
104 | 99, 103 | sylanb 581 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ 𝐵 ∧ 𝑤<P 𝑢) → ∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧) |
105 | 104 | rexlimiva 3210 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢 ∈
𝐵 𝑤<P 𝑢 → ∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧) |
106 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧 ↔ 𝑦 <R 𝑧)) |
107 | 106 | rexbidv 3226 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑤,
1P〉] ~R )
<R 𝑧 ↔ ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
108 | 105, 107 | syl5ib 243 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → (∃𝑢 ∈ 𝐵 𝑤<P 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
109 | 93, 108 | imim12d 81 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦 → ((𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
110 | 109 | impcom 408 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
111 | 110 | rexlimivw 3211 |
. . . . . . . . . . . . . 14
⊢
(∃𝑤 ∈
P ((𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ (𝐶 +R [〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
112 | 90, 111 | syl 17 |
. . . . . . . . . . . . 13
⊢
((∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ ∃𝑤 ∈ P (𝐶 +R
[〈𝑤,
1P〉] ~R ) = 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
113 | 65, 112 | sylan2b 594 |
. . . . . . . . . . . 12
⊢
((∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) ∧ (𝐶 +R
-1R) <R 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
114 | 113 | ex 413 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → ((𝐶 +R
-1R) <R 𝑦 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
115 | 114 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ((𝐶 +R
-1R) <R 𝑦 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
116 | 115 | a1dd 50 |
. . . . . . . . 9
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ((𝐶 +R
-1R) <R 𝑦 → (𝑦 ∈ R → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
117 | 34, 35 | sotri2 6034 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ R ∧
¬ (𝐶
+R -1R)
<R 𝑦 ∧ (𝐶 +R
-1R) <R 𝐶) → 𝑦 <R 𝐶) |
118 | 33, 117 | mp3an3 1449 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ R ∧
¬ (𝐶
+R -1R)
<R 𝑦) → 𝑦 <R 𝐶) |
119 | | breq2 5078 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝐶 → (𝑦 <R 𝑧 ↔ 𝑦 <R 𝐶)) |
120 | 119 | rspcev 3561 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ 𝐴 ∧ 𝑦 <R 𝐶) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) |
121 | 120 | ex 413 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝐴 → (𝑦 <R 𝐶 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
122 | 121 | a1dd 50 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝐴 → (𝑦 <R 𝐶 → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
123 | 118, 122 | syl5 34 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝐴 → ((𝑦 ∈ R ∧ ¬ (𝐶 +R
-1R) <R 𝑦) → (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
124 | 123 | expcomd 417 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝐴 → (¬ (𝐶 +R
-1R) <R 𝑦 → (𝑦 ∈ R → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
125 | 124 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → (¬ (𝐶 +R
-1R) <R 𝑦 → (𝑦 ∈ R → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
126 | 116, 125 | pm2.61d 179 |
. . . . . . . 8
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → (𝑦 ∈ R → (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
127 | 126 | ralrimiv 3102 |
. . . . . . 7
⊢ (((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∀𝑦 ∈ R (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) |
128 | 127 | ex 413 |
. . . . . 6
⊢ ((𝐶 ∈ 𝐴 ∧ 𝑣 ∈ P) →
(∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → ∀𝑦 ∈ R (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
129 | 128 | adantlr 712 |
. . . . 5
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) →
(∀𝑤 ∈
P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢) → ∀𝑦 ∈ R (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
130 | 89, 129 | anim12d 609 |
. . . 4
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) →
((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
131 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → (𝑥 <R
𝑦 ↔ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
132 | 131 | notbid 318 |
. . . . . . 7
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → (¬
𝑥
<R 𝑦 ↔ ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
133 | 132 | ralbidv 3112 |
. . . . . 6
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦)) |
134 | | breq2 5078 |
. . . . . . . 8
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → (𝑦 <R
𝑥 ↔ 𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
))) |
135 | 134 | imbi1d 342 |
. . . . . . 7
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → ((𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) ↔ (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
136 | 135 | ralbidv 3112 |
. . . . . 6
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
(∀𝑦 ∈
R (𝑦
<R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧) ↔ ∀𝑦 ∈ R (𝑦 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
137 | 133, 136 | anbi12d 631 |
. . . . 5
⊢ (𝑥 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
((∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
138 | 137 | rspcev 3561 |
. . . 4
⊢ (((𝐶 +R
[〈𝑣,
1P〉] ~R ) ∈
R ∧ (∀𝑦 ∈ 𝐴 ¬ (𝐶 +R [〈𝑣,
1P〉] ~R )
<R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |
139 | 62, 130, 138 | syl6an 681 |
. . 3
⊢ (((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ∧ 𝑣 ∈ P) →
((∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
140 | 139 | rexlimdva 3213 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → (∃𝑣 ∈ P
(∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P
𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) |
141 | 57, 140 | mpd 15 |
1
⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |