Step | Hyp | Ref
| Expression |
1 | | df-enq0 7386 |
. . 3
⊢
~Q0 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))} |
2 | | df-xp 4617 |
. . 3
⊢
((N × N) × (N
× N)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))} |
3 | 1, 2 | ineq12i 3326 |
. 2
⊢ (
~Q0 ∩ ((N × N)
× (N × N))) = ({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))} ∩ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))}) |
4 | | inopab 4743 |
. 2
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))} ∩ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))}) = {〈𝑥, 𝑦〉 ∣ (((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)))} |
5 | | an32 557 |
. . . . . 6
⊢ ((((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ↔ (((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
6 | | an4 581 |
. . . . . . . 8
⊢ (((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ↔ ((𝑥 ∈ (ω × N)
∧ 𝑥 ∈
(N × N)) ∧ (𝑦 ∈ (ω × N)
∧ 𝑦 ∈
(N × N)))) |
7 | | pinn 7271 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ N →
𝑥 ∈
ω) |
8 | 7 | ssriv 3151 |
. . . . . . . . . . . 12
⊢
N ⊆ ω |
9 | | xpss1 4721 |
. . . . . . . . . . . 12
⊢
(N ⊆ ω → (N ×
N) ⊆ (ω × N)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(N × N) ⊆ (ω ×
N) |
11 | 10 | sseli 3143 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (N ×
N) → 𝑥
∈ (ω × N)) |
12 | 11 | pm4.71ri 390 |
. . . . . . . . 9
⊢ (𝑥 ∈ (N ×
N) ↔ (𝑥
∈ (ω × N) ∧ 𝑥 ∈ (N ×
N))) |
13 | 10 | sseli 3143 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (N ×
N) → 𝑦
∈ (ω × N)) |
14 | 13 | pm4.71ri 390 |
. . . . . . . . 9
⊢ (𝑦 ∈ (N ×
N) ↔ (𝑦
∈ (ω × N) ∧ 𝑦 ∈ (N ×
N))) |
15 | 12, 14 | anbi12i 457 |
. . . . . . . 8
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ↔ ((𝑥 ∈ (ω × N)
∧ 𝑥 ∈
(N × N)) ∧ (𝑦 ∈ (ω × N)
∧ 𝑦 ∈
(N × N)))) |
16 | 6, 15 | bitr4i 186 |
. . . . . . 7
⊢ (((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ↔ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) |
17 | 16 | anbi1i 455 |
. . . . . 6
⊢ ((((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
18 | 5, 17 | bitri 183 |
. . . . 5
⊢ ((((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
19 | | eleq1 2233 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 〈𝑧, 𝑤〉 → (𝑥 ∈ (N ×
N) ↔ 〈𝑧, 𝑤〉 ∈ (N ×
N))) |
20 | | opelxp 4641 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑧, 𝑤〉 ∈ (N
× N) ↔ (𝑧 ∈ N ∧ 𝑤 ∈
N)) |
21 | 19, 20 | bitrdi 195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 〈𝑧, 𝑤〉 → (𝑥 ∈ (N ×
N) ↔ (𝑧
∈ N ∧ 𝑤 ∈ N))) |
22 | | eleq1 2233 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 〈𝑣, 𝑢〉 → (𝑦 ∈ (N ×
N) ↔ 〈𝑣, 𝑢〉 ∈ (N ×
N))) |
23 | | opelxp 4641 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑣, 𝑢〉 ∈ (N
× N) ↔ (𝑣 ∈ N ∧ 𝑢 ∈
N)) |
24 | 22, 23 | bitrdi 195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 〈𝑣, 𝑢〉 → (𝑦 ∈ (N ×
N) ↔ (𝑣
∈ N ∧ 𝑢 ∈ N))) |
25 | 21, 24 | bi2anan9 601 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) → ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ↔ ((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)))) |
26 | 25 | pm5.32i 451 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ↔ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ ((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)))) |
27 | 26 | anbi1i 455 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ ((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N))) ∧ (𝑧
·o 𝑢) =
(𝑤 ·o
𝑣))) |
28 | | anass 399 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ ((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N))) ∧ (𝑧
·o 𝑢) =
(𝑤 ·o
𝑣)) ↔ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)) ∧ (𝑧
·o 𝑢) =
(𝑤 ·o
𝑣)))) |
29 | 27, 28 | bitri 183 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)) ∧ (𝑧
·o 𝑢) =
(𝑤 ·o
𝑣)))) |
30 | | mulpiord 7279 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ N ∧
𝑢 ∈ N)
→ (𝑧
·N 𝑢) = (𝑧 ·o 𝑢)) |
31 | | mulpiord 7279 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ N ∧
𝑣 ∈ N)
→ (𝑤
·N 𝑣) = (𝑤 ·o 𝑣)) |
32 | 30, 31 | eqeqan12d 2186 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ N ∧
𝑢 ∈ N)
∧ (𝑤 ∈
N ∧ 𝑣
∈ N)) → ((𝑧 ·N 𝑢) = (𝑤 ·N 𝑣) ↔ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
33 | 32 | an42s 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) → ((𝑧 ·N 𝑢) = (𝑤 ·N 𝑣) ↔ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
34 | 33 | pm5.32i 451 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑣 ∈
N ∧ 𝑢
∈ N)) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) ↔ (((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)) ∧ (𝑧
·o 𝑢) =
(𝑤 ·o
𝑣))) |
35 | 34 | anbi2i 454 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)) ∧ (𝑧
·N 𝑢) = (𝑤 ·N 𝑣))) ↔ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)) ∧ (𝑧
·o 𝑢) =
(𝑤 ·o
𝑣)))) |
36 | 29, 35 | bitr4i 186 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)) ∧ (𝑧
·N 𝑢) = (𝑤 ·N 𝑣)))) |
37 | | anass 399 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ ((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N))) ∧ (𝑧
·N 𝑢) = (𝑤 ·N 𝑣)) ↔ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N)) ∧ (𝑧
·N 𝑢) = (𝑤 ·N 𝑣)))) |
38 | 36, 37 | bitr4i 186 |
. . . . . . . . . . . 12
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ ((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N))) ∧ (𝑧
·N 𝑢) = (𝑤 ·N 𝑣))) |
39 | 26 | anbi1i 455 |
. . . . . . . . . . . 12
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) ↔ (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ ((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ N
∧ 𝑢 ∈
N))) ∧ (𝑧
·N 𝑢) = (𝑤 ·N 𝑣))) |
40 | 38, 39 | bitr4i 186 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))) |
41 | | ancom 264 |
. . . . . . . . . . . 12
⊢ (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉))) |
42 | 41 | anbi1i 455 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
43 | 41 | anbi1i 455 |
. . . . . . . . . . 11
⊢ ((((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) ↔ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))) |
44 | 40, 42, 43 | 3bitr3i 209 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))) |
45 | | anass 399 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
46 | | anass 399 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
47 | 44, 45, 46 | 3bitr3i 209 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
48 | 47 | 2exbii 1599 |
. . . . . . . 8
⊢
(∃𝑣∃𝑢((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ∃𝑣∃𝑢((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
49 | | 19.42vv 1904 |
. . . . . . . 8
⊢
(∃𝑣∃𝑢((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
50 | | 19.42vv 1904 |
. . . . . . . 8
⊢
(∃𝑣∃𝑢((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
51 | 48, 49, 50 | 3bitr3i 209 |
. . . . . . 7
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
52 | 51 | 2exbii 1599 |
. . . . . 6
⊢
(∃𝑧∃𝑤((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ∃𝑧∃𝑤((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
53 | | 19.42vv 1904 |
. . . . . 6
⊢
(∃𝑧∃𝑤((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
54 | | 19.42vv 1904 |
. . . . . 6
⊢
(∃𝑧∃𝑤((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
55 | 52, 53, 54 | 3bitr3i 209 |
. . . . 5
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
56 | 18, 55 | bitri 183 |
. . . 4
⊢ ((((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N))) ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))) |
57 | 56 | opabbii 4056 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ (((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} |
58 | | df-enq 7309 |
. . 3
⊢
~Q = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} |
59 | 57, 58 | eqtr4i 2194 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ (((𝑥 ∈ (ω ×
N) ∧ 𝑦
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ∧ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)))} =
~Q |
60 | 3, 4, 59 | 3eqtrri 2196 |
1
⊢
~Q = ( ~Q0 ∩
((N × N) × (N ×
N))) |