Proof of Theorem dfplq0qs
Step | Hyp | Ref
| Expression |
1 | | df-plq0 7376 |
. 2
⊢
+Q0 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q0 ∧
𝑦 ∈
Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
))} |
2 | | df-nq0 7374 |
. . . . . 6
⊢
Q0 = ((ω × N)
/ ~Q0 ) |
3 | 2 | eleq2i 2237 |
. . . . 5
⊢ (𝑥 ∈
Q0 ↔ 𝑥 ∈ ((ω × N)
/ ~Q0 )) |
4 | 2 | eleq2i 2237 |
. . . . 5
⊢ (𝑦 ∈
Q0 ↔ 𝑦 ∈ ((ω × N)
/ ~Q0 )) |
5 | 3, 4 | anbi12i 457 |
. . . 4
⊢ ((𝑥 ∈
Q0 ∧ 𝑦 ∈ Q0) ↔
(𝑥 ∈ ((ω ×
N) / ~Q0 ) ∧ 𝑦 ∈ ((ω ×
N) / ~Q0 ))) |
6 | 5 | anbi1i 455 |
. . 3
⊢ (((𝑥 ∈
Q0 ∧ 𝑦 ∈ Q0) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0 ))
↔ ((𝑥 ∈ ((ω
× N) / ~Q0 ) ∧ 𝑦 ∈ ((ω ×
N) / ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
))) |
7 | 6 | oprabbii 5905 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q0 ∧
𝑦 ∈
Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0 ))} =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((ω × N)
/ ~Q0 ) ∧ 𝑦 ∈ ((ω × N)
/ ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
))} |
8 | 1, 7 | eqtri 2191 |
1
⊢
+Q0 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((ω × N)
/ ~Q0 ) ∧ 𝑦 ∈ ((ω × N)
/ ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
))} |