Proof of Theorem suplocsrlemb
Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → 𝑢<P 𝑣) |
2 | | simplrl 530 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → 𝑢 ∈ P) |
3 | | simplrr 531 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → 𝑣 ∈ P) |
4 | | suplocsrlem.ss |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ R) |
5 | | suplocsrlem.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
6 | 4, 5 | sseldd 3148 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ R) |
7 | 6 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → 𝐶 ∈ R) |
8 | | ltpsrprg 7765 |
. . . . . . 7
⊢ ((𝑢 ∈ P ∧
𝑣 ∈ P
∧ 𝐶 ∈
R) → ((𝐶
+R [〈𝑢, 1P〉]
~R ) <R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑢<P
𝑣)) |
9 | 2, 3, 7, 8 | syl3anc 1233 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → ((𝐶 +R [〈𝑢,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑢<P
𝑣)) |
10 | 1, 9 | mpbird 166 |
. . . . 5
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → (𝐶 +R [〈𝑢,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R
)) |
11 | | breq2 3993 |
. . . . . . 7
⊢ (𝑦 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → ((𝐶 +R
[〈𝑢,
1P〉] ~R )
<R 𝑦 ↔ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R
))) |
12 | | breq2 3993 |
. . . . . . . . 9
⊢ (𝑦 = (𝐶 +R [〈𝑣,
1P〉] ~R ) → (𝑧 <R
𝑦 ↔ 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
))) |
13 | 12 | ralbidv 2470 |
. . . . . . . 8
⊢ (𝑦 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
(∀𝑧 ∈ 𝐴 𝑧 <R 𝑦 ↔ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
))) |
14 | 13 | orbi2d 785 |
. . . . . . 7
⊢ (𝑦 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
((∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦) ↔ (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
)))) |
15 | 11, 14 | imbi12d 233 |
. . . . . 6
⊢ (𝑦 = (𝐶 +R [〈𝑣,
1P〉] ~R ) →
(((𝐶
+R [〈𝑢, 1P〉]
~R ) <R 𝑦 → (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)) ↔ ((𝐶 +R [〈𝑢,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R ) →
(∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
))))) |
16 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑥 = (𝐶 +R [〈𝑢,
1P〉] ~R ) → (𝑥 <R
𝑦 ↔ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑦)) |
17 | | breq1 3992 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐶 +R [〈𝑢,
1P〉] ~R ) → (𝑥 <R
𝑧 ↔ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧)) |
18 | 17 | rexbidv 2471 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐶 +R [〈𝑢,
1P〉] ~R ) →
(∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ↔ ∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧)) |
19 | 18 | orbi1d 786 |
. . . . . . . . 9
⊢ (𝑥 = (𝐶 +R [〈𝑢,
1P〉] ~R ) →
((∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦) ↔ (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦))) |
20 | 16, 19 | imbi12d 233 |
. . . . . . . 8
⊢ (𝑥 = (𝐶 +R [〈𝑢,
1P〉] ~R ) → ((𝑥 <R
𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)) ↔ ((𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑦 → (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))) |
21 | 20 | ralbidv 2470 |
. . . . . . 7
⊢ (𝑥 = (𝐶 +R [〈𝑢,
1P〉] ~R ) →
(∀𝑦 ∈
R (𝑥
<R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)) ↔ ∀𝑦 ∈ R ((𝐶 +R
[〈𝑢,
1P〉] ~R )
<R 𝑦 → (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))) |
22 | | suplocsrlem.loc |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R
𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦))) |
23 | 22 | ad2antrr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → ∀𝑥 ∈ R
∀𝑦 ∈
R (𝑥
<R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦))) |
24 | | 1pr 7516 |
. . . . . . . . . . . 12
⊢
1P ∈ P |
25 | 24 | a1i 9 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) →
1P ∈ P) |
26 | 2, 25 | opelxpd 4644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → 〈𝑢,
1P〉 ∈ (P ×
P)) |
27 | | enrex 7699 |
. . . . . . . . . . 11
⊢
~R ∈ V |
28 | 27 | ecelqsi 6567 |
. . . . . . . . . 10
⊢
(〈𝑢,
1P〉 ∈ (P ×
P) → [〈𝑢, 1P〉]
~R ∈ ((P × P)
/ ~R )) |
29 | 26, 28 | syl 14 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → [〈𝑢,
1P〉] ~R ∈
((P × P) / ~R
)) |
30 | | df-nr 7689 |
. . . . . . . . 9
⊢
R = ((P × P) /
~R ) |
31 | 29, 30 | eleqtrrdi 2264 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → [〈𝑢,
1P〉] ~R ∈
R) |
32 | | addclsr 7715 |
. . . . . . . 8
⊢ ((𝐶 ∈ R ∧
[〈𝑢,
1P〉] ~R ∈
R) → (𝐶
+R [〈𝑢, 1P〉]
~R ) ∈ R) |
33 | 7, 31, 32 | syl2anc 409 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → (𝐶 +R [〈𝑢,
1P〉] ~R ) ∈
R) |
34 | 21, 23, 33 | rspcdva 2839 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → ∀𝑦 ∈ R ((𝐶 +R
[〈𝑢,
1P〉] ~R )
<R 𝑦 → (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦))) |
35 | 3, 25 | opelxpd 4644 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → 〈𝑣,
1P〉 ∈ (P ×
P)) |
36 | 27 | ecelqsi 6567 |
. . . . . . . . 9
⊢
(〈𝑣,
1P〉 ∈ (P ×
P) → [〈𝑣, 1P〉]
~R ∈ ((P × P)
/ ~R )) |
37 | 36, 30 | eleqtrrdi 2264 |
. . . . . . . 8
⊢
(〈𝑣,
1P〉 ∈ (P ×
P) → [〈𝑣, 1P〉]
~R ∈ R) |
38 | 35, 37 | syl 14 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → [〈𝑣,
1P〉] ~R ∈
R) |
39 | | addclsr 7715 |
. . . . . . 7
⊢ ((𝐶 ∈ R ∧
[〈𝑣,
1P〉] ~R ∈
R) → (𝐶
+R [〈𝑣, 1P〉]
~R ) ∈ R) |
40 | 7, 38, 39 | syl2anc 409 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → (𝐶 +R [〈𝑣,
1P〉] ~R ) ∈
R) |
41 | 15, 34, 40 | rspcdva 2839 |
. . . . 5
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → ((𝐶 +R [〈𝑢,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R ) →
(∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
)))) |
42 | 10, 41 | mpd 13 |
. . . 4
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
))) |
43 | 2 | ad2antrr 485 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → 𝑢 ∈ P) |
44 | 7 | ad2antrr 485 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → 𝐶 ∈ R) |
45 | | mappsrprg 7766 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ P ∧
𝐶 ∈ R)
→ (𝐶
+R -1R)
<R (𝐶 +R [〈𝑢,
1P〉] ~R
)) |
46 | 43, 44, 45 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → (𝐶 +R
-1R) <R (𝐶 +R [〈𝑢,
1P〉] ~R
)) |
47 | | simpr 109 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) |
48 | | ltsosr 7726 |
. . . . . . . . . . 11
⊢
<R Or R |
49 | | ltrelsr 7700 |
. . . . . . . . . . 11
⊢
<R ⊆ (R ×
R) |
50 | 48, 49 | sotri 5006 |
. . . . . . . . . 10
⊢ (((𝐶 +R
-1R) <R (𝐶 +R [〈𝑢,
1P〉] ~R ) ∧ (𝐶 +R
[〈𝑢,
1P〉] ~R )
<R 𝑧) → (𝐶 +R
-1R) <R 𝑧) |
51 | 46, 47, 50 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → (𝐶 +R
-1R) <R 𝑧) |
52 | | map2psrprg 7767 |
. . . . . . . . . 10
⊢ (𝐶 ∈ R →
((𝐶
+R -1R)
<R 𝑧 ↔ ∃𝑞 ∈ P (𝐶 +R [〈𝑞,
1P〉] ~R ) = 𝑧)) |
53 | 44, 52 | syl 14 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → ((𝐶 +R
-1R) <R 𝑧 ↔ ∃𝑞 ∈ P (𝐶 +R [〈𝑞,
1P〉] ~R ) = 𝑧)) |
54 | 51, 53 | mpbid 146 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → ∃𝑞 ∈ P (𝐶 +R [〈𝑞,
1P〉] ~R ) = 𝑧) |
55 | | simpr 109 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → (𝐶 +R [〈𝑞,
1P〉] ~R ) = 𝑧) |
56 | | simp-4r 537 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → 𝑧 ∈ 𝐴) |
57 | 55, 56 | eqeltrd 2247 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → (𝐶 +R [〈𝑞,
1P〉] ~R ) ∈ 𝐴) |
58 | | simpllr 529 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) |
59 | 58, 55 | breqtrrd 4017 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → (𝐶 +R [〈𝑢,
1P〉] ~R )
<R (𝐶 +R [〈𝑞,
1P〉] ~R
)) |
60 | 2 | ad4antr 491 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → 𝑢 ∈ P) |
61 | | simplr 525 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → 𝑞 ∈ P) |
62 | 44 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → 𝐶 ∈ R) |
63 | | ltpsrprg 7765 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ P ∧
𝑞 ∈ P
∧ 𝐶 ∈
R) → ((𝐶
+R [〈𝑢, 1P〉]
~R ) <R (𝐶 +R [〈𝑞,
1P〉] ~R ) ↔ 𝑢<P
𝑞)) |
64 | 60, 61, 62, 63 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → ((𝐶 +R [〈𝑢,
1P〉] ~R )
<R (𝐶 +R [〈𝑞,
1P〉] ~R ) ↔ 𝑢<P
𝑞)) |
65 | 59, 64 | mpbid 146 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → 𝑢<P 𝑞) |
66 | 57, 65 | jca 304 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧) → ((𝐶 +R [〈𝑞,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑢<P 𝑞)) |
67 | 66 | ex 114 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) ∧ 𝑞 ∈ P) → ((𝐶 +R
[〈𝑞,
1P〉] ~R ) = 𝑧 → ((𝐶 +R [〈𝑞,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑢<P 𝑞))) |
68 | 67 | reximdva 2572 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → (∃𝑞 ∈ P (𝐶 +R [〈𝑞,
1P〉] ~R ) = 𝑧 → ∃𝑞 ∈ P ((𝐶 +R
[〈𝑞,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑢<P 𝑞))) |
69 | 54, 68 | mpd 13 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → ∃𝑞 ∈ P ((𝐶 +R [〈𝑞,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑢<P 𝑞)) |
70 | | opeq1 3765 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑞 → 〈𝑤, 1P〉 =
〈𝑞,
1P〉) |
71 | 70 | eceq1d 6549 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑞 → [〈𝑤, 1P〉]
~R = [〈𝑞, 1P〉]
~R ) |
72 | 71 | oveq2d 5869 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑞 → (𝐶 +R [〈𝑤,
1P〉] ~R ) = (𝐶 +R
[〈𝑞,
1P〉] ~R
)) |
73 | 72 | eleq1d 2239 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑞 → ((𝐶 +R [〈𝑤,
1P〉] ~R ) ∈ 𝐴 ↔ (𝐶 +R [〈𝑞,
1P〉] ~R ) ∈ 𝐴)) |
74 | | suplocsrlem.b |
. . . . . . . . . . 11
⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R
[〈𝑤,
1P〉] ~R ) ∈ 𝐴} |
75 | 73, 74 | elrab2 2889 |
. . . . . . . . . 10
⊢ (𝑞 ∈ 𝐵 ↔ (𝑞 ∈ P ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) ∈ 𝐴)) |
76 | 75 | anbi1i 455 |
. . . . . . . . 9
⊢ ((𝑞 ∈ 𝐵 ∧ 𝑢<P 𝑞) ↔ ((𝑞 ∈ P ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) ∈ 𝐴) ∧ 𝑢<P 𝑞)) |
77 | | anass 399 |
. . . . . . . . 9
⊢ (((𝑞 ∈ P ∧
(𝐶
+R [〈𝑞, 1P〉]
~R ) ∈ 𝐴) ∧ 𝑢<P 𝑞) ↔ (𝑞 ∈ P ∧ ((𝐶 +R
[〈𝑞,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑢<P 𝑞))) |
78 | 76, 77 | bitri 183 |
. . . . . . . 8
⊢ ((𝑞 ∈ 𝐵 ∧ 𝑢<P 𝑞) ↔ (𝑞 ∈ P ∧ ((𝐶 +R
[〈𝑞,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑢<P 𝑞))) |
79 | 78 | rexbii2 2481 |
. . . . . . 7
⊢
(∃𝑞 ∈
𝐵 𝑢<P 𝑞 ↔ ∃𝑞 ∈ P ((𝐶 +R
[〈𝑞,
1P〉] ~R ) ∈ 𝐴 ∧ 𝑢<P 𝑞)) |
80 | 69, 79 | sylibr 133 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ 𝑧 ∈ 𝐴) ∧ (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧) → ∃𝑞 ∈ 𝐵 𝑢<P 𝑞) |
81 | 80 | rexlimdva2 2590 |
. . . . 5
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → (∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 → ∃𝑞 ∈ 𝐵 𝑢<P 𝑞)) |
82 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑧 = (𝐶 +R [〈𝑞,
1P〉] ~R ) → (𝑧 <R
(𝐶
+R [〈𝑣, 1P〉]
~R ) ↔ (𝐶 +R [〈𝑞,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R
))) |
83 | | simplr 525 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R
)) |
84 | | simpr 109 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ 𝐵) |
85 | 84, 75 | sylib 121 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → (𝑞 ∈ P ∧ (𝐶 +R
[〈𝑞,
1P〉] ~R ) ∈ 𝐴)) |
86 | 85 | simprd 113 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → (𝐶 +R [〈𝑞,
1P〉] ~R ) ∈ 𝐴) |
87 | 82, 83, 86 | rspcdva 2839 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → (𝐶 +R [〈𝑞,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R
)) |
88 | 85 | simpld 111 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ P) |
89 | 3 | ad2antrr 485 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → 𝑣 ∈ P) |
90 | 7 | ad2antrr 485 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → 𝐶 ∈ R) |
91 | | ltpsrprg 7765 |
. . . . . . . . 9
⊢ ((𝑞 ∈ P ∧
𝑣 ∈ P
∧ 𝐶 ∈
R) → ((𝐶
+R [〈𝑞, 1P〉]
~R ) <R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑞<P
𝑣)) |
92 | 88, 89, 90, 91 | syl3anc 1233 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → ((𝐶 +R [〈𝑞,
1P〉] ~R )
<R (𝐶 +R [〈𝑣,
1P〉] ~R ) ↔ 𝑞<P
𝑣)) |
93 | 87, 92 | mpbid 146 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑢 ∈ P ∧
𝑣 ∈ P))
∧ 𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) ∧ 𝑞 ∈ 𝐵) → 𝑞<P 𝑣) |
94 | 93 | ralrimiva 2543 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) ∧ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) →
∀𝑞 ∈ 𝐵 𝑞<P 𝑣) |
95 | 94 | ex 114 |
. . . . 5
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → (∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R ) →
∀𝑞 ∈ 𝐵 𝑞<P 𝑣)) |
96 | 81, 95 | orim12d 781 |
. . . 4
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → ((∃𝑧 ∈ 𝐴 (𝐶 +R [〈𝑢,
1P〉] ~R )
<R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R (𝐶 +R
[〈𝑣,
1P〉] ~R )) →
(∃𝑞 ∈ 𝐵 𝑢<P 𝑞 ∨ ∀𝑞 ∈ 𝐵 𝑞<P 𝑣))) |
97 | 42, 96 | mpd 13 |
. . 3
⊢ (((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) ∧
𝑢<P 𝑣) → (∃𝑞 ∈ 𝐵 𝑢<P 𝑞 ∨ ∀𝑞 ∈ 𝐵 𝑞<P 𝑣)) |
98 | 97 | ex 114 |
. 2
⊢ ((𝜑 ∧ (𝑢 ∈ P ∧ 𝑣 ∈ P)) →
(𝑢<P 𝑣 → (∃𝑞 ∈ 𝐵 𝑢<P 𝑞 ∨ ∀𝑞 ∈ 𝐵 𝑞<P 𝑣))) |
99 | 98 | ralrimivva 2552 |
1
⊢ (𝜑 → ∀𝑢 ∈ P ∀𝑣 ∈ P (𝑢<P
𝑣 → (∃𝑞 ∈ 𝐵 𝑢<P 𝑞 ∨ ∀𝑞 ∈ 𝐵 𝑞<P 𝑣))) |