Step | Hyp | Ref
| Expression |
1 | | df-nq0 6523 |
. . 3
⊢
Q0 = ((ω × N)
/ ~Q0 ) |
2 | | oveq1 5519 |
. . . 4
⊢
([〈𝑥, 𝑦〉]
~Q0 = 𝐴 → ([〈𝑥, 𝑦〉] ~Q0
+Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
(𝐴
+Q0 [〈𝑧, 𝑤〉] ~Q0
)) |
3 | 2 | eleq1d 2106 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~Q0 = 𝐴 → (([〈𝑥, 𝑦〉] ~Q0
+Q0 [〈𝑧, 𝑤〉] ~Q0 ) ∈
((ω × N) / ~Q0 )
↔ (𝐴
+Q0 [〈𝑧, 𝑤〉] ~Q0 ) ∈
((ω × N) / ~Q0
))) |
4 | | oveq2 5520 |
. . . 4
⊢
([〈𝑧, 𝑤〉]
~Q0 = 𝐵 → (𝐴 +Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
(𝐴
+Q0 𝐵)) |
5 | 4 | eleq1d 2106 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~Q0 = 𝐵 → ((𝐴 +Q0 [〈𝑧, 𝑤〉] ~Q0 ) ∈
((ω × N) / ~Q0 )
↔ (𝐴
+Q0 𝐵) ∈ ((ω × N)
/ ~Q0 ))) |
6 | | addnnnq0 6547 |
. . . 4
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ ([〈𝑥, 𝑦〉]
~Q0 +Q0 [〈𝑧, 𝑤〉] ~Q0 ) =
[〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ) |
7 | | pinn 6407 |
. . . . . . . . 9
⊢ (𝑤 ∈ N →
𝑤 ∈
ω) |
8 | | nnmcl 6060 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ω ∧ 𝑤 ∈ ω) → (𝑥 ·𝑜
𝑤) ∈
ω) |
9 | 7, 8 | sylan2 270 |
. . . . . . . 8
⊢ ((𝑥 ∈ ω ∧ 𝑤 ∈ N) →
(𝑥
·𝑜 𝑤) ∈ ω) |
10 | | pinn 6407 |
. . . . . . . . 9
⊢ (𝑦 ∈ N →
𝑦 ∈
ω) |
11 | | nnmcl 6060 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (𝑦 ·𝑜
𝑧) ∈
ω) |
12 | 10, 11 | sylan 267 |
. . . . . . . 8
⊢ ((𝑦 ∈ N ∧
𝑧 ∈ ω) →
(𝑦
·𝑜 𝑧) ∈ ω) |
13 | | nnacl 6059 |
. . . . . . . 8
⊢ (((𝑥 ·𝑜
𝑤) ∈ ω ∧
(𝑦
·𝑜 𝑧) ∈ ω) → ((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)) ∈
ω) |
14 | 9, 12, 13 | syl2an 273 |
. . . . . . 7
⊢ (((𝑥 ∈ ω ∧ 𝑤 ∈ N) ∧
(𝑦 ∈ N
∧ 𝑧 ∈ ω))
→ ((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)) ∈
ω) |
15 | 14 | an42s 523 |
. . . . . 6
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ ((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)) ∈
ω) |
16 | | mulpiord 6415 |
. . . . . . . 8
⊢ ((𝑦 ∈ N ∧
𝑤 ∈ N)
→ (𝑦
·N 𝑤) = (𝑦 ·𝑜 𝑤)) |
17 | | mulclpi 6426 |
. . . . . . . 8
⊢ ((𝑦 ∈ N ∧
𝑤 ∈ N)
→ (𝑦
·N 𝑤) ∈ N) |
18 | 16, 17 | eqeltrrd 2115 |
. . . . . . 7
⊢ ((𝑦 ∈ N ∧
𝑤 ∈ N)
→ (𝑦
·𝑜 𝑤) ∈ N) |
19 | 18 | ad2ant2l 477 |
. . . . . 6
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ (𝑦
·𝑜 𝑤) ∈ N) |
20 | 15, 19 | jca 290 |
. . . . 5
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ (((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)) ∈ ω ∧ (𝑦 ·𝑜
𝑤) ∈
N)) |
21 | | opelxpi 4376 |
. . . . 5
⊢ ((((𝑥 ·𝑜
𝑤) +𝑜
(𝑦
·𝑜 𝑧)) ∈ ω ∧ (𝑦 ·𝑜 𝑤) ∈ N) →
〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉 ∈ (ω ×
N)) |
22 | | enq0ex 6537 |
. . . . . 6
⊢
~Q0 ∈ V |
23 | 22 | ecelqsi 6160 |
. . . . 5
⊢
(〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉 ∈ (ω ×
N) → [〈((𝑥 ·𝑜 𝑤) +𝑜 (𝑦 ·𝑜
𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ∈ ((ω × N) /
~Q0 )) |
24 | 20, 21, 23 | 3syl 17 |
. . . 4
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ [〈((𝑥
·𝑜 𝑤) +𝑜 (𝑦 ·𝑜 𝑧)), (𝑦 ·𝑜 𝑤)〉]
~Q0 ∈ ((ω × N) /
~Q0 )) |
25 | 6, 24 | eqeltrd 2114 |
. . 3
⊢ (((𝑥 ∈ ω ∧ 𝑦 ∈ N) ∧
(𝑧 ∈ ω ∧
𝑤 ∈ N))
→ ([〈𝑥, 𝑦〉]
~Q0 +Q0 [〈𝑧, 𝑤〉] ~Q0 ) ∈
((ω × N) / ~Q0
)) |
26 | 1, 3, 5, 25 | 2ecoptocl 6194 |
. 2
⊢ ((𝐴 ∈
Q0 ∧ 𝐵 ∈ Q0) →
(𝐴
+Q0 𝐵) ∈ ((ω × N)
/ ~Q0 )) |
27 | 26, 1 | syl6eleqr 2131 |
1
⊢ ((𝐴 ∈
Q0 ∧ 𝐵 ∈ Q0) →
(𝐴
+Q0 𝐵) ∈
Q0) |