Step | Hyp | Ref
| Expression |
1 | | dmoprab 5902 |
. . 3
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q ))} =
{〈𝑥, 𝑦〉 ∣ ∃𝑧((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))} |
2 | | df-mqqs 7270 |
. . . 4
⊢
·Q = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))} |
3 | 2 | dmeqi 4787 |
. . 3
⊢ dom
·Q = dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))} |
4 | | dmaddpqlem 7297 |
. . . . . . . . 9
⊢ (𝑥 ∈ Q →
∃𝑤∃𝑣 𝑥 = [〈𝑤, 𝑣〉] ~Q
) |
5 | | dmaddpqlem 7297 |
. . . . . . . . 9
⊢ (𝑦 ∈ Q →
∃𝑢∃𝑓 𝑦 = [〈𝑢, 𝑓〉] ~Q
) |
6 | 4, 5 | anim12i 336 |
. . . . . . . 8
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (∃𝑤∃𝑣 𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
∃𝑢∃𝑓 𝑦 = [〈𝑢, 𝑓〉] ~Q
)) |
7 | | ee4anv 1914 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓(𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ↔
(∃𝑤∃𝑣 𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
∃𝑢∃𝑓 𝑦 = [〈𝑢, 𝑓〉] ~Q
)) |
8 | 6, 7 | sylibr 133 |
. . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ∃𝑤∃𝑣∃𝑢∃𝑓(𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q
)) |
9 | | enqex 7280 |
. . . . . . . . . . . . . 14
⊢
~Q ∈ V |
10 | | ecexg 6484 |
. . . . . . . . . . . . . 14
⊢ (
~Q ∈ V → [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q ∈
V) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
[(〈𝑤, 𝑣〉
·pQ 〈𝑢, 𝑓〉)] ~Q ∈
V |
12 | 11 | isseti 2720 |
. . . . . . . . . . . 12
⊢
∃𝑧 𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)]
~Q |
13 | | ax-ia3 107 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) →
(𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q →
((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))) |
14 | 13 | eximdv 1860 |
. . . . . . . . . . . 12
⊢ ((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) →
(∃𝑧 𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q →
∃𝑧((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))) |
15 | 12, 14 | mpi 15 |
. . . . . . . . . . 11
⊢ ((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) →
∃𝑧((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
)) |
16 | 15 | 2eximi 1581 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑓(𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) →
∃𝑢∃𝑓∃𝑧((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
)) |
17 | | exrot3 1670 |
. . . . . . . . . 10
⊢
(∃𝑧∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q ) ↔
∃𝑢∃𝑓∃𝑧((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
)) |
18 | 16, 17 | sylibr 133 |
. . . . . . . . 9
⊢
(∃𝑢∃𝑓(𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) →
∃𝑧∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
)) |
19 | 18 | 2eximi 1581 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓(𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) →
∃𝑤∃𝑣∃𝑧∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
)) |
20 | | exrot3 1670 |
. . . . . . . 8
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q ) ↔
∃𝑤∃𝑣∃𝑧∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
)) |
21 | 19, 20 | sylibr 133 |
. . . . . . 7
⊢
(∃𝑤∃𝑣∃𝑢∃𝑓(𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) →
∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
)) |
22 | 8, 21 | syl 14 |
. . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
)) |
23 | 22 | pm4.71i 389 |
. . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
↔ ((𝑥 ∈
Q ∧ 𝑦
∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))) |
24 | | 19.42v 1886 |
. . . . 5
⊢
(∃𝑧((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q ))
↔ ((𝑥 ∈
Q ∧ 𝑦
∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))) |
25 | 23, 24 | bitr4i 186 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
↔ ∃𝑧((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))) |
26 | 25 | opabbii 4031 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ Q ∧
𝑦 ∈ Q)}
= {〈𝑥, 𝑦〉 ∣ ∃𝑧((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)] ~Q
))} |
27 | 1, 3, 26 | 3eqtr4i 2188 |
. 2
⊢ dom
·Q = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ Q ∧ 𝑦 ∈
Q)} |
28 | | df-xp 4592 |
. 2
⊢
(Q × Q) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ Q ∧ 𝑦 ∈
Q)} |
29 | 27, 28 | eqtr4i 2181 |
1
⊢ dom
·Q = (Q ×
Q) |