Proof of Theorem cauappcvgprlemladd
Step | Hyp | Ref
| Expression |
1 | | cauappcvgpr.f |
. . . 4
⊢ (𝜑 → 𝐹:Q⟶Q) |
2 | | cauappcvgpr.app |
. . . 4
⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q
𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q
𝑞)))) |
3 | | cauappcvgpr.bnd |
. . . 4
⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) |
4 | | cauappcvgpr.lim |
. . . 4
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q
𝑢}〉 |
5 | | cauappcvgprlemladd.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Q) |
6 | 1, 2, 3, 4, 5 | cauappcvgprlemladdfl 7617 |
. . 3
⊢ (𝜑 → (1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) ⊆
(1st ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)) |
7 | 1, 2, 3, 4, 5 | cauappcvgprlemladdrl 7619 |
. . 3
⊢ (𝜑 → (1st
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉) ⊆ (1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉))) |
8 | 6, 7 | eqssd 3164 |
. 2
⊢ (𝜑 → (1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (1st
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)) |
9 | 1, 2, 3, 4, 5 | cauappcvgprlemladdfu 7616 |
. . 3
⊢ (𝜑 → (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) ⊆
(2nd ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)) |
10 | 1, 2, 3, 4, 5 | cauappcvgprlemladdru 7618 |
. . 3
⊢ (𝜑 → (2nd
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉) ⊆ (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉))) |
11 | 9, 10 | eqssd 3164 |
. 2
⊢ (𝜑 → (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (2nd
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)) |
12 | 1, 2, 3, 4 | cauappcvgprlemcl 7615 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ P) |
13 | | nqprlu 7509 |
. . . . 5
⊢ (𝑆 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉 ∈
P) |
14 | 5, 13 | syl 14 |
. . . 4
⊢ (𝜑 → 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉 ∈
P) |
15 | | addclpr 7499 |
. . . 4
⊢ ((𝐿 ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉 ∈ P)
→ (𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈
P) |
16 | 12, 14, 15 | syl2anc 409 |
. . 3
⊢ (𝜑 → (𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈
P) |
17 | | npsspw 7433 |
. . . . . . 7
⊢
P ⊆ (𝒫 Q × 𝒫
Q) |
18 | 17 | sseli 3143 |
. . . . . 6
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ P
→ (𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ (𝒫
Q × 𝒫 Q)) |
19 | | 1st2nd2 6154 |
. . . . . 6
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ (𝒫
Q × 𝒫 Q) → (𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) = 〈(1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)), (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉))〉) |
20 | 18, 19 | syl 14 |
. . . . 5
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ P
→ (𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) = 〈(1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)), (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉))〉) |
21 | | ssrab2 3232 |
. . . . . . . 8
⊢ {𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)} ⊆
Q |
22 | | nqex 7325 |
. . . . . . . . 9
⊢
Q ∈ V |
23 | 22 | elpw2 4143 |
. . . . . . . 8
⊢ ({𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)} ∈ 𝒫
Q ↔ {𝑙
∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)} ⊆
Q) |
24 | 21, 23 | mpbir 145 |
. . . . . . 7
⊢ {𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)} ∈ 𝒫
Q |
25 | | ssrab2 3232 |
. . . . . . . 8
⊢ {𝑢 ∈ Q ∣
∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢} ⊆ Q |
26 | 22 | elpw2 4143 |
. . . . . . . 8
⊢ ({𝑢 ∈ Q ∣
∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢} ∈ 𝒫 Q ↔
{𝑢 ∈ Q
∣ ∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢} ⊆ Q) |
27 | 25, 26 | mpbir 145 |
. . . . . . 7
⊢ {𝑢 ∈ Q ∣
∃𝑞 ∈
Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢} ∈ 𝒫
Q |
28 | | opelxpi 4643 |
. . . . . . 7
⊢ (({𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)} ∈ 𝒫
Q ∧ {𝑢
∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢} ∈ 𝒫 Q) →
〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉 ∈ (𝒫 Q
× 𝒫 Q)) |
29 | 24, 27, 28 | mp2an 424 |
. . . . . 6
⊢
〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉 ∈ (𝒫 Q
× 𝒫 Q) |
30 | | 1st2nd2 6154 |
. . . . . 6
⊢
(〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉 ∈ (𝒫 Q
× 𝒫 Q) → 〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉 = 〈(1st
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉), (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)〉) |
31 | 29, 30 | mp1i 10 |
. . . . 5
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ P
→ 〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉 = 〈(1st
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉), (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)〉) |
32 | 20, 31 | eqeq12d 2185 |
. . . 4
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ P
→ ((𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) = 〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉 ↔ 〈(1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)), (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉))〉 =
〈(1st ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉), (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)〉)) |
33 | | xp1st 6144 |
. . . . . 6
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ (𝒫
Q × 𝒫 Q) → (1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) ∈ 𝒫
Q) |
34 | 18, 33 | syl 14 |
. . . . 5
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ P
→ (1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) ∈ 𝒫
Q) |
35 | | xp2nd 6145 |
. . . . . 6
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ (𝒫
Q × 𝒫 Q) → (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) ∈ 𝒫
Q) |
36 | 18, 35 | syl 14 |
. . . . 5
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ P
→ (2nd ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) ∈ 𝒫
Q) |
37 | | opthg 4223 |
. . . . 5
⊢
(((1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) ∈ 𝒫
Q ∧ (2nd ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) ∈ 𝒫
Q) → (〈(1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)), (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉))〉 =
〈(1st ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉), (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)〉 ↔ ((1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (1st
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉) ∧ (2nd ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (2nd
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)))) |
38 | 34, 36, 37 | syl2anc 409 |
. . . 4
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ P
→ (〈(1st ‘(𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)), (2nd
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉))〉 =
〈(1st ‘〈{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q
𝑞)
<Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉), (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)〉 ↔ ((1st
‘(𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (1st
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉) ∧ (2nd ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (2nd
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)))) |
39 | 32, 38 | bitrd 187 |
. . 3
⊢ ((𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) ∈ P
→ ((𝐿
+P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) = 〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉 ↔ ((1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (1st
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉) ∧ (2nd ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (2nd
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)))) |
40 | 16, 39 | syl 14 |
. 2
⊢ (𝜑 → ((𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) = 〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉 ↔ ((1st ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (1st
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉) ∧ (2nd ‘(𝐿 +P
〈{𝑙 ∣ 𝑙 <Q
𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉)) = (2nd
‘〈{𝑙 ∈
Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q
((𝐹‘𝑞) +Q
𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉)))) |
41 | 8, 11, 40 | mpbir2and 939 |
1
⊢ (𝜑 → (𝐿 +P 〈{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}〉) = 〈{𝑙 ∈ Q ∣
∃𝑞 ∈
Q (𝑙
+Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q
𝑆)
<Q 𝑢}〉) |