Step | Hyp | Ref
| Expression |
1 | | elxpi 4625 |
. . . . . 6
⊢ (𝑓 ∈ (ω ×
N) → ∃𝑧∃𝑤(𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N))) |
2 | | elxpi 4625 |
. . . . . 6
⊢ (𝑓 ∈ (ω ×
N) → ∃𝑣∃𝑢(𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N))) |
3 | | ee4anv 1927 |
. . . . . 6
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ (𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N))) ↔
(∃𝑧∃𝑤(𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ ∃𝑣∃𝑢(𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N)))) |
4 | 1, 2, 3 | sylanbrc 415 |
. . . . 5
⊢ (𝑓 ∈ (ω ×
N) → ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ (𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N)))) |
5 | | eqtr2 2189 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) → 〈𝑧, 𝑤〉 = 〈𝑣, 𝑢〉) |
6 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
7 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑤 ∈ V |
8 | 6, 7 | opth 4220 |
. . . . . . . . . . . 12
⊢
(〈𝑧, 𝑤〉 = 〈𝑣, 𝑢〉 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)) |
9 | 5, 8 | sylib 121 |
. . . . . . . . . . 11
⊢ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) → (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)) |
10 | | oveq1 5857 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑣 → (𝑧 ·o 𝑢) = (𝑣 ·o 𝑢)) |
11 | | oveq2 5858 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (𝑣 ·o 𝑢) = (𝑣 ·o 𝑤)) |
12 | 11 | equcoms 1701 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑢 → (𝑣 ·o 𝑢) = (𝑣 ·o 𝑤)) |
13 | 10, 12 | sylan9eq 2223 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑧 ·o 𝑢) = (𝑣 ·o 𝑤)) |
14 | 9, 13 | syl 14 |
. . . . . . . . . 10
⊢ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) → (𝑧 ·o 𝑢) = (𝑣 ·o 𝑤)) |
15 | 14 | ancli 321 |
. . . . . . . . 9
⊢ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) → ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑣 ·o 𝑤))) |
16 | 15 | ad2ant2r 506 |
. . . . . . . 8
⊢ (((𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ (𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N))) → ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑣 ·o 𝑤))) |
17 | | pinn 7258 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ N →
𝑤 ∈
ω) |
18 | | nnmcom 6465 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ ω ∧ 𝑤 ∈ ω) → (𝑣 ·o 𝑤) = (𝑤 ·o 𝑣)) |
19 | 17, 18 | sylan2 284 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ ω ∧ 𝑤 ∈ N) →
(𝑣 ·o
𝑤) = (𝑤 ·o 𝑣)) |
20 | 19 | eqeq2d 2182 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ω ∧ 𝑤 ∈ N) →
((𝑧 ·o
𝑢) = (𝑣 ·o 𝑤) ↔ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
21 | 20 | ancoms 266 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ N ∧
𝑣 ∈ ω) →
((𝑧 ·o
𝑢) = (𝑣 ·o 𝑤) ↔ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
22 | 21 | ad2ant2lr 507 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ω ∧ 𝑤 ∈ N) ∧
(𝑣 ∈ ω ∧
𝑢 ∈ N))
→ ((𝑧
·o 𝑢) =
(𝑣 ·o
𝑤) ↔ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
23 | 22 | ad2ant2l 505 |
. . . . . . . . 9
⊢ (((𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ (𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N))) → ((𝑧 ·o 𝑢) = (𝑣 ·o 𝑤) ↔ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
24 | 23 | anbi2d 461 |
. . . . . . . 8
⊢ (((𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ (𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N))) → (((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑣 ·o 𝑤)) ↔ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
25 | 16, 24 | mpbid 146 |
. . . . . . 7
⊢ (((𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ (𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N))) → ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
26 | 25 | 2eximi 1594 |
. . . . . 6
⊢
(∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ (𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N))) →
∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
27 | 26 | 2eximi 1594 |
. . . . 5
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ N)) ∧ (𝑓 = 〈𝑣, 𝑢〉 ∧ (𝑣 ∈ ω ∧ 𝑢 ∈ N))) →
∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
28 | 4, 27 | syl 14 |
. . . 4
⊢ (𝑓 ∈ (ω ×
N) → ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) |
29 | 28 | ancli 321 |
. . 3
⊢ (𝑓 ∈ (ω ×
N) → (𝑓
∈ (ω × N) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
30 | | vex 2733 |
. . . . 5
⊢ 𝑓 ∈ V |
31 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑥 = 𝑓 → (𝑥 ∈ (ω × N)
↔ 𝑓 ∈ (ω
× N))) |
32 | 31 | anbi1d 462 |
. . . . . 6
⊢ (𝑥 = 𝑓 → ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ↔ (𝑓 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)))) |
33 | | eqeq1 2177 |
. . . . . . . . 9
⊢ (𝑥 = 𝑓 → (𝑥 = 〈𝑧, 𝑤〉 ↔ 𝑓 = 〈𝑧, 𝑤〉)) |
34 | 33 | anbi1d 462 |
. . . . . . . 8
⊢ (𝑥 = 𝑓 → ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ↔ (𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉))) |
35 | 34 | anbi1d 462 |
. . . . . . 7
⊢ (𝑥 = 𝑓 → (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
36 | 35 | 4exbidv 1863 |
. . . . . 6
⊢ (𝑥 = 𝑓 → (∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
37 | 32, 36 | anbi12d 470 |
. . . . 5
⊢ (𝑥 = 𝑓 → (((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑓 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))))) |
38 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑦 = 𝑓 → (𝑦 ∈ (ω × N)
↔ 𝑓 ∈ (ω
× N))) |
39 | 38 | anbi2d 461 |
. . . . . 6
⊢ (𝑦 = 𝑓 → ((𝑓 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ↔ (𝑓 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)))) |
40 | | eqeq1 2177 |
. . . . . . . . 9
⊢ (𝑦 = 𝑓 → (𝑦 = 〈𝑣, 𝑢〉 ↔ 𝑓 = 〈𝑣, 𝑢〉)) |
41 | 40 | anbi2d 461 |
. . . . . . . 8
⊢ (𝑦 = 𝑓 → ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ↔ (𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉))) |
42 | 41 | anbi1d 462 |
. . . . . . 7
⊢ (𝑦 = 𝑓 → (((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
43 | 42 | 4exbidv 1863 |
. . . . . 6
⊢ (𝑦 = 𝑓 → (∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
44 | 39, 43 | anbi12d 470 |
. . . . 5
⊢ (𝑦 = 𝑓 → (((𝑓 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑓 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))))) |
45 | | df-enq0 7373 |
. . . . 5
⊢
~Q0 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))} |
46 | 30, 30, 37, 44, 45 | brab 4255 |
. . . 4
⊢ (𝑓 ~Q0
𝑓 ↔ ((𝑓 ∈ (ω ×
N) ∧ 𝑓
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
47 | | anidm 394 |
. . . . 5
⊢ ((𝑓 ∈ (ω ×
N) ∧ 𝑓
∈ (ω × N)) ↔ 𝑓 ∈ (ω ×
N)) |
48 | 47 | anbi1i 455 |
. . . 4
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑓
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ (𝑓 ∈ (ω × N)
∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
49 | 46, 48 | bitri 183 |
. . 3
⊢ (𝑓 ~Q0
𝑓 ↔ (𝑓 ∈ (ω ×
N) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
50 | 29, 49 | sylibr 133 |
. 2
⊢ (𝑓 ∈ (ω ×
N) → 𝑓
~Q0 𝑓) |
51 | 49 | simplbi 272 |
. 2
⊢ (𝑓 ~Q0
𝑓 → 𝑓 ∈ (ω ×
N)) |
52 | 50, 51 | impbii 125 |
1
⊢ (𝑓 ∈ (ω ×
N) ↔ 𝑓
~Q0 𝑓) |