Step | Hyp | Ref
| Expression |
1 | | 1pi 6505 |
. . . . 5
⊢
1𝑜 ∈ N |
2 | | caucvgprpr.bnd |
. . . . 5
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) |
3 | | fveq2 5198 |
. . . . . . 7
⊢ (𝑚 = 1𝑜 →
(𝐹‘𝑚) = (𝐹‘1𝑜)) |
4 | 3 | breq2d 3797 |
. . . . . 6
⊢ (𝑚 = 1𝑜 →
(𝐴<P (𝐹‘𝑚) ↔ 𝐴<P (𝐹‘1𝑜))) |
5 | 4 | rspcv 2697 |
. . . . 5
⊢
(1𝑜 ∈ N → (∀𝑚 ∈ N 𝐴<P
(𝐹‘𝑚) → 𝐴<P (𝐹‘1𝑜))) |
6 | 1, 2, 5 | mpsyl 64 |
. . . 4
⊢ (𝜑 → 𝐴<P (𝐹‘1𝑜)) |
7 | | ltrelpr 6695 |
. . . . . 6
⊢
<P ⊆ (P ×
P) |
8 | 7 | brel 4410 |
. . . . 5
⊢ (𝐴<P
(𝐹‘1𝑜) → (𝐴 ∈ P ∧
(𝐹‘1𝑜) ∈
P)) |
9 | 8 | simpld 110 |
. . . 4
⊢ (𝐴<P
(𝐹‘1𝑜) → 𝐴 ∈
P) |
10 | 6, 9 | syl 14 |
. . 3
⊢ (𝜑 → 𝐴 ∈ P) |
11 | | prop 6665 |
. . . 4
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
12 | | prml 6667 |
. . . 4
⊢
(〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P →
∃𝑥 ∈
Q 𝑥 ∈
(1st ‘𝐴)) |
13 | 11, 12 | syl 14 |
. . 3
⊢ (𝐴 ∈ P →
∃𝑥 ∈
Q 𝑥 ∈
(1st ‘𝐴)) |
14 | 10, 13 | syl 14 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ Q 𝑥 ∈ (1st ‘𝐴)) |
15 | | subhalfnqq 6604 |
. . . 4
⊢ (𝑥 ∈ Q →
∃𝑠 ∈
Q (𝑠
+Q 𝑠) <Q 𝑥) |
16 | 15 | ad2antrl 473 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) →
∃𝑠 ∈
Q (𝑠
+Q 𝑠) <Q 𝑥) |
17 | | simplr 496 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) → 𝑠 ∈ Q) |
18 | | archrecnq 6853 |
. . . . . . . 8
⊢ (𝑠 ∈ Q →
∃𝑟 ∈
N (*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) |
19 | 17, 18 | syl 14 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) → ∃𝑟 ∈ N
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) |
20 | | simpr 108 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) →
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) |
21 | | simplr 496 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → 𝑟 ∈ N) |
22 | | nnnq 6612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ N →
[〈𝑟,
1𝑜〉] ~Q ∈
Q) |
23 | | recclnq 6582 |
. . . . . . . . . . . . . . . 16
⊢
([〈𝑟,
1𝑜〉] ~Q ∈ Q
→ (*Q‘[〈𝑟, 1𝑜〉]
~Q ) ∈ Q) |
24 | 21, 22, 23 | 3syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) →
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) ∈ Q) |
25 | 17 | ad2antrr 471 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → 𝑠 ∈ Q) |
26 | | ltanqg 6590 |
. . . . . . . . . . . . . . 15
⊢
(((*Q‘[〈𝑟, 1𝑜〉]
~Q ) ∈ Q ∧ 𝑠 ∈ Q ∧ 𝑠 ∈ Q) →
((*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠 ↔ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q (𝑠 +Q
𝑠))) |
27 | 24, 25, 25, 26 | syl3anc 1169 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) →
((*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠 ↔ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q (𝑠 +Q
𝑠))) |
28 | 20, 27 | mpbid 145 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q (𝑠 +Q
𝑠)) |
29 | | simpllr 500 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → (𝑠 +Q 𝑠) <Q
𝑥) |
30 | | ltsonq 6588 |
. . . . . . . . . . . . . 14
⊢
<Q Or Q |
31 | | ltrelnq 6555 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
32 | 30, 31 | sotri 4740 |
. . . . . . . . . . . . 13
⊢ (((𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q (𝑠 +Q
𝑠) ∧ (𝑠 +Q
𝑠)
<Q 𝑥) → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑥) |
33 | 28, 29, 32 | syl2anc 403 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑥) |
34 | 10 | ad5antr 479 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → 𝐴 ∈ P) |
35 | | simprr 498 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) → 𝑥 ∈ (1st
‘𝐴)) |
36 | 35 | ad4antr 477 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → 𝑥 ∈ (1st ‘𝐴)) |
37 | | prcdnql 6674 |
. . . . . . . . . . . . . 14
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑥 ∈ (1st
‘𝐴)) → ((𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑥 → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ (1st ‘𝐴))) |
38 | 11, 37 | sylan 277 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ (1st
‘𝐴)) → ((𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑥 → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ (1st ‘𝐴))) |
39 | 34, 36, 38 | syl2anc 403 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → ((𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑥 → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ (1st ‘𝐴))) |
40 | 33, 39 | mpd 13 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ (1st ‘𝐴)) |
41 | | addclnq 6565 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈ Q ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) ∈ Q) → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ Q) |
42 | 25, 24, 41 | syl2anc 403 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ Q) |
43 | | nqprl 6741 |
. . . . . . . . . . . 12
⊢ (((𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ Q ∧ 𝐴 ∈ P) → ((𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ (1st ‘𝐴) ↔ 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P 𝐴)) |
44 | 42, 34, 43 | syl2anc 403 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → ((𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ∈ (1st ‘𝐴) ↔ 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P 𝐴)) |
45 | 40, 44 | mpbid 145 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P 𝐴) |
46 | 2 | ad5antr 479 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) |
47 | | fveq2 5198 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑟 → (𝐹‘𝑚) = (𝐹‘𝑟)) |
48 | 47 | breq2d 3797 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑟 → (𝐴<P (𝐹‘𝑚) ↔ 𝐴<P (𝐹‘𝑟))) |
49 | 48 | rspcv 2697 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ N →
(∀𝑚 ∈
N 𝐴<P (𝐹‘𝑚) → 𝐴<P (𝐹‘𝑟))) |
50 | 21, 46, 49 | sylc 61 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → 𝐴<P (𝐹‘𝑟)) |
51 | | ltsopr 6786 |
. . . . . . . . . . 11
⊢
<P Or P |
52 | 51, 7 | sotri 4740 |
. . . . . . . . . 10
⊢
((〈{𝑝 ∣
𝑝
<Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P 𝐴 ∧ 𝐴<P (𝐹‘𝑟)) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)) |
53 | 45, 50, 52 | syl2anc 403 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) ∧
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)) |
54 | 53 | ex 113 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ Q ∧
𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) ∧ 𝑟 ∈ N) →
((*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠 → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟))) |
55 | 54 | reximdva 2463 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) → (∃𝑟 ∈ N
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑠 → ∃𝑟 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟))) |
56 | 19, 55 | mpd 13 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) → ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑠
+Q (*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)) |
57 | | oveq1 5539 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑠 → (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) = (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))) |
58 | 57 | breq2d 3797 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑠 → (𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) ↔ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )))) |
59 | 58 | abbidv 2196 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑠 → {𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}) |
60 | 57 | breq1d 3795 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑠 → ((𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞 ↔ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞)) |
61 | 60 | abbidv 2196 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑠 → {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞} = {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}) |
62 | 59, 61 | opeq12d 3578 |
. . . . . . . . 9
⊢ (𝑙 = 𝑠 → 〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉) |
63 | 62 | breq1d 3795 |
. . . . . . . 8
⊢ (𝑙 = 𝑠 → (〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟) ↔ 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟))) |
64 | 63 | rexbidv 2369 |
. . . . . . 7
⊢ (𝑙 = 𝑠 → (∃𝑟 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟) ↔ ∃𝑟 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟))) |
65 | | caucvgprpr.lim |
. . . . . . . . 9
⊢ 𝐿 = 〈{𝑙 ∈ 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 𝑞}〉}〉 |
66 | 65 | fveq2i 5201 |
. . . . . . . 8
⊢
(1st ‘𝐿) = (1st ‘〈{𝑙 ∈ 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 𝑞}〉}〉) |
67 | | nqex 6553 |
. . . . . . . . . 10
⊢
Q ∈ V |
68 | 67 | rabex 3922 |
. . . . . . . . 9
⊢ {𝑙 ∈ Q ∣
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} ∈ V |
69 | 67 | rabex 3922 |
. . . . . . . . 9
⊢ {𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1𝑜〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} ∈
V |
70 | 68, 69 | op1st 5793 |
. . . . . . . 8
⊢
(1st ‘〈{𝑙 ∈ 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 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} |
71 | 66, 70 | eqtri 2101 |
. . . . . . 7
⊢
(1st ‘𝐿) = {𝑙 ∈ Q ∣ ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} |
72 | 64, 71 | elrab2 2751 |
. . . . . 6
⊢ (𝑠 ∈ (1st
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1𝑜〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟))) |
73 | 17, 56, 72 | sylanbrc 408 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) ∧
(𝑠
+Q 𝑠) <Q 𝑥) → 𝑠 ∈ (1st ‘𝐿)) |
74 | 73 | ex 113 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) ∧ 𝑠 ∈ Q) →
((𝑠
+Q 𝑠) <Q 𝑥 → 𝑠 ∈ (1st ‘𝐿))) |
75 | 74 | reximdva 2463 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) →
(∃𝑠 ∈
Q (𝑠
+Q 𝑠) <Q 𝑥 → ∃𝑠 ∈ Q 𝑠 ∈ (1st
‘𝐿))) |
76 | 16, 75 | mpd 13 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ Q ∧ 𝑥 ∈ (1st
‘𝐴))) →
∃𝑠 ∈
Q 𝑠 ∈
(1st ‘𝐿)) |
77 | 14, 76 | rexlimddv 2481 |
1
⊢ (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿)) |