Step | Hyp | Ref
| Expression |
1 | | df-mpt2 5460 |
. 2
⊢ (x ∈
(N × N), y ∈
(N × N) ↦ ⟨((1^{st}
‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩) =
{⟨⟨x, y⟩, z⟩
∣ ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ z =
⟨((1^{st} ‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩)} |
2 | | df-mpq 6329 |
. 2
⊢
·_{pQ} = (x
∈ (N × N),
y ∈
(N × N) ↦ ⟨((1^{st}
‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩) |
3 | | 1st2nd2 5743 |
. . . . . . . . . 10
⊢ (x ∈
(N × N) → x = ⟨(1^{st} ‘x), (2^{nd} ‘x)⟩) |
4 | 3 | eqeq1d 2045 |
. . . . . . . . 9
⊢ (x ∈
(N × N) → (x = ⟨w,
v⟩ ↔ ⟨(1^{st}
‘x), (2^{nd} ‘x)⟩ = ⟨w, v⟩)) |
5 | | 1st2nd2 5743 |
. . . . . . . . . 10
⊢ (y ∈
(N × N) → y = ⟨(1^{st} ‘y), (2^{nd} ‘y)⟩) |
6 | 5 | eqeq1d 2045 |
. . . . . . . . 9
⊢ (y ∈
(N × N) → (y = ⟨u,
f⟩ ↔ ⟨(1^{st}
‘y), (2^{nd} ‘y)⟩ = ⟨u, f⟩)) |
7 | 4, 6 | bi2anan9 538 |
. . . . . . . 8
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
((x = ⟨w, v⟩ ∧ y =
⟨u, f⟩) ↔ (⟨(1^{st}
‘x), (2^{nd} ‘x)⟩ = ⟨w, v⟩ ∧ ⟨(1^{st} ‘y), (2^{nd} ‘y)⟩ = ⟨u, f⟩))) |
8 | 7 | anbi1d 438 |
. . . . . . 7
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(((x = ⟨w, v⟩ ∧ y =
⟨u, f⟩) ∧ z = ⟨(w
·_{N} u),
(v ·_{N}
f)⟩) ↔ ((⟨(1^{st}
‘x), (2^{nd} ‘x)⟩ = ⟨w, v⟩ ∧ ⟨(1^{st} ‘y), (2^{nd} ‘y)⟩ = ⟨u, f⟩)
∧ z =
⟨(w ·_{N}
u), (v
·_{N} f)⟩))) |
9 | 8 | bicomd 129 |
. . . . . 6
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(((⟨(1^{st} ‘x),
(2^{nd} ‘x)⟩ =
⟨w, v⟩ ∧
⟨(1^{st} ‘y),
(2^{nd} ‘y)⟩ =
⟨u, f⟩) ∧ z = ⟨(w
·_{N} u),
(v ·_{N}
f)⟩) ↔ ((x = ⟨w,
v⟩ ∧
y = ⟨u, f⟩)
∧ z =
⟨(w ·_{N}
u), (v
·_{N} f)⟩))) |
10 | 9 | 4exbidv 1747 |
. . . . 5
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(∃w∃v∃u∃f((⟨(1^{st} ‘x), (2^{nd} ‘x)⟩ = ⟨w, v⟩ ∧ ⟨(1^{st} ‘y), (2^{nd} ‘y)⟩ = ⟨u, f⟩)
∧ z =
⟨(w ·_{N}
u), (v
·_{N} f)⟩) ↔ ∃w∃v∃u∃f((x = ⟨w,
v⟩ ∧
y = ⟨u, f⟩)
∧ z =
⟨(w ·_{N}
u), (v
·_{N} f)⟩))) |
11 | | xp1st 5734 |
. . . . . . 7
⊢ (x ∈
(N × N) → (1^{st}
‘x) ∈ N) |
12 | | xp2nd 5735 |
. . . . . . 7
⊢ (x ∈
(N × N) → (2^{nd}
‘x) ∈ N) |
13 | 11, 12 | jca 290 |
. . . . . 6
⊢ (x ∈
(N × N) → ((1^{st}
‘x) ∈ N ∧ (2^{nd} ‘x) ∈
N)) |
14 | | xp1st 5734 |
. . . . . . 7
⊢ (y ∈
(N × N) → (1^{st}
‘y) ∈ N) |
15 | | xp2nd 5735 |
. . . . . . 7
⊢ (y ∈
(N × N) → (2^{nd}
‘y) ∈ N) |
16 | 14, 15 | jca 290 |
. . . . . 6
⊢ (y ∈
(N × N) → ((1^{st}
‘y) ∈ N ∧ (2^{nd} ‘y) ∈
N)) |
17 | | simpll 481 |
. . . . . . . . . 10
⊢
(((w = (1^{st}
‘x) ∧ v =
(2^{nd} ‘x)) ∧ (u =
(1^{st} ‘y) ∧ f =
(2^{nd} ‘y))) → w = (1^{st} ‘x)) |
18 | | simprl 483 |
. . . . . . . . . 10
⊢
(((w = (1^{st}
‘x) ∧ v =
(2^{nd} ‘x)) ∧ (u =
(1^{st} ‘y) ∧ f =
(2^{nd} ‘y))) → u = (1^{st} ‘y)) |
19 | 17, 18 | oveq12d 5473 |
. . . . . . . . 9
⊢
(((w = (1^{st}
‘x) ∧ v =
(2^{nd} ‘x)) ∧ (u =
(1^{st} ‘y) ∧ f =
(2^{nd} ‘y))) →
(w ·_{N}
u) = ((1^{st} ‘x) ·_{N}
(1^{st} ‘y))) |
20 | | simplr 482 |
. . . . . . . . . 10
⊢
(((w = (1^{st}
‘x) ∧ v =
(2^{nd} ‘x)) ∧ (u =
(1^{st} ‘y) ∧ f =
(2^{nd} ‘y))) → v = (2^{nd} ‘x)) |
21 | | simprr 484 |
. . . . . . . . . 10
⊢
(((w = (1^{st}
‘x) ∧ v =
(2^{nd} ‘x)) ∧ (u =
(1^{st} ‘y) ∧ f =
(2^{nd} ‘y))) → f = (2^{nd} ‘y)) |
22 | 20, 21 | oveq12d 5473 |
. . . . . . . . 9
⊢
(((w = (1^{st}
‘x) ∧ v =
(2^{nd} ‘x)) ∧ (u =
(1^{st} ‘y) ∧ f =
(2^{nd} ‘y))) →
(v ·_{N}
f) = ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))) |
23 | 19, 22 | opeq12d 3548 |
. . . . . . . 8
⊢
(((w = (1^{st}
‘x) ∧ v =
(2^{nd} ‘x)) ∧ (u =
(1^{st} ‘y) ∧ f =
(2^{nd} ‘y))) →
⟨(w ·_{N}
u), (v
·_{N} f)⟩
= ⟨((1^{st} ‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩) |
24 | 23 | eqeq2d 2048 |
. . . . . . 7
⊢
(((w = (1^{st}
‘x) ∧ v =
(2^{nd} ‘x)) ∧ (u =
(1^{st} ‘y) ∧ f =
(2^{nd} ‘y))) →
(z = ⟨(w ·_{N} u), (v
·_{N} f)⟩
↔ z = ⟨((1^{st}
‘x)
·_{N} (1^{st} ‘y)), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩)) |
25 | 24 | copsex4g 3975 |
. . . . . 6
⊢
((((1^{st} ‘x) ∈ N ∧ (2^{nd} ‘x) ∈
N) ∧ ((1^{st}
‘y) ∈ N ∧ (2^{nd} ‘y) ∈
N)) → (∃w∃v∃u∃f((⟨(1^{st} ‘x), (2^{nd} ‘x)⟩ = ⟨w, v⟩ ∧ ⟨(1^{st} ‘y), (2^{nd} ‘y)⟩ = ⟨u, f⟩)
∧ z =
⟨(w ·_{N}
u), (v
·_{N} f)⟩) ↔ z = ⟨((1^{st} ‘x) ·_{N}
(1^{st} ‘y)),
((2^{nd} ‘x)
·_{N} (2^{nd} ‘y))⟩)) |
26 | 13, 16, 25 | syl2an 273 |
. . . . 5
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(∃w∃v∃u∃f((⟨(1^{st} ‘x), (2^{nd} ‘x)⟩ = ⟨w, v⟩ ∧ ⟨(1^{st} ‘y), (2^{nd} ‘y)⟩ = ⟨u, f⟩)
∧ z =
⟨(w ·_{N}
u), (v
·_{N} f)⟩) ↔ z = ⟨((1^{st} ‘x) ·_{N}
(1^{st} ‘y)),
((2^{nd} ‘x)
·_{N} (2^{nd} ‘y))⟩)) |
27 | 10, 26 | bitr3d 179 |
. . . 4
⊢
((x ∈ (N × N) ∧ y ∈ (N × N)) →
(∃w∃v∃u∃f((x = ⟨w,
v⟩ ∧
y = ⟨u, f⟩)
∧ z =
⟨(w ·_{N}
u), (v
·_{N} f)⟩) ↔ z = ⟨((1^{st} ‘x) ·_{N}
(1^{st} ‘y)),
((2^{nd} ‘x)
·_{N} (2^{nd} ‘y))⟩)) |
28 | 27 | pm5.32i 427 |
. . 3
⊢
(((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x =
⟨w, v⟩ ∧ y = ⟨u,
f⟩) ∧
z = ⟨(w ·_{N} u), (v
·_{N} f)⟩)) ↔ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
z = ⟨((1^{st} ‘x) ·_{N}
(1^{st} ‘y)),
((2^{nd} ‘x)
·_{N} (2^{nd} ‘y))⟩)) |
29 | 28 | oprabbii 5502 |
. 2
⊢
{⟨⟨x, y⟩, z⟩
∣ ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x =
⟨w, v⟩ ∧ y = ⟨u,
f⟩) ∧
z = ⟨(w ·_{N} u), (v
·_{N} f)⟩))} = {⟨⟨x, y⟩,
z⟩ ∣ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
z = ⟨((1^{st} ‘x) ·_{N}
(1^{st} ‘y)),
((2^{nd} ‘x)
·_{N} (2^{nd} ‘y))⟩)} |
30 | 1, 2, 29 | 3eqtr4i 2067 |
1
⊢
·_{pQ} = {⟨⟨x, y⟩,
z⟩ ∣ ((x ∈
(N × N) ∧
y ∈
(N × N)) ∧
∃w∃v∃u∃f((x = ⟨w,
v⟩ ∧
y = ⟨u, f⟩)
∧ z =
⟨(w ·_{N}
u), (v
·_{N} f)⟩))} |