Step | Hyp | Ref
| Expression |
1 | | caucvgprpr.f |
. . . 4
⊢ (𝜑 → 𝐹:N⟶P) |
2 | | caucvgprpr.cau |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉)))) |
3 | | caucvgprpr.bnd |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) |
4 | | caucvgprpr.lim |
. . . 4
⊢ 𝐿 = 〈{𝑙 ∈ 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 𝑞}〉}〉 |
5 | 1, 2, 3, 4 | caucvgprprlemm 7616 |
. . 3
⊢ (𝜑 → (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑡 ∈ Q 𝑡 ∈ (2nd
‘𝐿))) |
6 | | ssrab2 3213 |
. . . . . 6
⊢ {𝑙 ∈ Q ∣
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} ⊆ Q |
7 | | nqex 7283 |
. . . . . . 7
⊢
Q ∈ V |
8 | 7 | elpw2 4118 |
. . . . . 6
⊢ ({𝑙 ∈ Q ∣
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} ∈ 𝒫 Q ↔
{𝑙 ∈ Q
∣ ∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} ⊆ Q) |
9 | 6, 8 | mpbir 145 |
. . . . 5
⊢ {𝑙 ∈ Q ∣
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} ∈ 𝒫
Q |
10 | | ssrab2 3213 |
. . . . . 6
⊢ {𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} ⊆
Q |
11 | 7 | elpw2 4118 |
. . . . . 6
⊢ ({𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} ∈ 𝒫
Q ↔ {𝑢
∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} ⊆
Q) |
12 | 10, 11 | mpbir 145 |
. . . . 5
⊢ {𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} ∈ 𝒫
Q |
13 | | opelxpi 4618 |
. . . . 5
⊢ (({𝑙 ∈ Q ∣
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)} ∈ 𝒫 Q ∧
{𝑢 ∈ Q
∣ ∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} ∈ 𝒫
Q) → 〈{𝑙 ∈ 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 𝑞}〉}〉 ∈ (𝒫
Q × 𝒫 Q)) |
14 | 9, 12, 13 | mp2an 423 |
. . . 4
⊢
〈{𝑙 ∈
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 𝑞}〉}〉 ∈ (𝒫
Q × 𝒫 Q) |
15 | 4, 14 | eqeltri 2230 |
. . 3
⊢ 𝐿 ∈ (𝒫
Q × 𝒫 Q) |
16 | 5, 15 | jctil 310 |
. 2
⊢ (𝜑 → (𝐿 ∈ (𝒫 Q ×
𝒫 Q) ∧ (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑡 ∈ Q 𝑡 ∈ (2nd
‘𝐿)))) |
17 | 1, 2, 3, 4 | caucvgprprlemrnd 7621 |
. . 3
⊢ (𝜑 → (∀𝑠 ∈ Q (𝑠 ∈ (1st
‘𝐿) ↔
∃𝑡 ∈
Q (𝑠
<Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿))) ∧ ∀𝑡 ∈ Q (𝑡 ∈ (2nd
‘𝐿) ↔
∃𝑠 ∈
Q (𝑠
<Q 𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿))))) |
18 | 1, 2, 3, 4 | caucvgprprlemdisj 7622 |
. . 3
⊢ (𝜑 → ∀𝑠 ∈ Q ¬ (𝑠 ∈ (1st
‘𝐿) ∧ 𝑠 ∈ (2nd
‘𝐿))) |
19 | 1, 2, 3, 4 | caucvgprprlemloc 7623 |
. . 3
⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑡 ∈ Q (𝑠 <Q
𝑡 → (𝑠 ∈ (1st
‘𝐿) ∨ 𝑡 ∈ (2nd
‘𝐿)))) |
20 | 17, 18, 19 | 3jca 1162 |
. 2
⊢ (𝜑 → ((∀𝑠 ∈ Q (𝑠 ∈ (1st
‘𝐿) ↔
∃𝑡 ∈
Q (𝑠
<Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿))) ∧ ∀𝑡 ∈ Q (𝑡 ∈ (2nd
‘𝐿) ↔
∃𝑠 ∈
Q (𝑠
<Q 𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿)))) ∧ ∀𝑠 ∈ Q ¬
(𝑠 ∈ (1st
‘𝐿) ∧ 𝑠 ∈ (2nd
‘𝐿)) ∧
∀𝑠 ∈
Q ∀𝑡
∈ Q (𝑠
<Q 𝑡 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))))) |
21 | | elnp1st2nd 7396 |
. 2
⊢ (𝐿 ∈ P ↔
((𝐿 ∈ (𝒫
Q × 𝒫 Q) ∧ (∃𝑠 ∈ Q 𝑠 ∈ (1st
‘𝐿) ∧
∃𝑡 ∈
Q 𝑡 ∈
(2nd ‘𝐿)))
∧ ((∀𝑠 ∈
Q (𝑠 ∈
(1st ‘𝐿)
↔ ∃𝑡 ∈
Q (𝑠
<Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿))) ∧ ∀𝑡 ∈ Q (𝑡 ∈ (2nd
‘𝐿) ↔
∃𝑠 ∈
Q (𝑠
<Q 𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿)))) ∧ ∀𝑠 ∈ Q ¬
(𝑠 ∈ (1st
‘𝐿) ∧ 𝑠 ∈ (2nd
‘𝐿)) ∧
∀𝑠 ∈
Q ∀𝑡
∈ Q (𝑠
<Q 𝑡 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿)))))) |
22 | 16, 20, 21 | sylanbrc 414 |
1
⊢ (𝜑 → 𝐿 ∈ P) |