Step | Hyp | Ref
| Expression |
1 | | simprl 483 |
. . 3
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿) ∧ (𝑋 ∈ 𝜔 ∧
𝑃 ∈ Q)) → 𝑋 ∈
𝜔) |
2 | | simpll 481 |
. . 3
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿) ∧ (𝑋 ∈ 𝜔 ∧
𝑃 ∈ Q)) → 〈𝐿, 𝑈〉 ∈
P) |
3 | | simplr 482 |
. . 3
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿) ∧ (𝑋 ∈ 𝜔 ∧
𝑃 ∈ Q)) → A ∈ 𝐿) |
4 | | simprr 484 |
. . 3
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿) ∧ (𝑋 ∈ 𝜔 ∧
𝑃 ∈ Q)) → 𝑃 ∈
Q) |
5 | | oveq2 5463 |
. . . . . . . . . . . . . 14
⊢ (x = 𝑋 → ((y +𝑜 2𝑜)
+𝑜 x) = ((y +𝑜 2𝑜)
+𝑜 𝑋)) |
6 | 5 | opeq1d 3546 |
. . . . . . . . . . . . 13
⊢ (x = 𝑋 → 〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉 = 〈((y
+𝑜 2𝑜) +𝑜 𝑋),
1𝑜〉) |
7 | 6 | eceq1d 6078 |
. . . . . . . . . . . 12
⊢ (x = 𝑋 → [〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉] ~Q = [〈((y +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q ) |
8 | 7 | oveq1d 5470 |
. . . . . . . . . . 11
⊢ (x = 𝑋 → ([〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉] ~Q
·Q 𝑃) = ([〈((y +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) |
9 | 8 | oveq2d 5471 |
. . . . . . . . . 10
⊢ (x = 𝑋 → (A +Q ([〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉] ~Q
·Q 𝑃)) = (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃))) |
10 | 9 | eleq1d 2103 |
. . . . . . . . 9
⊢ (x = 𝑋 → ((A +Q ([〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈 ↔ (A +Q ([〈((y +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈)) |
11 | 10 | anbi2d 437 |
. . . . . . . 8
⊢ (x = 𝑋 → (((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
12 | 11 | rexbidv 2321 |
. . . . . . 7
⊢ (x = 𝑋 → (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
13 | 12 | imbi1d 220 |
. . . . . 6
⊢ (x = 𝑋 → ((∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) ↔ (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
14 | 13 | imbi2d 219 |
. . . . 5
⊢ (x = 𝑋 → (((〈𝐿, 𝑈〉 ∈
P ∧ A ∈ 𝐿 ∧ 𝑃 ∈
Q) → (∃y ∈ 𝜔
((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) ↔ ((〈𝐿, 𝑈〉 ∈
P ∧ A ∈ 𝐿 ∧ 𝑃 ∈
Q) → (∃y ∈ 𝜔
((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))))) |
15 | | oveq2 5463 |
. . . . . . . . . . . . . 14
⊢ (x = ∅ → ((y +𝑜 2𝑜)
+𝑜 x) = ((y +𝑜 2𝑜)
+𝑜 ∅)) |
16 | 15 | opeq1d 3546 |
. . . . . . . . . . . . 13
⊢ (x = ∅ → 〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉 = 〈((y
+𝑜 2𝑜) +𝑜 ∅),
1𝑜〉) |
17 | 16 | eceq1d 6078 |
. . . . . . . . . . . 12
⊢ (x = ∅ → [〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉] ~Q = [〈((y +𝑜 2𝑜)
+𝑜 ∅), 1𝑜〉]
~Q ) |
18 | 17 | oveq1d 5470 |
. . . . . . . . . . 11
⊢ (x = ∅ → ([〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉] ~Q
·Q 𝑃) = ([〈((y +𝑜 2𝑜)
+𝑜 ∅), 1𝑜〉]
~Q ·Q 𝑃)) |
19 | 18 | oveq2d 5471 |
. . . . . . . . . 10
⊢ (x = ∅ → (A +Q ([〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉] ~Q
·Q 𝑃)) = (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃))) |
20 | 19 | eleq1d 2103 |
. . . . . . . . 9
⊢ (x = ∅ → ((A +Q ([〈((y +𝑜 2𝑜)
+𝑜 x),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈 ↔ (A +Q ([〈((y +𝑜 2𝑜)
+𝑜 ∅), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
21 | 20 | anbi2d 437 |
. . . . . . . 8
⊢ (x = ∅ → (((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈))) |
22 | 21 | rexbidv 2321 |
. . . . . . 7
⊢ (x = ∅ → (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈))) |
23 | 22 | imbi1d 220 |
. . . . . 6
⊢ (x = ∅ → ((∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) ↔ (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
24 | | oveq2 5463 |
. . . . . . . . . . . . . 14
⊢ (x = z →
((y +𝑜
2𝑜) +𝑜 x) = ((y
+𝑜 2𝑜) +𝑜 z)) |
25 | 24 | opeq1d 3546 |
. . . . . . . . . . . . 13
⊢ (x = z →
〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉 = 〈((y +𝑜 2𝑜)
+𝑜 z),
1𝑜〉) |
26 | 25 | eceq1d 6078 |
. . . . . . . . . . . 12
⊢ (x = z →
[〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q = [〈((y
+𝑜 2𝑜) +𝑜 z), 1𝑜〉]
~Q ) |
27 | 26 | oveq1d 5470 |
. . . . . . . . . . 11
⊢ (x = z →
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃) = ([〈((y +𝑜 2𝑜)
+𝑜 z),
1𝑜〉] ~Q
·Q 𝑃)) |
28 | 27 | oveq2d 5471 |
. . . . . . . . . 10
⊢ (x = z →
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) = (A +Q ([〈((y +𝑜 2𝑜)
+𝑜 z),
1𝑜〉] ~Q
·Q 𝑃))) |
29 | 28 | eleq1d 2103 |
. . . . . . . . 9
⊢ (x = z →
((A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈 ↔ (A +Q ([〈((y +𝑜 2𝑜)
+𝑜 z),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈)) |
30 | 29 | anbi2d 437 |
. . . . . . . 8
⊢ (x = z →
(((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
31 | 30 | rexbidv 2321 |
. . . . . . 7
⊢ (x = z →
(∃y
∈ 𝜔 ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
32 | 31 | imbi1d 220 |
. . . . . 6
⊢ (x = z →
((∃y
∈ 𝜔 ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) ↔ (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
33 | | oveq2 5463 |
. . . . . . . . . . . . . 14
⊢ (x = suc z →
((y +𝑜
2𝑜) +𝑜 x) = ((y
+𝑜 2𝑜) +𝑜 suc z)) |
34 | 33 | opeq1d 3546 |
. . . . . . . . . . . . 13
⊢ (x = suc z →
〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉 = 〈((y +𝑜 2𝑜)
+𝑜 suc z),
1𝑜〉) |
35 | 34 | eceq1d 6078 |
. . . . . . . . . . . 12
⊢ (x = suc z →
[〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q = [〈((y
+𝑜 2𝑜) +𝑜 suc z), 1𝑜〉]
~Q ) |
36 | 35 | oveq1d 5470 |
. . . . . . . . . . 11
⊢ (x = suc z →
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃) = ([〈((y +𝑜 2𝑜)
+𝑜 suc z),
1𝑜〉] ~Q
·Q 𝑃)) |
37 | 36 | oveq2d 5471 |
. . . . . . . . . 10
⊢ (x = suc z →
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) = (A +Q ([〈((y +𝑜 2𝑜)
+𝑜 suc z),
1𝑜〉] ~Q
·Q 𝑃))) |
38 | 37 | eleq1d 2103 |
. . . . . . . . 9
⊢ (x = suc z →
((A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈 ↔ (A +Q ([〈((y +𝑜 2𝑜)
+𝑜 suc z),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈)) |
39 | 38 | anbi2d 437 |
. . . . . . . 8
⊢ (x = suc z →
(((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 suc z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
40 | 39 | rexbidv 2321 |
. . . . . . 7
⊢ (x = suc z →
(∃y
∈ 𝜔 ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 suc z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
41 | 40 | imbi1d 220 |
. . . . . 6
⊢ (x = suc z →
((∃y
∈ 𝜔 ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) ↔ (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 suc z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
42 | | 2onn 6030 |
. . . . . . . . . . . . . . . . 17
⊢
2𝑜 ∈
𝜔 |
43 | | nnacl 5998 |
. . . . . . . . . . . . . . . . . 18
⊢
((y ∈ 𝜔 ∧
2𝑜 ∈ 𝜔) →
(y +𝑜
2𝑜) ∈
𝜔) |
44 | | nna0 5992 |
. . . . . . . . . . . . . . . . . 18
⊢
((y +𝑜
2𝑜) ∈ 𝜔 →
((y +𝑜
2𝑜) +𝑜 ∅) = (y +𝑜
2𝑜)) |
45 | 43, 44 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢
((y ∈ 𝜔 ∧
2𝑜 ∈ 𝜔) →
((y +𝑜
2𝑜) +𝑜 ∅) = (y +𝑜
2𝑜)) |
46 | 42, 45 | mpan2 401 |
. . . . . . . . . . . . . . . 16
⊢ (y ∈ 𝜔
→ ((y +𝑜
2𝑜) +𝑜 ∅) = (y +𝑜
2𝑜)) |
47 | 46 | opeq1d 3546 |
. . . . . . . . . . . . . . 15
⊢ (y ∈ 𝜔
→ 〈((y +𝑜
2𝑜) +𝑜 ∅),
1𝑜〉 = 〈(y
+𝑜 2𝑜),
1𝑜〉) |
48 | 47 | eceq1d 6078 |
. . . . . . . . . . . . . 14
⊢ (y ∈ 𝜔
→ [〈((y +𝑜
2𝑜) +𝑜 ∅),
1𝑜〉] ~Q = [〈(y +𝑜 2𝑜),
1𝑜〉] ~Q ) |
49 | 48 | oveq1d 5470 |
. . . . . . . . . . . . 13
⊢ (y ∈ 𝜔
→ ([〈((y +𝑜
2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃) = ([〈(y +𝑜 2𝑜),
1𝑜〉] ~Q
·Q 𝑃)) |
50 | 49 | oveq2d 5471 |
. . . . . . . . . . . 12
⊢ (y ∈ 𝜔
→ (A +Q
([〈((y +𝑜
2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) = (A
+Q ([〈(y
+𝑜 2𝑜), 1𝑜〉]
~Q ·Q 𝑃))) |
51 | 50 | eleq1d 2103 |
. . . . . . . . . . 11
⊢ (y ∈ 𝜔
→ ((A +Q
([〈((y +𝑜
2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈 ↔ (A +Q ([〈(y +𝑜 2𝑜),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈)) |
52 | 51 | anbi2d 437 |
. . . . . . . . . 10
⊢ (y ∈ 𝜔
→ (((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) ↔ ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈(y +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
53 | 52 | rexbiia 2333 |
. . . . . . . . 9
⊢ (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) ↔ ∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(y
+𝑜 2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
54 | | opeq1 3540 |
. . . . . . . . . . . . . . 15
⊢ (y = 𝑗 → 〈y, 1𝑜〉 = 〈𝑗,
1𝑜〉) |
55 | 54 | eceq1d 6078 |
. . . . . . . . . . . . . 14
⊢ (y = 𝑗 → [〈y, 1𝑜〉]
~Q0 = [〈𝑗, 1𝑜〉]
~Q0 ) |
56 | 55 | oveq1d 5470 |
. . . . . . . . . . . . 13
⊢ (y = 𝑗 → ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃) = ([〈𝑗, 1𝑜〉]
~Q0 ·Q0 𝑃)) |
57 | 56 | oveq2d 5471 |
. . . . . . . . . . . 12
⊢ (y = 𝑗 → (A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) = (A +Q0 ([〈𝑗, 1𝑜〉]
~Q0 ·Q0 𝑃))) |
58 | 57 | eleq1d 2103 |
. . . . . . . . . . 11
⊢ (y = 𝑗 → ((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ↔ (A +Q0 ([〈𝑗, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿)) |
59 | | oveq1 5462 |
. . . . . . . . . . . . . . . 16
⊢ (y = 𝑗 → (y +𝑜 2𝑜) =
(𝑗 +𝑜
2𝑜)) |
60 | 59 | opeq1d 3546 |
. . . . . . . . . . . . . . 15
⊢ (y = 𝑗 → 〈(y +𝑜 2𝑜),
1𝑜〉 = 〈(𝑗 +𝑜
2𝑜), 1𝑜〉) |
61 | 60 | eceq1d 6078 |
. . . . . . . . . . . . . 14
⊢ (y = 𝑗 → [〈(y +𝑜 2𝑜),
1𝑜〉] ~Q = [〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ) |
62 | 61 | oveq1d 5470 |
. . . . . . . . . . . . 13
⊢ (y = 𝑗 → ([〈(y +𝑜 2𝑜),
1𝑜〉] ~Q
·Q 𝑃) = ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) |
63 | 62 | oveq2d 5471 |
. . . . . . . . . . . 12
⊢ (y = 𝑗 → (A +Q ([〈(y +𝑜 2𝑜),
1𝑜〉] ~Q
·Q 𝑃)) = (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃))) |
64 | 63 | eleq1d 2103 |
. . . . . . . . . . 11
⊢ (y = 𝑗 → ((A +Q ([〈(y +𝑜 2𝑜),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈 ↔ (A +Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
65 | 58, 64 | anbi12d 442 |
. . . . . . . . . 10
⊢ (y = 𝑗 → (((A +Q0 ([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈(y +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((A +Q0 ([〈𝑗, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈(𝑗
+𝑜 2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
66 | 65 | cbvrexv 2528 |
. . . . . . . . 9
⊢ (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(y
+𝑜 2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
67 | 53, 66 | bitri 173 |
. . . . . . . 8
⊢ (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) ↔ ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
68 | 67 | biimpi 113 |
. . . . . . 7
⊢ (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
69 | 68 | a1i 9 |
. . . . . 6
⊢
((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿 ∧ 𝑃 ∈ Q) → (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 ∅),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
70 | | prarloclem3step 6479 |
. . . . . . . . 9
⊢
(((z ∈ 𝜔 ∧
(〈𝐿, 𝑈〉 ∈
P ∧ A ∈ 𝐿 ∧ 𝑃 ∈
Q)) ∧ ∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 suc z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → ∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
71 | 70 | ex 108 |
. . . . . . . 8
⊢
((z ∈ 𝜔 ∧
(〈𝐿, 𝑈〉 ∈
P ∧ A ∈ 𝐿 ∧ 𝑃 ∈
Q)) → (∃y ∈ 𝜔
((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 suc z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
72 | 71 | imim1d 69 |
. . . . . . 7
⊢
((z ∈ 𝜔 ∧
(〈𝐿, 𝑈〉 ∈
P ∧ A ∈ 𝐿 ∧ 𝑃 ∈
Q)) → ((∃y ∈ 𝜔
((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 suc z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
73 | 72 | ex 108 |
. . . . . 6
⊢ (z ∈ 𝜔
→ ((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿 ∧ 𝑃 ∈ Q) → ((∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 suc z), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))))) |
74 | 23, 32, 41, 69, 73 | finds2 4267 |
. . . . 5
⊢ (x ∈ 𝜔
→ ((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿 ∧ 𝑃 ∈ Q) → (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 x), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
75 | 14, 74 | vtoclga 2613 |
. . . 4
⊢ (𝑋 ∈ 𝜔 → ((〈𝐿, 𝑈〉 ∈
P ∧ A ∈ 𝐿 ∧ 𝑃 ∈
Q) → (∃y ∈ 𝜔
((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |
76 | 75 | imp 115 |
. . 3
⊢ ((𝑋 ∈ 𝜔 ∧
(〈𝐿, 𝑈〉 ∈
P ∧ A ∈ 𝐿 ∧ 𝑃 ∈
Q)) → (∃y ∈ 𝜔
((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
77 | 1, 2, 3, 4, 76 | syl13anc 1136 |
. 2
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿) ∧ (𝑋 ∈ 𝜔 ∧
𝑃 ∈ Q)) → (∃y ∈ 𝜔 ((A
+Q0 ([〈y,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈((y
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
78 | 77 | 3impia 1100 |
1
⊢
(((〈𝐿, 𝑈〉 ∈ P ∧ A ∈ 𝐿) ∧ (𝑋 ∈ 𝜔 ∧
𝑃 ∈ Q) ∧ ∃y ∈ 𝜔
((A +Q0
([〈y, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧
(A +Q
([〈((y +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑗 ∈
𝜔 ((A +Q0
([〈𝑗,
1𝑜〉] ~Q0
·Q0 𝑃)) ∈ 𝐿 ∧ (A
+Q ([〈(𝑗 +𝑜
2𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |