Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . . . 7
⊢ c ∈
V |
2 | | vex 2862 |
. . . . . . 7
⊢ d ∈
V |
3 | 1, 2 | opex 4588 |
. . . . . 6
⊢ 〈c, d〉 ∈ V |
4 | 3 | isseti 2865 |
. . . . 5
⊢ ∃x x = 〈c, d〉 |
5 | | 19.41v 1901 |
. . . . 5
⊢ (∃x(x = 〈c, d〉 ∧ (aAc ∧ bBd)) ↔ (∃x x = 〈c, d〉 ∧ (aAc ∧ bBd))) |
6 | 4, 5 | mpbiran 884 |
. . . 4
⊢ (∃x(x = 〈c, d〉 ∧ (aAc ∧ bBd)) ↔ (aAc ∧ bBd)) |
7 | 6 | 2exbii 1583 |
. . 3
⊢ (∃c∃d∃x(x = 〈c, d〉 ∧ (aAc ∧ bBd)) ↔ ∃c∃d(aAc ∧ bBd)) |
8 | | df-br 4640 |
. . . 4
⊢ (adom PProd (A, B)b ↔ 〈a, b〉 ∈ dom PProd (A, B)) |
9 | | eldm 4898 |
. . . 4
⊢ (〈a, b〉 ∈ dom PProd (A, B) ↔
∃x〈a, b〉 PProd (A, B)x) |
10 | | brpprod 5839 |
. . . . . . 7
⊢ (〈a, b〉 PProd (A, B)x ↔ ∃t∃u∃c∃d(〈a, b〉 = 〈t, u〉 ∧ x = 〈c, d〉 ∧ (tAc ∧ uBd))) |
11 | | 19.42vv 1907 |
. . . . . . . . 9
⊢ (∃c∃d((t = a ∧ u = b) ∧ (x = 〈c, d〉 ∧ (tAc ∧ uBd))) ↔ ((t
= a ∧
u = b)
∧ ∃c∃d(x = 〈c, d〉 ∧ (tAc ∧ uBd)))) |
12 | | 3anass 938 |
. . . . . . . . . . 11
⊢ ((〈a, b〉 = 〈t, u〉 ∧ x = 〈c, d〉 ∧ (tAc ∧ uBd)) ↔
(〈a,
b〉 =
〈t,
u〉 ∧ (x = 〈c, d〉 ∧ (tAc ∧ uBd)))) |
13 | | eqcom 2355 |
. . . . . . . . . . . . 13
⊢ (〈a, b〉 = 〈t, u〉 ↔ 〈t, u〉 = 〈a, b〉) |
14 | | opth 4602 |
. . . . . . . . . . . . 13
⊢ (〈t, u〉 = 〈a, b〉 ↔
(t = a
∧ u =
b)) |
15 | 13, 14 | bitri 240 |
. . . . . . . . . . . 12
⊢ (〈a, b〉 = 〈t, u〉 ↔
(t = a
∧ u =
b)) |
16 | 15 | anbi1i 676 |
. . . . . . . . . . 11
⊢ ((〈a, b〉 = 〈t, u〉 ∧ (x = 〈c, d〉 ∧ (tAc ∧ uBd))) ↔
((t = a
∧ u =
b) ∧
(x = 〈c, d〉 ∧ (tAc ∧ uBd)))) |
17 | 12, 16 | bitri 240 |
. . . . . . . . . 10
⊢ ((〈a, b〉 = 〈t, u〉 ∧ x = 〈c, d〉 ∧ (tAc ∧ uBd)) ↔
((t = a
∧ u =
b) ∧
(x = 〈c, d〉 ∧ (tAc ∧ uBd)))) |
18 | 17 | 2exbii 1583 |
. . . . . . . . 9
⊢ (∃c∃d(〈a, b〉 = 〈t, u〉 ∧ x = 〈c, d〉 ∧ (tAc ∧ uBd)) ↔
∃c∃d((t = a ∧ u = b) ∧ (x = 〈c, d〉 ∧ (tAc ∧ uBd)))) |
19 | | df-3an 936 |
. . . . . . . . 9
⊢ ((t = a ∧ u = b ∧ ∃c∃d(x = 〈c, d〉 ∧ (tAc ∧ uBd))) ↔ ((t
= a ∧
u = b)
∧ ∃c∃d(x = 〈c, d〉 ∧ (tAc ∧ uBd)))) |
20 | 11, 18, 19 | 3bitr4i 268 |
. . . . . . . 8
⊢ (∃c∃d(〈a, b〉 = 〈t, u〉 ∧ x = 〈c, d〉 ∧ (tAc ∧ uBd)) ↔
(t = a
∧ u =
b ∧ ∃c∃d(x = 〈c, d〉 ∧ (tAc ∧ uBd)))) |
21 | 20 | 2exbii 1583 |
. . . . . . 7
⊢ (∃t∃u∃c∃d(〈a, b〉 = 〈t, u〉 ∧ x = 〈c, d〉 ∧ (tAc ∧ uBd)) ↔
∃t∃u(t = a ∧ u = b ∧ ∃c∃d(x = 〈c, d〉 ∧ (tAc ∧ uBd)))) |
22 | | vex 2862 |
. . . . . . . 8
⊢ a ∈
V |
23 | | vex 2862 |
. . . . . . . 8
⊢ b ∈
V |
24 | | breq1 4642 |
. . . . . . . . . . 11
⊢ (t = a →
(tAc ↔
aAc)) |
25 | 24 | anbi1d 685 |
. . . . . . . . . 10
⊢ (t = a →
((tAc ∧ uBd) ↔
(aAc ∧ uBd))) |
26 | 25 | anbi2d 684 |
. . . . . . . . 9
⊢ (t = a →
((x = 〈c, d〉 ∧ (tAc ∧ uBd)) ↔
(x = 〈c, d〉 ∧ (aAc ∧ uBd)))) |
27 | 26 | 2exbidv 1628 |
. . . . . . . 8
⊢ (t = a →
(∃c∃d(x = 〈c, d〉 ∧ (tAc ∧ uBd)) ↔ ∃c∃d(x = 〈c, d〉 ∧ (aAc ∧ uBd)))) |
28 | | breq1 4642 |
. . . . . . . . . . 11
⊢ (u = b →
(uBd ↔
bBd)) |
29 | 28 | anbi2d 684 |
. . . . . . . . . 10
⊢ (u = b →
((aAc ∧ uBd) ↔
(aAc ∧ bBd))) |
30 | 29 | anbi2d 684 |
. . . . . . . . 9
⊢ (u = b →
((x = 〈c, d〉 ∧ (aAc ∧ uBd)) ↔
(x = 〈c, d〉 ∧ (aAc ∧ bBd)))) |
31 | 30 | 2exbidv 1628 |
. . . . . . . 8
⊢ (u = b →
(∃c∃d(x = 〈c, d〉 ∧ (aAc ∧ uBd)) ↔ ∃c∃d(x = 〈c, d〉 ∧ (aAc ∧ bBd)))) |
32 | 22, 23, 27, 31 | ceqsex2v 2896 |
. . . . . . 7
⊢ (∃t∃u(t = a ∧ u = b ∧ ∃c∃d(x = 〈c, d〉 ∧ (tAc ∧ uBd))) ↔ ∃c∃d(x = 〈c, d〉 ∧ (aAc ∧ bBd))) |
33 | 10, 21, 32 | 3bitri 262 |
. . . . . 6
⊢ (〈a, b〉 PProd (A, B)x ↔ ∃c∃d(x = 〈c, d〉 ∧ (aAc ∧ bBd))) |
34 | 33 | exbii 1582 |
. . . . 5
⊢ (∃x〈a, b〉 PProd (A, B)x ↔ ∃x∃c∃d(x = 〈c, d〉 ∧ (aAc ∧ bBd))) |
35 | | exrot3 1744 |
. . . . 5
⊢ (∃x∃c∃d(x = 〈c, d〉 ∧ (aAc ∧ bBd)) ↔ ∃c∃d∃x(x = 〈c, d〉 ∧ (aAc ∧ bBd))) |
36 | 34, 35 | bitri 240 |
. . . 4
⊢ (∃x〈a, b〉 PProd (A, B)x ↔ ∃c∃d∃x(x = 〈c, d〉 ∧ (aAc ∧ bBd))) |
37 | 8, 9, 36 | 3bitri 262 |
. . 3
⊢ (adom PProd (A, B)b ↔ ∃c∃d∃x(x = 〈c, d〉 ∧ (aAc ∧ bBd))) |
38 | | eldm 4898 |
. . . . 5
⊢ (a ∈ dom A ↔ ∃c aAc) |
39 | | eldm 4898 |
. . . . 5
⊢ (b ∈ dom B ↔ ∃d bBd) |
40 | 38, 39 | anbi12i 678 |
. . . 4
⊢ ((a ∈ dom A ∧ b ∈ dom B) ↔ (∃c aAc ∧ ∃d bBd)) |
41 | | brxp 4812 |
. . . 4
⊢ (a(dom A ×
dom B)b
↔ (a ∈ dom A ∧ b ∈ dom B)) |
42 | | eeanv 1913 |
. . . 4
⊢ (∃c∃d(aAc ∧ bBd) ↔ (∃c aAc ∧ ∃d bBd)) |
43 | 40, 41, 42 | 3bitr4i 268 |
. . 3
⊢ (a(dom A ×
dom B)b
↔ ∃c∃d(aAc ∧ bBd)) |
44 | 7, 37, 43 | 3bitr4i 268 |
. 2
⊢ (adom PProd (A, B)b ↔ a(dom
A × dom B)b) |
45 | 44 | eqbrriv 4851 |
1
⊢ dom PProd (A, B) = (dom A
× dom B) |