Step | Hyp | Ref
| Expression |
1 | | dmoprab 5527 |
. . 3
⊢ dom
{〈〈x, y〉, z〉
∣ ((x ∈ Q ∧ y ∈ Q) ∧ ∃w∃v∃u∃f((x =
[〈w, v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q ))} =
{〈x, y〉 ∣ ∃z((x ∈
Q ∧ y ∈
Q) ∧ ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))} |
2 | | df-mqqs 6334 |
. . . 4
⊢
·Q = {〈〈x, y〉,
z〉 ∣ ((x ∈
Q ∧ y ∈
Q) ∧ ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))} |
3 | 2 | dmeqi 4479 |
. . 3
⊢ dom
·Q = dom {〈〈x, y〉,
z〉 ∣ ((x ∈
Q ∧ y ∈
Q) ∧ ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))} |
4 | | dmaddpqlem 6361 |
. . . . . . . . 9
⊢ (x ∈
Q → ∃w∃v x =
[〈w, v〉] ~Q
) |
5 | | dmaddpqlem 6361 |
. . . . . . . . 9
⊢ (y ∈
Q → ∃u∃f y =
[〈u, f〉] ~Q
) |
6 | 4, 5 | anim12i 321 |
. . . . . . . 8
⊢
((x ∈ Q ∧ y ∈ Q) → (∃w∃v x = [〈w,
v〉] ~Q ∧ ∃u∃f y =
[〈u, f〉] ~Q
)) |
7 | | ee4anv 1806 |
. . . . . . . 8
⊢ (∃w∃v∃u∃f(x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ↔ (∃w∃v x = [〈w,
v〉] ~Q ∧ ∃u∃f y =
[〈u, f〉] ~Q
)) |
8 | 6, 7 | sylibr 137 |
. . . . . . 7
⊢
((x ∈ Q ∧ y ∈ Q) → ∃w∃v∃u∃f(x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q
)) |
9 | | enqex 6344 |
. . . . . . . . . . . . . 14
⊢
~Q ∈
V |
10 | | ecexg 6046 |
. . . . . . . . . . . . . 14
⊢ (
~Q ∈ V →
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q ∈ V) |
11 | 9, 10 | ax-mp 7 |
. . . . . . . . . . . . 13
⊢
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q ∈ V |
12 | 11 | isseti 2557 |
. . . . . . . . . . . 12
⊢ ∃z z = [(〈w,
v〉 ·pQ
〈u, f〉)]
~Q |
13 | | ax-ia3 101 |
. . . . . . . . . . . . 13
⊢
((x = [〈w, v〉]
~Q ∧ y = [〈u,
f〉] ~Q )
→ (z = [(〈w, v〉
·pQ 〈u, f〉)]
~Q → ((x =
[〈w, v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))) |
14 | 13 | eximdv 1757 |
. . . . . . . . . . . 12
⊢
((x = [〈w, v〉]
~Q ∧ y = [〈u,
f〉] ~Q )
→ (∃z z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q → ∃z((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))) |
15 | 12, 14 | mpi 15 |
. . . . . . . . . . 11
⊢
((x = [〈w, v〉]
~Q ∧ y = [〈u,
f〉] ~Q )
→ ∃z((x =
[〈w, v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
)) |
16 | 15 | 2eximi 1489 |
. . . . . . . . . 10
⊢ (∃u∃f(x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) → ∃u∃f∃z((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
)) |
17 | | exrot3 1577 |
. . . . . . . . . 10
⊢ (∃z∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q ) ↔ ∃u∃f∃z((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
)) |
18 | 16, 17 | sylibr 137 |
. . . . . . . . 9
⊢ (∃u∃f(x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) → ∃z∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
)) |
19 | 18 | 2eximi 1489 |
. . . . . . . 8
⊢ (∃w∃v∃u∃f(x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) → ∃w∃v∃z∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
)) |
20 | | exrot3 1577 |
. . . . . . . 8
⊢ (∃z∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q ) ↔ ∃w∃v∃z∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
)) |
21 | 19, 20 | sylibr 137 |
. . . . . . 7
⊢ (∃w∃v∃u∃f(x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) → ∃z∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
)) |
22 | 8, 21 | syl 14 |
. . . . . 6
⊢
((x ∈ Q ∧ y ∈ Q) → ∃z∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
)) |
23 | 22 | pm4.71i 371 |
. . . . 5
⊢
((x ∈ Q ∧ y ∈ Q) ↔ ((x ∈
Q ∧ y ∈
Q) ∧ ∃z∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))) |
24 | | 19.42v 1783 |
. . . . 5
⊢ (∃z((x ∈
Q ∧ y ∈
Q) ∧ ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q )) ↔
((x ∈
Q ∧ y ∈
Q) ∧ ∃z∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))) |
25 | 23, 24 | bitr4i 176 |
. . . 4
⊢
((x ∈ Q ∧ y ∈ Q) ↔ ∃z((x ∈
Q ∧ y ∈
Q) ∧ ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))) |
26 | 25 | opabbii 3815 |
. . 3
⊢
{〈x, y〉 ∣ (x ∈
Q ∧ y ∈
Q)} = {〈x, y〉 ∣ ∃z((x ∈
Q ∧ y ∈
Q) ∧ ∃w∃v∃u∃f((x = [〈w,
v〉] ~Q ∧ y =
[〈u, f〉] ~Q ) ∧ z =
[(〈w, v〉 ·pQ
〈u, f〉)] ~Q
))} |
27 | 1, 3, 26 | 3eqtr4i 2067 |
. 2
⊢ dom
·Q = {〈x, y〉
∣ (x ∈ Q ∧ y ∈ Q)} |
28 | | df-xp 4294 |
. 2
⊢
(Q × Q) = {〈x, y〉
∣ (x ∈ Q ∧ y ∈ Q)} |
29 | 27, 28 | eqtr4i 2060 |
1
⊢ dom
·Q = (Q ×
Q) |