Step | Hyp | Ref
| Expression |
1 | | nnaass 6087 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ω ∧ 𝑔 ∈ ω ∧ ℎ ∈ ω) → ((𝑓 +𝑜 𝑔) +𝑜 ℎ) = (𝑓 +𝑜 (𝑔 +𝑜 ℎ))) |
2 | 1 | adantl 271 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω ∧ ℎ ∈ ω)) → ((𝑓 +𝑜 𝑔) +𝑜 ℎ) = (𝑓 +𝑜 (𝑔 +𝑜 ℎ))) |
3 | | simpr 108 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → 𝑦 ∈
ω) |
4 | | 1onn 6116 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ ω |
5 | | nnacl 6082 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ω ∧
1𝑜 ∈ ω) → (𝑦 +𝑜 1𝑜)
∈ ω) |
6 | 3, 4, 5 | sylancl 404 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝑦 +𝑜
1𝑜) ∈ ω) |
7 | | 2onn 6117 |
. . . . . . . . . . . . . 14
⊢
2𝑜 ∈ ω |
8 | 7 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
2𝑜 ∈ ω) |
9 | | simpll 495 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → 𝑋 ∈
ω) |
10 | 2, 6, 8, 9 | caovassd 5680 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (((𝑦 +𝑜
1𝑜) +𝑜 2𝑜)
+𝑜 𝑋) =
((𝑦 +𝑜
1𝑜) +𝑜 (2𝑜
+𝑜 𝑋))) |
11 | 4 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
1𝑜 ∈ ω) |
12 | | nnacom 6086 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ω ∧ 𝑔 ∈ ω) → (𝑓 +𝑜 𝑔) = (𝑔 +𝑜 𝑓)) |
13 | 12 | adantl 271 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑓 +𝑜 𝑔) = (𝑔 +𝑜 𝑓)) |
14 | | nnacl 6082 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ω ∧ 𝑔 ∈ ω) → (𝑓 +𝑜 𝑔) ∈
ω) |
15 | 14 | adantl 271 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑓 +𝑜 𝑔) ∈
ω) |
16 | 3, 8, 11, 13, 2, 9, 15 | caov4d 5705 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝑦 +𝑜
2𝑜) +𝑜 (1𝑜
+𝑜 𝑋)) =
((𝑦 +𝑜
1𝑜) +𝑜 (2𝑜
+𝑜 𝑋))) |
17 | 13, 11, 9 | caovcomd 5677 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
(1𝑜 +𝑜 𝑋) = (𝑋 +𝑜
1𝑜)) |
18 | | nnon 4350 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ω → 𝑋 ∈ On) |
19 | | oa1suc 6070 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ On → (𝑋 +𝑜
1𝑜) = suc 𝑋) |
20 | 9, 18, 19 | 3syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝑋 +𝑜
1𝑜) = suc 𝑋) |
21 | 17, 20 | eqtrd 2113 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
(1𝑜 +𝑜 𝑋) = suc 𝑋) |
22 | 21 | oveq2d 5548 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝑦 +𝑜
2𝑜) +𝑜 (1𝑜
+𝑜 𝑋)) =
((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋)) |
23 | 10, 16, 22 | 3eqtr2rd 2120 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋) = (((𝑦 +𝑜 1𝑜)
+𝑜 2𝑜) +𝑜 𝑋)) |
24 | 23 | opeq1d 3576 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
〈((𝑦
+𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜〉 =
〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋),
1𝑜〉) |
25 | 24 | eceq1d 6165 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
[〈((𝑦
+𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q = [〈(((𝑦 +𝑜 1𝑜)
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ) |
26 | 25 | oveq1d 5547 |
. . . . . . . 8
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈((𝑦
+𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃) = ([〈(((𝑦 +𝑜
1𝑜) +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) |
27 | 26 | oveq2d 5548 |
. . . . . . 7
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +Q
([〈((𝑦
+𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) = (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃))) |
28 | 27 | eleq1d 2147 |
. . . . . 6
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q
([〈((𝑦
+𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈 ↔ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
29 | 28 | biimpd 142 |
. . . . 5
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q
([〈((𝑦
+𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈 → (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
30 | | simplr1 980 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
〈𝐿, 𝑈〉 ∈
P) |
31 | | simplr2 981 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → 𝐴 ∈ 𝐿) |
32 | | elprnql 6671 |
. . . . . . . . . . . 12
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐴 ∈ 𝐿) → 𝐴 ∈ Q) |
33 | 30, 31, 32 | syl2anc 403 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → 𝐴 ∈
Q) |
34 | | 1pi 6505 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ N |
35 | | nnppipi 6533 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ω ∧
1𝑜 ∈ N) → (𝑦 +𝑜 1𝑜)
∈ N) |
36 | 3, 34, 35 | sylancl 404 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝑦 +𝑜
1𝑜) ∈ N) |
37 | | opelxpi 4394 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 +𝑜
1𝑜) ∈ N ∧ 1𝑜
∈ N) → 〈(𝑦 +𝑜
1𝑜), 1𝑜〉 ∈ (N
× N)) |
38 | 34, 37 | mpan2 415 |
. . . . . . . . . . . . 13
⊢ ((𝑦 +𝑜
1𝑜) ∈ N → 〈(𝑦 +𝑜
1𝑜), 1𝑜〉 ∈ (N
× N)) |
39 | | enqex 6550 |
. . . . . . . . . . . . . . 15
⊢
~Q ∈ V |
40 | 39 | ecelqsi 6183 |
. . . . . . . . . . . . . 14
⊢
(〈(𝑦
+𝑜 1𝑜), 1𝑜〉
∈ (N × N) → [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ∈ ((N × N)
/ ~Q )) |
41 | | df-nqqs 6538 |
. . . . . . . . . . . . . 14
⊢
Q = ((N × N) /
~Q ) |
42 | 40, 41 | syl6eleqr 2172 |
. . . . . . . . . . . . 13
⊢
(〈(𝑦
+𝑜 1𝑜), 1𝑜〉
∈ (N × N) → [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ∈ Q) |
43 | 36, 38, 42 | 3syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ Q) |
44 | | simplr3 982 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → 𝑃 ∈
Q) |
45 | | mulclnq 6566 |
. . . . . . . . . . . 12
⊢
(([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ Q ∧ 𝑃 ∈ Q) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) ∈
Q) |
46 | 43, 44, 45 | syl2anc 403 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) ∈
Q) |
47 | | nqnq0a 6644 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Q ∧
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) ∈ Q) →
(𝐴
+Q ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) = (𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃))) |
48 | 33, 46, 47 | syl2anc 403 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) = (𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q 𝑃))) |
49 | | nqnq0m 6645 |
. . . . . . . . . . . . 13
⊢
(([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ∈ Q ∧ 𝑃 ∈ Q) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) = ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q0 𝑃)) |
50 | 43, 44, 49 | syl2anc 403 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) = ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q0 𝑃)) |
51 | | nqnq0pi 6628 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 +𝑜
1𝑜) ∈ N ∧ 1𝑜
∈ N) → [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 = [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ) |
52 | 36, 34, 51 | sylancl 404 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
[〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q0 = [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ) |
53 | 52 | oveq1d 5547 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃) = ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q ·Q0 𝑃)) |
54 | 50, 53 | eqtr4d 2116 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) →
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃) = ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) |
55 | 54 | oveq2d 5548 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +Q0
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) = (𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃))) |
56 | 48, 55 | eqtrd 2113 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) = (𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃))) |
57 | 56 | eleq1d 2147 |
. . . . . . . 8
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ↔ (𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿)) |
58 | 57 | anbi1d 452 |
. . . . . . 7
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
59 | | opeq1 3570 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ 〈𝑧,
1𝑜〉 = 〈(𝑦 +𝑜
1𝑜), 1𝑜〉) |
60 | 59 | eceq1d 6165 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ [〈𝑧,
1𝑜〉] ~Q0 = [〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ) |
61 | 60 | oveq1d 5547 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ ([〈𝑧,
1𝑜〉] ~Q0
·Q0 𝑃) = ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) |
62 | 61 | oveq2d 5548 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ (𝐴
+Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) = (𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃))) |
63 | 62 | eleq1d 2147 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ ((𝐴
+Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ↔ (𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿)) |
64 | | oveq1 5539 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ (𝑧
+𝑜 2𝑜) = ((𝑦 +𝑜 1𝑜)
+𝑜 2𝑜)) |
65 | 64 | oveq1d 5547 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ ((𝑧
+𝑜 2𝑜) +𝑜 𝑋) = (((𝑦 +𝑜 1𝑜)
+𝑜 2𝑜) +𝑜 𝑋)) |
66 | 65 | opeq1d 3576 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ 〈((𝑧
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉 =
〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋),
1𝑜〉) |
67 | 66 | eceq1d 6165 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ [〈((𝑧
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q = [〈(((𝑦 +𝑜 1𝑜)
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ) |
68 | 67 | oveq1d 5547 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ ([〈((𝑧
+𝑜 2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃) = ([〈(((𝑦 +𝑜
1𝑜) +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) |
69 | 68 | oveq2d 5548 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ (𝐴
+Q ([〈((𝑧 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) = (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃))) |
70 | 69 | eleq1d 2147 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ ((𝐴
+Q ([〈((𝑧 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) ∈ 𝑈 ↔ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
71 | 63, 70 | anbi12d 456 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑦 +𝑜 1𝑜)
→ (((𝐴
+Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
72 | 71 | rspcev 2701 |
. . . . . . . . 9
⊢ (((𝑦 +𝑜
1𝑜) ∈ ω ∧ ((𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑧 ∈ ω ((𝐴 +Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
73 | 72 | ex 113 |
. . . . . . . 8
⊢ ((𝑦 +𝑜
1𝑜) ∈ ω → (((𝐴 +Q0 ([〈(𝑦 +𝑜
1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑧 ∈ ω ((𝐴 +Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
74 | 6, 73 | syl 14 |
. . . . . . 7
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (((𝐴 +Q0
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑧 ∈ ω ((𝐴 +Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
75 | 58, 74 | sylbid 148 |
. . . . . 6
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑧 ∈ ω ((𝐴 +Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
76 | | opeq1 3570 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → 〈𝑧, 1𝑜〉 = 〈𝑦,
1𝑜〉) |
77 | 76 | eceq1d 6165 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → [〈𝑧, 1𝑜〉]
~Q0 = [〈𝑦, 1𝑜〉]
~Q0 ) |
78 | 77 | oveq1d 5547 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃) = ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) |
79 | 78 | oveq2d 5548 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝐴 +Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) = (𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃))) |
80 | 79 | eleq1d 2147 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝐴 +Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ↔ (𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿)) |
81 | | oveq1 5539 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → (𝑧 +𝑜 2𝑜)
= (𝑦 +𝑜
2𝑜)) |
82 | 81 | oveq1d 5547 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → ((𝑧 +𝑜 2𝑜)
+𝑜 𝑋) =
((𝑦 +𝑜
2𝑜) +𝑜 𝑋)) |
83 | 82 | opeq1d 3576 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → 〈((𝑧 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉 = 〈((𝑦 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉) |
84 | 83 | eceq1d 6165 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → [〈((𝑧 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q = [〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ) |
85 | 84 | oveq1d 5547 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → ([〈((𝑧 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃) = ([〈((𝑦 +𝑜 2𝑜)
+𝑜 𝑋),
1𝑜〉] ~Q
·Q 𝑃)) |
86 | 85 | oveq2d 5548 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) = (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃))) |
87 | 86 | eleq1d 2147 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈 ↔ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
88 | 80, 87 | anbi12d 456 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (((𝐴 +Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
89 | 88 | cbvrexv 2578 |
. . . . . 6
⊢
(∃𝑧 ∈
ω ((𝐴
+Q0 ([〈𝑧, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑧 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) ↔ ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)) |
90 | 75, 89 | syl6ib 159 |
. . . . 5
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q
([〈(((𝑦
+𝑜 1𝑜) +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
91 | 29, 90 | sylan2d 288 |
. . . 4
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
92 | 91 | expdimp 255 |
. . 3
⊢ ((((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿) → ((𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈 → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
93 | 92 | adantld 272 |
. 2
⊢ ((((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿) → (((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈))) |
94 | 93 | ex 113 |
1
⊢ (((𝑋 ∈ ω ∧
(〈𝐿, 𝑈〉 ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q
([〈(𝑦
+𝑜 1𝑜), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝐿 → (((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 suc 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([〈𝑦, 1𝑜〉]
~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([〈((𝑦 +𝑜
2𝑜) +𝑜 𝑋), 1𝑜〉]
~Q ·Q 𝑃)) ∈ 𝑈)))) |