Step | Hyp | Ref
| Expression |
1 | | vex 2733 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
2 | | vex 2733 |
. . . . . . . 8
⊢ 𝑔 ∈ V |
3 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑓 → (𝑥 ∈ (ω × N)
↔ 𝑓 ∈ (ω
× N))) |
4 | 3 | anbi1d 462 |
. . . . . . . . 9
⊢ (𝑥 = 𝑓 → ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ↔ (𝑓 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)))) |
5 | | eqeq1 2177 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑓 → (𝑥 = 〈𝑧, 𝑤〉 ↔ 𝑓 = 〈𝑧, 𝑤〉)) |
6 | 5 | anbi1d 462 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑓 → ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ↔ (𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉))) |
7 | 6 | anbi1d 462 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑓 → (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
8 | 7 | 4exbidv 1863 |
. . . . . . . . 9
⊢ (𝑥 = 𝑓 → (∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
9 | 4, 8 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑥 = 𝑓 → (((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑓 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))))) |
10 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑔 → (𝑦 ∈ (ω × N)
↔ 𝑔 ∈ (ω
× N))) |
11 | 10 | anbi2d 461 |
. . . . . . . . 9
⊢ (𝑦 = 𝑔 → ((𝑓 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ↔ (𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)))) |
12 | | eqeq1 2177 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑔 → (𝑦 = 〈𝑣, 𝑢〉 ↔ 𝑔 = 〈𝑣, 𝑢〉)) |
13 | 12 | anbi2d 461 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑔 → ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ↔ (𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉))) |
14 | 13 | anbi1d 462 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑔 → (((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
15 | 14 | 4exbidv 1863 |
. . . . . . . . 9
⊢ (𝑦 = 𝑔 → (∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
16 | 11, 15 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑦 = 𝑔 → (((𝑓 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))))) |
17 | | df-enq0 7373 |
. . . . . . . 8
⊢
~Q0 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))} |
18 | 1, 2, 9, 16, 17 | brab 4255 |
. . . . . . 7
⊢ (𝑓 ~Q0
𝑔 ↔ ((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
19 | 18 | biimpi 119 |
. . . . . 6
⊢ (𝑓 ~Q0
𝑔 → ((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
20 | | opeq12 3765 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → 〈𝑧, 𝑤〉 = 〈𝑎, 𝑏〉) |
21 | 20 | eqeq2d 2182 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → (𝑓 = 〈𝑧, 𝑤〉 ↔ 𝑓 = 〈𝑎, 𝑏〉)) |
22 | 21 | anbi1d 462 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → ((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ↔ (𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑣, 𝑢〉))) |
23 | | simpl 108 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → 𝑧 = 𝑎) |
24 | 23 | oveq1d 5865 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → (𝑧 ·o 𝑢) = (𝑎 ·o 𝑢)) |
25 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → 𝑤 = 𝑏) |
26 | 25 | oveq1d 5865 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → (𝑤 ·o 𝑣) = (𝑏 ·o 𝑣)) |
27 | 24, 26 | eqeq12d 2185 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → ((𝑧 ·o 𝑢) = (𝑤 ·o 𝑣) ↔ (𝑎 ·o 𝑢) = (𝑏 ·o 𝑣))) |
28 | 22, 27 | anbi12d 470 |
. . . . . . . 8
⊢ ((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) → (((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑎 ·o 𝑢) = (𝑏 ·o 𝑣)))) |
29 | | opeq12 3765 |
. . . . . . . . . . 11
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → 〈𝑣, 𝑢〉 = 〈𝑐, 𝑑〉) |
30 | 29 | eqeq2d 2182 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → (𝑔 = 〈𝑣, 𝑢〉 ↔ 𝑔 = 〈𝑐, 𝑑〉)) |
31 | 30 | anbi2d 461 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ↔ (𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉))) |
32 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → 𝑢 = 𝑑) |
33 | 32 | oveq2d 5866 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → (𝑎 ·o 𝑢) = (𝑎 ·o 𝑑)) |
34 | | simpl 108 |
. . . . . . . . . . 11
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → 𝑣 = 𝑐) |
35 | 34 | oveq2d 5866 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → (𝑏 ·o 𝑣) = (𝑏 ·o 𝑐)) |
36 | 33, 35 | eqeq12d 2185 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → ((𝑎 ·o 𝑢) = (𝑏 ·o 𝑣) ↔ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) |
37 | 31, 36 | anbi12d 470 |
. . . . . . . 8
⊢ ((𝑣 = 𝑐 ∧ 𝑢 = 𝑑) → (((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑎 ·o 𝑢) = (𝑏 ·o 𝑣)) ↔ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)))) |
38 | 28, 37 | cbvex4v 1923 |
. . . . . . 7
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) |
39 | 38 | anbi2i 454 |
. . . . . 6
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑓 = 〈𝑧, 𝑤〉 ∧ 𝑔 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)))) |
40 | 19, 39 | sylib 121 |
. . . . 5
⊢ (𝑓 ~Q0
𝑔 → ((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)))) |
41 | | 19.42vv 1904 |
. . . . 5
⊢
(∃𝑎∃𝑏((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ∃𝑐∃𝑑((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) ↔ ((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)))) |
42 | 40, 41 | sylibr 133 |
. . . 4
⊢ (𝑓 ~Q0
𝑔 → ∃𝑎∃𝑏((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ∃𝑐∃𝑑((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)))) |
43 | | 19.42vv 1904 |
. . . . 5
⊢
(∃𝑐∃𝑑((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) ↔ ((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ∃𝑐∃𝑑((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)))) |
44 | 43 | 2exbii 1599 |
. . . 4
⊢
(∃𝑎∃𝑏∃𝑐∃𝑑((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) ↔ ∃𝑎∃𝑏((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ∃𝑐∃𝑑((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)))) |
45 | 42, 44 | sylibr 133 |
. . 3
⊢ (𝑓 ~Q0
𝑔 → ∃𝑎∃𝑏∃𝑐∃𝑑((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)))) |
46 | | pm3.22 263 |
. . . . . . 7
⊢ ((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) → (𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N))) |
47 | 46 | adantr 274 |
. . . . . 6
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → (𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N))) |
48 | | pm3.22 263 |
. . . . . . 7
⊢ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) → (𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉)) |
49 | 48 | ad2antrl 487 |
. . . . . 6
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → (𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉)) |
50 | | simprr 527 |
. . . . . . . 8
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐)) |
51 | | eleq1 2233 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 〈𝑎, 𝑏〉 → (𝑓 ∈ (ω × N)
↔ 〈𝑎, 𝑏〉 ∈ (ω ×
N))) |
52 | | opelxp 4639 |
. . . . . . . . . . . . . 14
⊢
(〈𝑎, 𝑏〉 ∈ (ω ×
N) ↔ (𝑎
∈ ω ∧ 𝑏
∈ N)) |
53 | 51, 52 | bitrdi 195 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 〈𝑎, 𝑏〉 → (𝑓 ∈ (ω × N)
↔ (𝑎 ∈ ω
∧ 𝑏 ∈
N))) |
54 | 53 | biimpcd 158 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (ω ×
N) → (𝑓
= 〈𝑎, 𝑏〉 → (𝑎 ∈ ω ∧ 𝑏 ∈
N))) |
55 | | eleq1 2233 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 〈𝑐, 𝑑〉 → (𝑔 ∈ (ω × N)
↔ 〈𝑐, 𝑑〉 ∈ (ω ×
N))) |
56 | | opelxp 4639 |
. . . . . . . . . . . . . 14
⊢
(〈𝑐, 𝑑〉 ∈ (ω ×
N) ↔ (𝑐
∈ ω ∧ 𝑑
∈ N)) |
57 | 55, 56 | bitrdi 195 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 〈𝑐, 𝑑〉 → (𝑔 ∈ (ω × N)
↔ (𝑐 ∈ ω
∧ 𝑑 ∈
N))) |
58 | 57 | biimpcd 158 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (ω ×
N) → (𝑔
= 〈𝑐, 𝑑〉 → (𝑐 ∈ ω ∧ 𝑑 ∈
N))) |
59 | 54, 58 | im2anan9 593 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) → ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) → ((𝑎 ∈ ω ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ ω ∧ 𝑑 ∈
N)))) |
60 | 59 | imp 123 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ (𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉)) → ((𝑎 ∈ ω ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ ω ∧ 𝑑 ∈
N))) |
61 | 60 | adantrr 476 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → ((𝑎 ∈ ω ∧ 𝑏 ∈ N) ∧ (𝑐 ∈ ω ∧ 𝑑 ∈
N))) |
62 | | pinn 7258 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ N →
𝑑 ∈
ω) |
63 | | nnmcom 6465 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ω ∧ 𝑑 ∈ ω) → (𝑎 ·o 𝑑) = (𝑑 ·o 𝑎)) |
64 | 62, 63 | sylan2 284 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ω ∧ 𝑑 ∈ N) →
(𝑎 ·o
𝑑) = (𝑑 ·o 𝑎)) |
65 | | pinn 7258 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ N →
𝑏 ∈
ω) |
66 | | nnmcom 6465 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ω ∧ 𝑐 ∈ ω) → (𝑏 ·o 𝑐) = (𝑐 ·o 𝑏)) |
67 | 65, 66 | sylan 281 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ N ∧
𝑐 ∈ ω) →
(𝑏 ·o
𝑐) = (𝑐 ·o 𝑏)) |
68 | 64, 67 | eqeqan12d 2186 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ω ∧ 𝑑 ∈ N) ∧
(𝑏 ∈ N
∧ 𝑐 ∈ ω))
→ ((𝑎
·o 𝑑) =
(𝑏 ·o
𝑐) ↔ (𝑑 ·o 𝑎) = (𝑐 ·o 𝑏))) |
69 | 68 | an42s 584 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ω ∧ 𝑏 ∈ N) ∧
(𝑐 ∈ ω ∧
𝑑 ∈ N))
→ ((𝑎
·o 𝑑) =
(𝑏 ·o
𝑐) ↔ (𝑑 ·o 𝑎) = (𝑐 ·o 𝑏))) |
70 | 61, 69 | syl 14 |
. . . . . . . 8
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → ((𝑎 ·o 𝑑) = (𝑏 ·o 𝑐) ↔ (𝑑 ·o 𝑎) = (𝑐 ·o 𝑏))) |
71 | 50, 70 | mpbid 146 |
. . . . . . 7
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → (𝑑 ·o 𝑎) = (𝑐 ·o 𝑏)) |
72 | 71 | eqcomd 2176 |
. . . . . 6
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)) |
73 | 47, 49, 72 | jca32 308 |
. . . . 5
⊢ (((𝑓 ∈ (ω ×
N) ∧ 𝑔
∈ (ω × N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → ((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
74 | 73 | 2eximi 1594 |
. . . 4
⊢
(∃𝑐∃𝑑((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → ∃𝑐∃𝑑((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
75 | 74 | 2eximi 1594 |
. . 3
⊢
(∃𝑎∃𝑏∃𝑐∃𝑑((𝑓 ∈ (ω × N)
∧ 𝑔 ∈ (ω
× N)) ∧ ((𝑓 = 〈𝑎, 𝑏〉 ∧ 𝑔 = 〈𝑐, 𝑑〉) ∧ (𝑎 ·o 𝑑) = (𝑏 ·o 𝑐))) → ∃𝑎∃𝑏∃𝑐∃𝑑((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
76 | 45, 75 | syl 14 |
. 2
⊢ (𝑓 ~Q0
𝑔 → ∃𝑎∃𝑏∃𝑐∃𝑑((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
77 | | exrot4 1684 |
. . 3
⊢
(∃𝑎∃𝑏∃𝑐∃𝑑((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) ↔ ∃𝑐∃𝑑∃𝑎∃𝑏((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
78 | | 19.42vv 1904 |
. . . . 5
⊢
(∃𝑎∃𝑏((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) ↔ ((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ∃𝑎∃𝑏((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
79 | 78 | 2exbii 1599 |
. . . 4
⊢
(∃𝑐∃𝑑∃𝑎∃𝑏((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) ↔ ∃𝑐∃𝑑((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ∃𝑎∃𝑏((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
80 | | 19.42vv 1904 |
. . . . 5
⊢
(∃𝑐∃𝑑((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ∃𝑎∃𝑏((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) ↔ ((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ∃𝑐∃𝑑∃𝑎∃𝑏((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
81 | | opeq12 3765 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 〈𝑧, 𝑤〉 = 〈𝑐, 𝑑〉) |
82 | 81 | eqeq2d 2182 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑔 = 〈𝑧, 𝑤〉 ↔ 𝑔 = 〈𝑐, 𝑑〉)) |
83 | 82 | anbi1d 462 |
. . . . . . . 8
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → ((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ↔ (𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑣, 𝑢〉))) |
84 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 𝑧 = 𝑐) |
85 | 84 | oveq1d 5865 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑧 ·o 𝑢) = (𝑐 ·o 𝑢)) |
86 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 𝑤 = 𝑑) |
87 | 86 | oveq1d 5865 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑤 ·o 𝑣) = (𝑑 ·o 𝑣)) |
88 | 85, 87 | eqeq12d 2185 |
. . . . . . . 8
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → ((𝑧 ·o 𝑢) = (𝑤 ·o 𝑣) ↔ (𝑐 ·o 𝑢) = (𝑑 ·o 𝑣))) |
89 | 83, 88 | anbi12d 470 |
. . . . . . 7
⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑐 ·o 𝑢) = (𝑑 ·o 𝑣)))) |
90 | | opeq12 3765 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → 〈𝑣, 𝑢〉 = 〈𝑎, 𝑏〉) |
91 | 90 | eqeq2d 2182 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → (𝑓 = 〈𝑣, 𝑢〉 ↔ 𝑓 = 〈𝑎, 𝑏〉)) |
92 | 91 | anbi2d 461 |
. . . . . . . 8
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ↔ (𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉))) |
93 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → 𝑢 = 𝑏) |
94 | 93 | oveq2d 5866 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → (𝑐 ·o 𝑢) = (𝑐 ·o 𝑏)) |
95 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → 𝑣 = 𝑎) |
96 | 95 | oveq2d 5866 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → (𝑑 ·o 𝑣) = (𝑑 ·o 𝑎)) |
97 | 94, 96 | eqeq12d 2185 |
. . . . . . . 8
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → ((𝑐 ·o 𝑢) = (𝑑 ·o 𝑣) ↔ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) |
98 | 92, 97 | anbi12d 470 |
. . . . . . 7
⊢ ((𝑣 = 𝑎 ∧ 𝑢 = 𝑏) → (((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑐 ·o 𝑢) = (𝑑 ·o 𝑣)) ↔ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎)))) |
99 | 89, 98 | cbvex4v 1923 |
. . . . . 6
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ∃𝑐∃𝑑∃𝑎∃𝑏((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) |
100 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑔 → (𝑥 ∈ (ω × N)
↔ 𝑔 ∈ (ω
× N))) |
101 | 100 | anbi1d 462 |
. . . . . . . . 9
⊢ (𝑥 = 𝑔 → ((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ↔ (𝑔 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)))) |
102 | | eqeq1 2177 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑔 → (𝑥 = 〈𝑧, 𝑤〉 ↔ 𝑔 = 〈𝑧, 𝑤〉)) |
103 | 102 | anbi1d 462 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑔 → ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ↔ (𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉))) |
104 | 103 | anbi1d 462 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑔 → (((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
105 | 104 | 4exbidv 1863 |
. . . . . . . . 9
⊢ (𝑥 = 𝑔 → (∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
106 | 101, 105 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑥 = 𝑔 → (((𝑥 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑔 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))))) |
107 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑓 → (𝑦 ∈ (ω × N)
↔ 𝑓 ∈ (ω
× N))) |
108 | 107 | anbi2d 461 |
. . . . . . . . 9
⊢ (𝑦 = 𝑓 → ((𝑔 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ↔ (𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)))) |
109 | | eqeq1 2177 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑓 → (𝑦 = 〈𝑣, 𝑢〉 ↔ 𝑓 = 〈𝑣, 𝑢〉)) |
110 | 109 | anbi2d 461 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑓 → ((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ↔ (𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉))) |
111 | 110 | anbi1d 462 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑓 → (((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
112 | 111 | 4exbidv 1863 |
. . . . . . . . 9
⊢ (𝑦 = 𝑓 → (∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
113 | 108, 112 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑦 = 𝑓 → (((𝑔 ∈ (ω × N)
∧ 𝑦 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) ↔ ((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))))) |
114 | 2, 1, 106, 113, 17 | brab 4255 |
. . . . . . 7
⊢ (𝑔 ~Q0
𝑓 ↔ ((𝑔 ∈ (ω ×
N) ∧ 𝑓
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))) |
115 | 114 | biimpri 132 |
. . . . . 6
⊢ (((𝑔 ∈ (ω ×
N) ∧ 𝑓
∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑔 = 〈𝑧, 𝑤〉 ∧ 𝑓 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣))) → 𝑔 ~Q0 𝑓) |
116 | 99, 115 | sylan2br 286 |
. . . . 5
⊢ (((𝑔 ∈ (ω ×
N) ∧ 𝑓
∈ (ω × N)) ∧ ∃𝑐∃𝑑∃𝑎∃𝑏((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) → 𝑔 ~Q0 𝑓) |
117 | 80, 116 | sylbi 120 |
. . . 4
⊢
(∃𝑐∃𝑑((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ∃𝑎∃𝑏((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) → 𝑔 ~Q0 𝑓) |
118 | 79, 117 | sylbi 120 |
. . 3
⊢
(∃𝑐∃𝑑∃𝑎∃𝑏((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) → 𝑔 ~Q0 𝑓) |
119 | 77, 118 | sylbi 120 |
. 2
⊢
(∃𝑎∃𝑏∃𝑐∃𝑑((𝑔 ∈ (ω × N)
∧ 𝑓 ∈ (ω
× N)) ∧ ((𝑔 = 〈𝑐, 𝑑〉 ∧ 𝑓 = 〈𝑎, 𝑏〉) ∧ (𝑐 ·o 𝑏) = (𝑑 ·o 𝑎))) → 𝑔 ~Q0 𝑓) |
120 | 76, 119 | syl 14 |
1
⊢ (𝑓 ~Q0
𝑔 → 𝑔 ~Q0 𝑓) |