Step | Hyp | Ref
| Expression |
1 | | vex 2863 |
. . . . . . 7
⊢ c ∈
V |
2 | | vex 2863 |
. . . . . . 7
⊢ d ∈
V |
3 | 1, 2 | opex 4589 |
. . . . . 6
⊢ ⟨c, d⟩ ∈ V |
4 | 3 | isseti 2866 |
. . . . 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 4641 |
. . . 4
⊢ (adom PProd (A, B)b ↔ ⟨a, b⟩ ∈ dom PProd (A, B)) |
9 | | eldm 4899 |
. . . 4
⊢ (⟨a, b⟩ ∈ dom PProd (A, B) ↔
∃x⟨a, b⟩ PProd (A, B)x) |
10 | | brpprod 5840 |
. . . . . . 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 4603 |
. . . . . . . . . . . . 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 2863 |
. . . . . . . 8
⊢ a ∈
V |
23 | | vex 2863 |
. . . . . . . 8
⊢ b ∈
V |
24 | | breq1 4643 |
. . . . . . . . . . 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 4643 |
. . . . . . . . . . 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 2897 |
. . . . . . 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 4899 |
. . . . 5
⊢ (a ∈ dom A ↔ ∃c aAc) |
39 | | eldm 4899 |
. . . . 5
⊢ (b ∈ dom B ↔ ∃d bBd) |
40 | 38, 39 | anbi12i 678 |
. . . 4
⊢ ((a ∈ dom A ∧ b ∈ dom B) ↔ (∃c aAc ∧ ∃d bBd)) |
41 | | brxp 4813 |
. . . 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 4852 |
1
⊢ dom PProd (A, B) = (dom A
× dom B) |