Step | Hyp | Ref
| Expression |
1 | | caucvgprpr.lim |
. . . . 5
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉}〉 |
2 | 1 | caucvgprprlemelu 7648 |
. . . 4
⊢ (𝑡 ∈ (2nd
‘𝐿) ↔ (𝑡 ∈ Q ∧
∃𝑏 ∈
N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) |
3 | 2 | simprbi 273 |
. . 3
⊢ (𝑡 ∈ (2nd
‘𝐿) →
∃𝑏 ∈
N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) |
4 | 3 | adantl 275 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) → ∃𝑏 ∈ N ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) |
5 | | simprr 527 |
. . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) |
6 | | caucvgprpr.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:N⟶P) |
7 | 6 | ffvelrnda 5631 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ N) → (𝐹‘𝑏) ∈ P) |
8 | | recnnpr 7510 |
. . . . . . . . 9
⊢ (𝑏 ∈ N →
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
9 | 8 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ N) → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 ∈
P) |
10 | | addclpr 7499 |
. . . . . . . 8
⊢ (((𝐹‘𝑏) ∈ P ∧ 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉 ∈ P) →
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
11 | 7, 9, 10 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ N) → ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
12 | 11 | ad2ant2r 506 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
13 | 2 | simplbi 272 |
. . . . . . . 8
⊢ (𝑡 ∈ (2nd
‘𝐿) → 𝑡 ∈
Q) |
14 | 13 | ad2antlr 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → 𝑡 ∈
Q) |
15 | | nqprlu 7509 |
. . . . . . 7
⊢ (𝑡 ∈ Q →
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ∈
P) |
16 | 14, 15 | syl 14 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → 〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ∈
P) |
17 | | ltdfpr 7468 |
. . . . . 6
⊢ ((((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P ∧
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ∈ P)
→ (((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ↔ ∃𝑠 ∈ Q (𝑠 ∈ (2nd
‘((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) ∧ 𝑠 ∈ (1st ‘〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)))) |
18 | 12, 16, 17 | syl2anc 409 |
. . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉 ↔ ∃𝑠 ∈ Q (𝑠 ∈ (2nd
‘((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) ∧ 𝑠 ∈ (1st ‘〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)))) |
19 | 5, 18 | mpbid 146 |
. . . 4
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → ∃𝑠 ∈ Q (𝑠 ∈ (2nd
‘((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) ∧ 𝑠 ∈ (1st ‘〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉))) |
20 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) →
𝑠 ∈
Q) |
21 | 12 | adantr 274 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) →
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈
P) |
22 | | nqpru 7514 |
. . . . . . . 8
⊢ ((𝑠 ∈ Q ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) ∈ P) →
(𝑠 ∈ (2nd
‘((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) ↔ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉)) |
23 | 20, 21, 22 | syl2anc 409 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) →
(𝑠 ∈ (2nd
‘((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) ↔ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉)) |
24 | | vex 2733 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
25 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑝 = 𝑠 → (𝑝 <Q 𝑡 ↔ 𝑠 <Q 𝑡)) |
26 | | ltnqex 7511 |
. . . . . . . . . 10
⊢ {𝑝 ∣ 𝑝 <Q 𝑡} ∈ V |
27 | | gtnqex 7512 |
. . . . . . . . . 10
⊢ {𝑞 ∣ 𝑡 <Q 𝑞} ∈ V |
28 | 26, 27 | op1st 6125 |
. . . . . . . . 9
⊢
(1st ‘〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) = {𝑝 ∣ 𝑝 <Q 𝑡} |
29 | 24, 25, 28 | elab2 2878 |
. . . . . . . 8
⊢ (𝑠 ∈ (1st
‘〈{𝑝 ∣
𝑝
<Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) ↔ 𝑠 <Q
𝑡) |
30 | 29 | a1i 9 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) →
(𝑠 ∈ (1st
‘〈{𝑝 ∣
𝑝
<Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉) ↔ 𝑠 <Q
𝑡)) |
31 | 23, 30 | anbi12d 470 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) →
((𝑠 ∈ (2nd
‘((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) ∧ 𝑠 ∈ (1st ‘〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ↔ (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡))) |
32 | 31 | biimpd 143 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) →
((𝑠 ∈ (2nd
‘((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) ∧ 𝑠 ∈ (1st ‘〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡))) |
33 | 32 | reximdva 2572 |
. . . 4
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → (∃𝑠 ∈ Q (𝑠 ∈ (2nd
‘((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) ∧ 𝑠 ∈ (1st ‘〈{𝑝 ∣ 𝑝 <Q 𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → ∃𝑠 ∈ Q (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡))) |
34 | 19, 33 | mpd 13 |
. . 3
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → ∃𝑠 ∈ Q (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡)) |
35 | | simprr 527 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑡 ∈ (2nd
‘𝐿)) ∧ (𝑏 ∈ N ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) ∧
(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡)) → 𝑠 <Q 𝑡) |
36 | | simplr 525 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑡 ∈ (2nd
‘𝐿)) ∧ (𝑏 ∈ N ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) ∧
(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡)) → 𝑠 ∈ Q) |
37 | | simplrl 530 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) →
𝑏 ∈
N) |
38 | 37 | adantr 274 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑡 ∈ (2nd
‘𝐿)) ∧ (𝑏 ∈ N ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) ∧
(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡)) → 𝑏 ∈ N) |
39 | | simprl 526 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑡 ∈ (2nd
‘𝐿)) ∧ (𝑏 ∈ N ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) ∧
(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡)) → ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉) |
40 | | fveq2 5496 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑏 → (𝐹‘𝑟) = (𝐹‘𝑏)) |
41 | | opeq1 3765 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑏 → 〈𝑟, 1o〉 = 〈𝑏,
1o〉) |
42 | 41 | eceq1d 6549 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑏 → [〈𝑟, 1o〉]
~Q = [〈𝑏, 1o〉]
~Q ) |
43 | 42 | fveq2d 5500 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑏 →
(*Q‘[〈𝑟, 1o〉]
~Q ) = (*Q‘[〈𝑏, 1o〉]
~Q )) |
44 | 43 | breq2d 4001 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑏 → (𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q ) ↔ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q ))) |
45 | 44 | abbidv 2288 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑏 → {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )} = {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}) |
46 | 43 | breq1d 3999 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑏 →
((*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞 ↔
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞)) |
47 | 46 | abbidv 2288 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑏 → {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞} = {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}) |
48 | 45, 47 | opeq12d 3773 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑏 → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉) |
49 | 40, 48 | oveq12d 5871 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑏 → ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) = ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)) |
50 | 49 | breq1d 3999 |
. . . . . . . . 9
⊢ (𝑟 = 𝑏 → (((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ↔ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉)) |
51 | 50 | rspcev 2834 |
. . . . . . . 8
⊢ ((𝑏 ∈ N ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉) → ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉) |
52 | 38, 39, 51 | syl2anc 409 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑡 ∈ (2nd
‘𝐿)) ∧ (𝑏 ∈ N ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) ∧
(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡)) → ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉) |
53 | 1 | caucvgprprlemelu 7648 |
. . . . . . 7
⊢ (𝑠 ∈ (2nd
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉)) |
54 | 36, 52, 53 | sylanbrc 415 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑡 ∈ (2nd
‘𝐿)) ∧ (𝑏 ∈ N ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) ∧
(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡)) → 𝑠 ∈ (2nd ‘𝐿)) |
55 | 35, 54 | jca 304 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑡 ∈ (2nd
‘𝐿)) ∧ (𝑏 ∈ N ∧
((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) ∧
(((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡)) → (𝑠 <Q 𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿))) |
56 | 55 | ex 114 |
. . . 4
⊢ ((((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) ∧ 𝑠 ∈ Q) →
((((𝐹‘𝑏) +P
〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡) → (𝑠 <Q 𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿)))) |
57 | 56 | reximdva 2572 |
. . 3
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → (∃𝑠 ∈ Q (((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑠}, {𝑞 ∣ 𝑠 <Q 𝑞}〉 ∧ 𝑠 <Q 𝑡) → ∃𝑠 ∈ Q (𝑠 <Q
𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿)))) |
58 | 34, 57 | mpd 13 |
. 2
⊢ (((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) ∧ (𝑏 ∈ N ∧ ((𝐹‘𝑏) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑏, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑏, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑡}, {𝑞 ∣ 𝑡 <Q 𝑞}〉)) → ∃𝑠 ∈ Q (𝑠 <Q
𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿))) |
59 | 4, 58 | rexlimddv 2592 |
1
⊢ ((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) → ∃𝑠 ∈ Q (𝑠 <Q
𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿))) |