Step | Hyp | Ref
| Expression |
1 | | caucvgprpr.f |
. . . 4
⊢ (𝜑 → 𝐹:N⟶P) |
2 | | 1pi 6505 |
. . . . 5
⊢
1𝑜 ∈ N |
3 | 2 | a1i 9 |
. . . 4
⊢ (𝜑 → 1𝑜
∈ N) |
4 | 1, 3 | ffvelrnd 5324 |
. . 3
⊢ (𝜑 → (𝐹‘1𝑜) ∈
P) |
5 | | prop 6665 |
. . 3
⊢ ((𝐹‘1𝑜)
∈ P → 〈(1st ‘(𝐹‘1𝑜)),
(2nd ‘(𝐹‘1𝑜))〉 ∈
P) |
6 | | prmu 6668 |
. . 3
⊢
(〈(1st ‘(𝐹‘1𝑜)),
(2nd ‘(𝐹‘1𝑜))〉 ∈
P → ∃𝑥 ∈ Q 𝑥 ∈ (2nd ‘(𝐹‘1𝑜))) |
7 | 4, 5, 6 | 3syl 17 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ Q 𝑥 ∈ (2nd ‘(𝐹‘1𝑜))) |
8 | | simprl 497 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
𝑥 ∈
Q) |
9 | | 1nq 6556 |
. . . 4
⊢
1Q ∈ Q |
10 | | addclnq 6565 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
1Q ∈ Q) → (𝑥 +Q
1Q) ∈ Q) |
11 | 8, 9, 10 | sylancl 404 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
(𝑥
+Q 1Q) ∈
Q) |
12 | 2 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
1𝑜 ∈ N) |
13 | | simprr 498 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
𝑥 ∈ (2nd
‘(𝐹‘1𝑜))) |
14 | 4 | adantr 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
(𝐹‘1𝑜) ∈
P) |
15 | | nqpru 6742 |
. . . . . . . . 9
⊢ ((𝑥 ∈ Q ∧
(𝐹‘1𝑜) ∈
P) → (𝑥
∈ (2nd ‘(𝐹‘1𝑜)) ↔ (𝐹‘1𝑜)<P
〈{𝑝 ∣ 𝑝 <Q 𝑥}, {𝑞
∣ 𝑥 <Q
𝑞}〉)) |
16 | 8, 14, 15 | syl2anc 403 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
(𝑥 ∈ (2nd
‘(𝐹‘1𝑜)) ↔ (𝐹‘1𝑜)<P
〈{𝑝 ∣ 𝑝 <Q 𝑥}, {𝑞
∣ 𝑥 <Q
𝑞}〉)) |
17 | 13, 16 | mpbid 145 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
(𝐹‘1𝑜)<P
〈{𝑝 ∣ 𝑝 <Q 𝑥}, {𝑞
∣ 𝑥 <Q
𝑞}〉) |
18 | | ltaprg 6809 |
. . . . . . . . 9
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P
∧ ℎ ∈
P) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
19 | 18 | adantl 271 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P ∧ ℎ
∈ P)) → (𝑓<P 𝑔 ↔ (ℎ +P 𝑓)<P
(ℎ
+P 𝑔))) |
20 | | nqprlu 6737 |
. . . . . . . . 9
⊢ (𝑥 ∈ Q →
〈{𝑝 ∣ 𝑝 <Q
𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉 ∈
P) |
21 | 8, 20 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
〈{𝑝 ∣ 𝑝 <Q
𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉 ∈
P) |
22 | | nqprlu 6737 |
. . . . . . . . 9
⊢
(1Q ∈ Q → 〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉 ∈
P) |
23 | 9, 22 | mp1i 10 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉 ∈
P) |
24 | | addcomprg 6768 |
. . . . . . . . 9
⊢ ((𝑓 ∈ P ∧
𝑔 ∈ P)
→ (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
25 | 24 | adantl 271 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) ∧
(𝑓 ∈ P
∧ 𝑔 ∈
P)) → (𝑓
+P 𝑔) = (𝑔 +P 𝑓)) |
26 | 19, 14, 21, 23, 25 | caovord2d 5690 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
((𝐹‘1𝑜)<P
〈{𝑝 ∣ 𝑝 <Q 𝑥}, {𝑞
∣ 𝑥 <Q
𝑞}〉 ↔ ((𝐹‘1𝑜) +P
〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣
1Q <Q 𝑞}〉)<P (〈{𝑝 ∣ 𝑝 <Q 𝑥}, {𝑞
∣ 𝑥 <Q
𝑞}〉 +P
〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣
1Q <Q 𝑞}〉))) |
27 | 17, 26 | mpbid 145 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉)<P
(〈{𝑝 ∣ 𝑝 <Q
𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉)) |
28 | | df-1nqqs 6541 |
. . . . . . . . . . . . 13
⊢
1Q = [〈1𝑜,
1𝑜〉] ~Q |
29 | 28 | fveq2i 5201 |
. . . . . . . . . . . 12
⊢
(*Q‘1Q) =
(*Q‘[〈1𝑜,
1𝑜〉] ~Q ) |
30 | | rec1nq 6585 |
. . . . . . . . . . . 12
⊢
(*Q‘1Q) =
1Q |
31 | 29, 30 | eqtr3i 2103 |
. . . . . . . . . . 11
⊢
(*Q‘[〈1𝑜,
1𝑜〉] ~Q ) =
1Q |
32 | 31 | breq2i 3793 |
. . . . . . . . . 10
⊢ (𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q ) ↔ 𝑝 <Q
1Q) |
33 | 32 | abbii 2194 |
. . . . . . . . 9
⊢ {𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )} = {𝑝 ∣ 𝑝 <Q
1Q} |
34 | 31 | breq1i 3792 |
. . . . . . . . . 10
⊢
((*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞 ↔ 1Q
<Q 𝑞) |
35 | 34 | abbii 2194 |
. . . . . . . . 9
⊢ {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞} = {𝑞 ∣ 1Q
<Q 𝑞} |
36 | 33, 35 | opeq12i 3575 |
. . . . . . . 8
⊢
〈{𝑝 ∣
𝑝
<Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}, {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉 |
37 | 36 | oveq2i 5543 |
. . . . . . 7
⊢ ((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}, {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}〉) = ((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉) |
38 | 37 | a1i 9 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}, {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}〉) = ((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉)) |
39 | | addnqpr 6751 |
. . . . . . 7
⊢ ((𝑥 ∈ Q ∧
1Q ∈ Q) → 〈{𝑝 ∣ 𝑝 <Q (𝑥 +Q
1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉 = (〈{𝑝 ∣ 𝑝 <Q 𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉)) |
40 | 8, 9, 39 | sylancl 404 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉 = (〈{𝑝 ∣ 𝑝 <Q 𝑥}, {𝑞 ∣ 𝑥 <Q 𝑞}〉
+P 〈{𝑝 ∣ 𝑝 <Q
1Q}, {𝑞 ∣ 1Q
<Q 𝑞}〉)) |
41 | 27, 38, 40 | 3brtr4d 3815 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}, {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉) |
42 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑟 = 1𝑜 →
(𝐹‘𝑟) = (𝐹‘1𝑜)) |
43 | | opeq1 3570 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 1𝑜 →
〈𝑟,
1𝑜〉 = 〈1𝑜,
1𝑜〉) |
44 | 43 | eceq1d 6165 |
. . . . . . . . . . . 12
⊢ (𝑟 = 1𝑜 →
[〈𝑟,
1𝑜〉] ~Q =
[〈1𝑜, 1𝑜〉]
~Q ) |
45 | 44 | fveq2d 5202 |
. . . . . . . . . . 11
⊢ (𝑟 = 1𝑜 →
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) =
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )) |
46 | 45 | breq2d 3797 |
. . . . . . . . . 10
⊢ (𝑟 = 1𝑜 →
(𝑝
<Q (*Q‘[〈𝑟, 1𝑜〉]
~Q ) ↔ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q ))) |
47 | 46 | abbidv 2196 |
. . . . . . . . 9
⊢ (𝑟 = 1𝑜 →
{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )} = {𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}) |
48 | 45 | breq1d 3795 |
. . . . . . . . . 10
⊢ (𝑟 = 1𝑜 →
((*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞 ↔
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞)) |
49 | 48 | abbidv 2196 |
. . . . . . . . 9
⊢ (𝑟 = 1𝑜 →
{𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞} = {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}) |
50 | 47, 49 | opeq12d 3578 |
. . . . . . . 8
⊢ (𝑟 = 1𝑜 →
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}, {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}〉) |
51 | 42, 50 | oveq12d 5550 |
. . . . . . 7
⊢ (𝑟 = 1𝑜 →
((𝐹‘𝑟) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉) = ((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}, {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}〉)) |
52 | 51 | breq1d 3795 |
. . . . . 6
⊢ (𝑟 = 1𝑜 →
(((𝐹‘𝑟) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉 ↔ ((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}, {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉)) |
53 | 52 | rspcev 2701 |
. . . . 5
⊢
((1𝑜 ∈ N ∧ ((𝐹‘1𝑜)
+P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )}, {𝑞 ∣
(*Q‘[〈1𝑜,
1𝑜〉] ~Q )
<Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉) → ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉) |
54 | 12, 41, 53 | syl2anc 403 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉) |
55 | | breq2 3789 |
. . . . . . . . 9
⊢ (𝑢 = (𝑥 +Q
1Q) → (𝑝 <Q 𝑢 ↔ 𝑝 <Q (𝑥 +Q
1Q))) |
56 | 55 | abbidv 2196 |
. . . . . . . 8
⊢ (𝑢 = (𝑥 +Q
1Q) → {𝑝 ∣ 𝑝 <Q 𝑢} = {𝑝 ∣ 𝑝 <Q (𝑥 +Q
1Q)}) |
57 | | breq1 3788 |
. . . . . . . . 9
⊢ (𝑢 = (𝑥 +Q
1Q) → (𝑢 <Q 𝑞 ↔ (𝑥 +Q
1Q) <Q 𝑞)) |
58 | 57 | abbidv 2196 |
. . . . . . . 8
⊢ (𝑢 = (𝑥 +Q
1Q) → {𝑞 ∣ 𝑢 <Q 𝑞} = {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}) |
59 | 56, 58 | opeq12d 3578 |
. . . . . . 7
⊢ (𝑢 = (𝑥 +Q
1Q) → 〈{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q (𝑥 +Q
1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉) |
60 | 59 | breq2d 3797 |
. . . . . 6
⊢ (𝑢 = (𝑥 +Q
1Q) → (((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 ↔ ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉)) |
61 | 60 | rexbidv 2369 |
. . . . 5
⊢ (𝑢 = (𝑥 +Q
1Q) → (∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 ↔ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉)) |
62 | | caucvgprpr.lim |
. . . . . . 7
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉}〉 |
63 | 62 | fveq2i 5201 |
. . . . . 6
⊢
(2nd ‘𝐿) = (2nd ‘〈{𝑙 ∈ Q ∣
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉}〉) |
64 | | nqex 6553 |
. . . . . . . 8
⊢
Q ∈ V |
65 | 64 | rabex 3922 |
. . . . . . 7
⊢ {𝑙 ∈ Q ∣
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} ∈ V |
66 | 64 | rabex 3922 |
. . . . . . 7
⊢ {𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} ∈
V |
67 | 65, 66 | op2nd 5794 |
. . . . . 6
⊢
(2nd ‘〈{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉}〉) = {𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} |
68 | 63, 67 | eqtri 2101 |
. . . . 5
⊢
(2nd ‘𝐿) = {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} |
69 | 61, 68 | elrab2 2751 |
. . . 4
⊢ ((𝑥 +Q
1Q) ∈ (2nd ‘𝐿) ↔ ((𝑥 +Q
1Q) ∈ Q ∧ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
(𝑥
+Q 1Q)}, {𝑞 ∣ (𝑥 +Q
1Q) <Q 𝑞}〉)) |
70 | 11, 54, 69 | sylanbrc 408 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
(𝑥
+Q 1Q) ∈ (2nd
‘𝐿)) |
71 | | eleq1 2141 |
. . . 4
⊢ (𝑡 = (𝑥 +Q
1Q) → (𝑡 ∈ (2nd ‘𝐿) ↔ (𝑥 +Q
1Q) ∈ (2nd ‘𝐿))) |
72 | 71 | rspcev 2701 |
. . 3
⊢ (((𝑥 +Q
1Q) ∈ Q ∧ (𝑥 +Q
1Q) ∈ (2nd ‘𝐿)) → ∃𝑡 ∈ Q 𝑡 ∈ (2nd ‘𝐿)) |
73 | 11, 70, 72 | syl2anc 403 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (2nd
‘(𝐹‘1𝑜)))) →
∃𝑡 ∈
Q 𝑡 ∈
(2nd ‘𝐿)) |
74 | 7, 73 | rexlimddv 2481 |
1
⊢ (𝜑 → ∃𝑡 ∈ Q 𝑡 ∈ (2nd ‘𝐿)) |