Proof of Theorem caucvgprlemdisj
Step | Hyp | Ref
| Expression |
1 | | oveq1 5462 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑠 → (𝑙 +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) = (𝑠 +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q ))) |
2 | 1 | breq1d 3765 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑠 → ((𝑙 +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗) ↔ (𝑠 +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗))) |
3 | 2 | rexbidv 2321 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑠 → (∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗) ↔ ∃𝑗 ∈
N (𝑠
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗))) |
4 | | caucvgpr.lim |
. . . . . . . . . . . 12
⊢ 𝐿 = 〈{𝑙 ∈
Q ∣ ∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)}, {u
∈ Q ∣ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u}〉 |
5 | 4 | fveq2i 5124 |
. . . . . . . . . . 11
⊢
(1st ‘𝐿) = (1st ‘〈{𝑙 ∈ Q ∣ ∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)}, {u
∈ Q ∣ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u}〉) |
6 | | nqex 6347 |
. . . . . . . . . . . . 13
⊢
Q ∈ V |
7 | 6 | rabex 3892 |
. . . . . . . . . . . 12
⊢ {𝑙 ∈ Q ∣ ∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)} ∈
V |
8 | 6 | rabex 3892 |
. . . . . . . . . . . 12
⊢ {u ∈
Q ∣ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u} ∈
V |
9 | 7, 8 | op1st 5715 |
. . . . . . . . . . 11
⊢
(1st ‘〈{𝑙 ∈
Q ∣ ∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)}, {u
∈ Q ∣ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u}〉) = {𝑙 ∈
Q ∣ ∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)} |
10 | 5, 9 | eqtri 2057 |
. . . . . . . . . 10
⊢
(1st ‘𝐿) = {𝑙 ∈
Q ∣ ∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)} |
11 | 3, 10 | elrab2 2694 |
. . . . . . . . 9
⊢ (𝑠 ∈ (1st ‘𝐿) ↔ (𝑠 ∈
Q ∧ ∃𝑗 ∈
N (𝑠
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗))) |
12 | 11 | simprbi 260 |
. . . . . . . 8
⊢ (𝑠 ∈ (1st ‘𝐿) → ∃𝑗 ∈
N (𝑠
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)) |
13 | | opeq1 3540 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → 〈𝑗, 1𝑜〉 = 〈𝑘,
1𝑜〉) |
14 | 13 | eceq1d 6078 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → [〈𝑗, 1𝑜〉]
~Q = [〈𝑘, 1𝑜〉]
~Q ) |
15 | 14 | fveq2d 5125 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 →
(*Q‘[〈𝑗, 1𝑜〉]
~Q ) = (*Q‘[〈𝑘, 1𝑜〉]
~Q )) |
16 | 15 | oveq2d 5471 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑠 +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) = (𝑠 +Q
(*Q‘[〈𝑘, 1𝑜〉]
~Q ))) |
17 | | fveq2 5121 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘)) |
18 | 16, 17 | breq12d 3768 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑠 +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗) ↔ (𝑠 +Q
(*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘))) |
19 | 18 | cbvrexv 2528 |
. . . . . . . 8
⊢ (∃𝑗 ∈
N (𝑠
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗) ↔ ∃𝑘 ∈
N (𝑠
+Q (*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘)) |
20 | 12, 19 | sylib 127 |
. . . . . . 7
⊢ (𝑠 ∈ (1st ‘𝐿) → ∃𝑘 ∈
N (𝑠
+Q (*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘)) |
21 | | breq2 3759 |
. . . . . . . . . 10
⊢ (u = 𝑠 → (((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u ↔ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠)) |
22 | 21 | rexbidv 2321 |
. . . . . . . . 9
⊢ (u = 𝑠 → (∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u ↔ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠)) |
23 | 4 | fveq2i 5124 |
. . . . . . . . . 10
⊢
(2nd ‘𝐿) = (2nd ‘〈{𝑙 ∈ Q ∣ ∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)}, {u
∈ Q ∣ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u}〉) |
24 | 7, 8 | op2nd 5716 |
. . . . . . . . . 10
⊢
(2nd ‘〈{𝑙 ∈
Q ∣ ∃𝑗 ∈
N (𝑙
+Q (*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q (𝐹‘𝑗)}, {u
∈ Q ∣ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u}〉) = {u
∈ Q ∣ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u} |
25 | 23, 24 | eqtri 2057 |
. . . . . . . . 9
⊢
(2nd ‘𝐿) = {u
∈ Q ∣ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q u} |
26 | 22, 25 | elrab2 2694 |
. . . . . . . 8
⊢ (𝑠 ∈ (2nd ‘𝐿) ↔ (𝑠 ∈
Q ∧ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠)) |
27 | 26 | simprbi 260 |
. . . . . . 7
⊢ (𝑠 ∈ (2nd ‘𝐿) → ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠) |
28 | 20, 27 | anim12i 321 |
. . . . . 6
⊢ ((𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿)) → (∃𝑘 ∈
N (𝑠
+Q (*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘) ∧ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠)) |
29 | | reeanv 2473 |
. . . . . 6
⊢ (∃𝑘 ∈
N ∃𝑗 ∈
N ((𝑠
+Q (*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠) ↔ (∃𝑘 ∈
N (𝑠
+Q (*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘) ∧ ∃𝑗 ∈
N ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠)) |
30 | 28, 29 | sylibr 137 |
. . . . 5
⊢ ((𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿)) → ∃𝑘 ∈
N ∃𝑗 ∈
N ((𝑠
+Q (*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠)) |
31 | 30 | adantl 262 |
. . . 4
⊢ ((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) → ∃𝑘 ∈
N ∃𝑗 ∈
N ((𝑠
+Q (*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠)) |
32 | | caucvgpr.f |
. . . . . . . 8
⊢ (φ → 𝐹:N⟶Q) |
33 | 32 | ad2antrr 457 |
. . . . . . 7
⊢ (((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧
(𝑘 ∈ N ∧ 𝑗
∈ N)) → 𝐹:N⟶Q) |
34 | | caucvgpr.cau |
. . . . . . . 8
⊢ (φ → ∀𝑛 ∈
N ∀𝑘 ∈
N (𝑛
<N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q
(*Q‘[〈𝑛, 1𝑜〉]
~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q
(*Q‘[〈𝑛, 1𝑜〉]
~Q ))))) |
35 | 34 | ad2antrr 457 |
. . . . . . 7
⊢ (((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧
(𝑘 ∈ N ∧ 𝑗
∈ N)) → ∀𝑛 ∈
N ∀𝑘 ∈
N (𝑛
<N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q
(*Q‘[〈𝑛, 1𝑜〉]
~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q
(*Q‘[〈𝑛, 1𝑜〉]
~Q ))))) |
36 | | simprl 483 |
. . . . . . 7
⊢ (((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧
(𝑘 ∈ N ∧ 𝑗
∈ N)) → 𝑘 ∈
N) |
37 | | simprr 484 |
. . . . . . 7
⊢ (((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧
(𝑘 ∈ N ∧ 𝑗
∈ N)) → 𝑗 ∈
N) |
38 | 11 | simplbi 259 |
. . . . . . . . 9
⊢ (𝑠 ∈ (1st ‘𝐿) → 𝑠 ∈
Q) |
39 | 38 | ad2antrl 459 |
. . . . . . . 8
⊢ ((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) → 𝑠 ∈
Q) |
40 | 39 | adantr 261 |
. . . . . . 7
⊢ (((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧
(𝑘 ∈ N ∧ 𝑗
∈ N)) → 𝑠 ∈
Q) |
41 | 33, 35, 36, 37, 40 | caucvgprlemnkj 6637 |
. . . . . 6
⊢ (((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧
(𝑘 ∈ N ∧ 𝑗
∈ N)) → ¬ ((𝑠 +Q
(*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠)) |
42 | 41 | pm2.21d 549 |
. . . . 5
⊢ (((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) ∧
(𝑘 ∈ N ∧ 𝑗
∈ N)) → (((𝑠 +Q
(*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠) → ⊥ )) |
43 | 42 | rexlimdvva 2434 |
. . . 4
⊢ ((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) → (∃𝑘 ∈
N ∃𝑗 ∈
N ((𝑠
+Q (*Q‘[〈𝑘, 1𝑜〉]
~Q )) <Q (𝐹‘𝑘) ∧ ((𝐹‘𝑗) +Q
(*Q‘[〈𝑗, 1𝑜〉]
~Q )) <Q 𝑠) → ⊥ )) |
44 | 31, 43 | mpd 13 |
. . 3
⊢ ((φ ∧ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) → ⊥ ) |
45 | 44 | inegd 1262 |
. 2
⊢ (φ → ¬ (𝑠 ∈
(1st ‘𝐿)
∧ 𝑠 ∈
(2nd ‘𝐿))) |
46 | 45 | ralrimivw 2387 |
1
⊢ (φ → ∀𝑠 ∈
Q ¬ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) |