Step | Hyp | Ref
| Expression |
1 | | dmoprab 5955 |
. . 3
⊢ dom
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q ))} =
{⟨𝑥, 𝑦⟩ ∣ ∃𝑧((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))} |
2 | | df-plqqs 7347 |
. . . 4
⊢
+Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))} |
3 | 2 | dmeqi 4828 |
. . 3
⊢ dom
+Q = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))} |
4 | | dmaddpqlem 7375 |
. . . . . . . . 9
⊢ (𝑥 ∈ Q →
∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q
) |
5 | | dmaddpqlem 7375 |
. . . . . . . . 9
⊢ (𝑦 ∈ Q →
∃𝑢∃𝑓 𝑦 = [⟨𝑢, 𝑓⟩] ~Q
) |
6 | 4, 5 | anim12i 338 |
. . . . . . . 8
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
∃𝑢∃𝑓 𝑦 = [⟨𝑢, 𝑓⟩] ~Q
)) |
7 | | ee4anv 1934 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓(𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ↔
(∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
∃𝑢∃𝑓 𝑦 = [⟨𝑢, 𝑓⟩] ~Q
)) |
8 | 6, 7 | sylibr 134 |
. . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ∃𝑤∃𝑣∃𝑢∃𝑓(𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q
)) |
9 | | enqex 7358 |
. . . . . . . . . . . . . 14
⊢
~Q ∈ V |
10 | | ecexg 6538 |
. . . . . . . . . . . . . 14
⊢ (
~Q ∈ V → [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q ∈
V) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
[(⟨𝑤, 𝑣⟩
+pQ ⟨𝑢, 𝑓⟩)] ~Q ∈
V |
12 | 11 | isseti 2745 |
. . . . . . . . . . . 12
⊢
∃𝑧 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)]
~Q |
13 | | ax-ia3 108 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) →
(𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q →
((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))) |
14 | 13 | eximdv 1880 |
. . . . . . . . . . . 12
⊢ ((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) →
(∃𝑧 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q →
∃𝑧((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))) |
15 | 12, 14 | mpi 15 |
. . . . . . . . . . 11
⊢ ((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) →
∃𝑧((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
)) |
16 | 15 | 2eximi 1601 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓(𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) →
∃𝑢∃𝑓∃𝑧((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
)) |
17 | | exrot3 1690 |
. . . . . . . . . 10
⊢
(∃𝑧∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q ) ↔
∃𝑢∃𝑓∃𝑧((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
)) |
18 | 16, 17 | sylibr 134 |
. . . . . . . . 9
⊢
(∃𝑢∃𝑓(𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) →
∃𝑧∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
)) |
19 | 18 | 2eximi 1601 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓(𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) →
∃𝑤∃𝑣∃𝑧∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
)) |
20 | | exrot3 1690 |
. . . . . . . 8
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q ) ↔
∃𝑤∃𝑣∃𝑧∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
)) |
21 | 19, 20 | sylibr 134 |
. . . . . . 7
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓(𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) →
∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
)) |
22 | 8, 21 | syl 14 |
. . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
)) |
23 | 22 | pm4.71i 391 |
. . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
↔ ((𝑥 ∈
Q ∧ 𝑦
∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))) |
24 | | 19.42v 1906 |
. . . . 5
⊢
(∃𝑧((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q ))
↔ ((𝑥 ∈
Q ∧ 𝑦
∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))) |
25 | 23, 24 | bitr4i 187 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
↔ ∃𝑧((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))) |
26 | 25 | opabbii 4070 |
. . 3
⊢
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧
𝑦 ∈ Q)}
= {⟨𝑥, 𝑦⟩ ∣ ∃𝑧((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧
𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧
𝑧 = [(⟨𝑤, 𝑣⟩ +pQ
⟨𝑢, 𝑓⟩)] ~Q
))} |
27 | 1, 3, 26 | 3eqtr4i 2208 |
. 2
⊢ dom
+Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈
Q)} |
28 | | df-xp 4632 |
. 2
⊢
(Q × Q) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈
Q)} |
29 | 27, 28 | eqtr4i 2201 |
1
⊢ dom
+Q = (Q ×
Q) |