Step | Hyp | Ref
| Expression |
1 | | xpassen.1 |
. . . 4
⊢ 𝐴 ∈ V |
2 | | xpassen.2 |
. . . 4
⊢ 𝐵 ∈ V |
3 | 1, 2 | xpex 4741 |
. . 3
⊢ (𝐴 × 𝐵) ∈ V |
4 | | xpassen.3 |
. . 3
⊢ 𝐶 ∈ V |
5 | 3, 4 | xpex 4741 |
. 2
⊢ ((𝐴 × 𝐵) × 𝐶) ∈ V |
6 | 2, 4 | xpex 4741 |
. . 3
⊢ (𝐵 × 𝐶) ∈ V |
7 | 1, 6 | xpex 4741 |
. 2
⊢ (𝐴 × (𝐵 × 𝐶)) ∈ V |
8 | | vex 2740 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
9 | 8 | snex 4185 |
. . . . . . . . 9
⊢ {𝑥} ∈ V |
10 | 9 | dmex 4893 |
. . . . . . . 8
⊢ dom
{𝑥} ∈
V |
11 | 10 | uniex 4437 |
. . . . . . 7
⊢ ∪ dom {𝑥} ∈ V |
12 | 11 | snex 4185 |
. . . . . 6
⊢ {∪ dom {𝑥}} ∈ V |
13 | 12 | dmex 4893 |
. . . . 5
⊢ dom
{∪ dom {𝑥}} ∈ V |
14 | 13 | uniex 4437 |
. . . 4
⊢ ∪ dom {∪ dom {𝑥}} ∈ V |
15 | 12 | rnex 4894 |
. . . . . 6
⊢ ran
{∪ dom {𝑥}} ∈ V |
16 | 15 | uniex 4437 |
. . . . 5
⊢ ∪ ran {∪ dom {𝑥}} ∈ V |
17 | 9 | rnex 4894 |
. . . . . 6
⊢ ran
{𝑥} ∈
V |
18 | 17 | uniex 4437 |
. . . . 5
⊢ ∪ ran {𝑥} ∈ V |
19 | 16, 18 | opex 4229 |
. . . 4
⊢
⟨∪ ran {∪ dom
{𝑥}}, ∪ ran {𝑥}⟩ ∈ V |
20 | 14, 19 | opex 4229 |
. . 3
⊢
⟨∪ dom {∪ dom
{𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪
ran {𝑥}⟩⟩ ∈
V |
21 | 20 | a1i 9 |
. 2
⊢ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) → ⟨∪
dom {∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩ ∈
V) |
22 | | vex 2740 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
23 | 22 | snex 4185 |
. . . . . . 7
⊢ {𝑦} ∈ V |
24 | 23 | dmex 4893 |
. . . . . 6
⊢ dom
{𝑦} ∈
V |
25 | 24 | uniex 4437 |
. . . . 5
⊢ ∪ dom {𝑦} ∈ V |
26 | 23 | rnex 4894 |
. . . . . . . . 9
⊢ ran
{𝑦} ∈
V |
27 | 26 | uniex 4437 |
. . . . . . . 8
⊢ ∪ ran {𝑦} ∈ V |
28 | 27 | snex 4185 |
. . . . . . 7
⊢ {∪ ran {𝑦}} ∈ V |
29 | 28 | dmex 4893 |
. . . . . 6
⊢ dom
{∪ ran {𝑦}} ∈ V |
30 | 29 | uniex 4437 |
. . . . 5
⊢ ∪ dom {∪ ran {𝑦}} ∈ V |
31 | 25, 30 | opex 4229 |
. . . 4
⊢
⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩ ∈ V |
32 | 28 | rnex 4894 |
. . . . 5
⊢ ran
{∪ ran {𝑦}} ∈ V |
33 | 32 | uniex 4437 |
. . . 4
⊢ ∪ ran {∪ ran {𝑦}} ∈ V |
34 | 31, 33 | opex 4229 |
. . 3
⊢
⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran
{∪ ran {𝑦}}⟩ ∈ V |
35 | 34 | a1i 9 |
. 2
⊢ (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) → ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran
{∪ ran {𝑦}}⟩ ∈ V) |
36 | | sneq 3603 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → {𝑥} = {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}) |
37 | 36 | dmeqd 4829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → dom {𝑥} = dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}) |
38 | 37 | unieqd 3820 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ∪
dom {𝑥} = ∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}) |
39 | 38 | sneqd 3605 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → {∪
dom {𝑥}} = {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}}) |
40 | 39 | dmeqd 4829 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → dom {∪ dom {𝑥}} = dom {∪ dom
{⟨⟨𝑧, 𝑤⟩, 𝑣⟩}}) |
41 | 40 | unieqd 3820 |
. . . . . . . . . . . 12
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ∪
dom {∪ dom {𝑥}} = ∪ dom {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}}) |
42 | | vex 2740 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
43 | | vex 2740 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑤 ∈ V |
44 | 42, 43 | opex 4229 |
. . . . . . . . . . . . . . . . 17
⊢
⟨𝑧, 𝑤⟩ ∈ V |
45 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ V |
46 | 44, 45 | op1sta 5110 |
. . . . . . . . . . . . . . . 16
⊢ ∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩} = ⟨𝑧, 𝑤⟩ |
47 | 46 | sneqi 3604 |
. . . . . . . . . . . . . . 15
⊢ {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = {⟨𝑧, 𝑤⟩} |
48 | 47 | dmeqi 4828 |
. . . . . . . . . . . . . 14
⊢ dom
{∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = dom {⟨𝑧, 𝑤⟩} |
49 | 48 | unieqi 3819 |
. . . . . . . . . . . . 13
⊢ ∪ dom {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = ∪ dom
{⟨𝑧, 𝑤⟩} |
50 | 42, 43 | op1sta 5110 |
. . . . . . . . . . . . 13
⊢ ∪ dom {⟨𝑧, 𝑤⟩} = 𝑧 |
51 | 49, 50 | eqtri 2198 |
. . . . . . . . . . . 12
⊢ ∪ dom {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = 𝑧 |
52 | 41, 51 | eqtr2di 2227 |
. . . . . . . . . . 11
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑧 = ∪ dom {∪ dom {𝑥}}) |
53 | 39 | rneqd 4856 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ran {∪ dom {𝑥}} = ran {∪ dom
{⟨⟨𝑧, 𝑤⟩, 𝑣⟩}}) |
54 | 53 | unieqd 3820 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ∪
ran {∪ dom {𝑥}} = ∪ ran {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}}) |
55 | 47 | rneqi 4855 |
. . . . . . . . . . . . . . 15
⊢ ran
{∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = ran {⟨𝑧, 𝑤⟩} |
56 | 55 | unieqi 3819 |
. . . . . . . . . . . . . 14
⊢ ∪ ran {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = ∪ ran
{⟨𝑧, 𝑤⟩} |
57 | 42, 43 | op2nda 5113 |
. . . . . . . . . . . . . 14
⊢ ∪ ran {⟨𝑧, 𝑤⟩} = 𝑤 |
58 | 56, 57 | eqtri 2198 |
. . . . . . . . . . . . 13
⊢ ∪ ran {∪ dom {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}} = 𝑤 |
59 | 54, 58 | eqtr2di 2227 |
. . . . . . . . . . . 12
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑤 = ∪ ran {∪ dom {𝑥}}) |
60 | 36 | rneqd 4856 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ran {𝑥} = ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}) |
61 | 60 | unieqd 3820 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ∪
ran {𝑥} = ∪ ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩}) |
62 | 44, 45 | op2nda 5113 |
. . . . . . . . . . . . 13
⊢ ∪ ran {⟨⟨𝑧, 𝑤⟩, 𝑣⟩} = 𝑣 |
63 | 61, 62 | eqtr2di 2227 |
. . . . . . . . . . . 12
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → 𝑣 = ∪ ran {𝑥}) |
64 | 59, 63 | opeq12d 3786 |
. . . . . . . . . . 11
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ⟨𝑤, 𝑣⟩ = ⟨∪
ran {∪ dom {𝑥}}, ∪ ran {𝑥}⟩) |
65 | 52, 64 | opeq12d 3786 |
. . . . . . . . . 10
⊢ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ → ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ = ⟨∪ dom {∪ dom {𝑥}}, ⟨∪ ran {∪ dom {𝑥}}, ∪
ran {𝑥}⟩⟩) |
66 | | sneq 3603 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → {𝑦} = {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}) |
67 | 66 | dmeqd 4829 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → dom {𝑦} = dom {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}) |
68 | 67 | unieqd 3820 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ∪ dom {𝑦} = ∪ dom
{⟨𝑧, ⟨𝑤, 𝑣⟩⟩}) |
69 | 43, 45 | opex 4229 |
. . . . . . . . . . . . . 14
⊢
⟨𝑤, 𝑣⟩ ∈ V |
70 | 42, 69 | op1sta 5110 |
. . . . . . . . . . . . 13
⊢ ∪ dom {⟨𝑧, ⟨𝑤, 𝑣⟩⟩} = 𝑧 |
71 | 68, 70 | eqtr2di 2227 |
. . . . . . . . . . . 12
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑧 = ∪ dom {𝑦}) |
72 | 66 | rneqd 4856 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ran {𝑦} = ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}) |
73 | 72 | unieqd 3820 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ∪ ran {𝑦} = ∪ ran
{⟨𝑧, ⟨𝑤, 𝑣⟩⟩}) |
74 | 73 | sneqd 3605 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → {∪ ran {𝑦}} = {∪ ran
{⟨𝑧, ⟨𝑤, 𝑣⟩⟩}}) |
75 | 74 | dmeqd 4829 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → dom {∪ ran {𝑦}} = dom {∪ ran
{⟨𝑧, ⟨𝑤, 𝑣⟩⟩}}) |
76 | 75 | unieqd 3820 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ∪ dom {∪ ran {𝑦}} = ∪ dom {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}}) |
77 | 42, 69 | op2nda 5113 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩} = ⟨𝑤, 𝑣⟩ |
78 | 77 | sneqi 3604 |
. . . . . . . . . . . . . . . 16
⊢ {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = {⟨𝑤, 𝑣⟩} |
79 | 78 | dmeqi 4828 |
. . . . . . . . . . . . . . 15
⊢ dom
{∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = dom {⟨𝑤, 𝑣⟩} |
80 | 79 | unieqi 3819 |
. . . . . . . . . . . . . 14
⊢ ∪ dom {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = ∪
dom {⟨𝑤, 𝑣⟩} |
81 | 43, 45 | op1sta 5110 |
. . . . . . . . . . . . . 14
⊢ ∪ dom {⟨𝑤, 𝑣⟩} = 𝑤 |
82 | 80, 81 | eqtri 2198 |
. . . . . . . . . . . . 13
⊢ ∪ dom {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = 𝑤 |
83 | 76, 82 | eqtr2di 2227 |
. . . . . . . . . . . 12
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑤 = ∪ dom {∪ ran {𝑦}}) |
84 | 71, 83 | opeq12d 3786 |
. . . . . . . . . . 11
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ⟨𝑧, 𝑤⟩ = ⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩) |
85 | 74 | rneqd 4856 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ran {∪ ran {𝑦}} = ran {∪ ran
{⟨𝑧, ⟨𝑤, 𝑣⟩⟩}}) |
86 | 85 | unieqd 3820 |
. . . . . . . . . . . 12
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ∪ ran {∪ ran {𝑦}} = ∪ ran {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}}) |
87 | 78 | rneqi 4855 |
. . . . . . . . . . . . . 14
⊢ ran
{∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = ran {⟨𝑤, 𝑣⟩} |
88 | 87 | unieqi 3819 |
. . . . . . . . . . . . 13
⊢ ∪ ran {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = ∪
ran {⟨𝑤, 𝑣⟩} |
89 | 43, 45 | op2nda 5113 |
. . . . . . . . . . . . 13
⊢ ∪ ran {⟨𝑤, 𝑣⟩} = 𝑣 |
90 | 88, 89 | eqtri 2198 |
. . . . . . . . . . . 12
⊢ ∪ ran {∪ ran {⟨𝑧, ⟨𝑤, 𝑣⟩⟩}} = 𝑣 |
91 | 86, 90 | eqtr2di 2227 |
. . . . . . . . . . 11
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → 𝑣 = ∪ ran {∪ ran {𝑦}}) |
92 | 84, 91 | opeq12d 3786 |
. . . . . . . . . 10
⊢ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ → ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ = ⟨⟨∪ dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran
{∪ ran {𝑦}}⟩) |
93 | 65, 92 | eq2tri 2237 |
. . . . . . . . 9
⊢ ((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
94 | | anass 401 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶) ↔ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) |
95 | 93, 94 | anbi12i 460 |
. . . . . . . 8
⊢ (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
96 | | an32 562 |
. . . . . . . 8
⊢ (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ ((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶))) |
97 | | an32 562 |
. . . . . . . 8
⊢ (((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
98 | 95, 96, 97 | 3bitr4i 212 |
. . . . . . 7
⊢ (((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ ((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
99 | 98 | exbii 1605 |
. . . . . 6
⊢
(∃𝑣((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔
∃𝑣((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
100 | | 19.41v 1902 |
. . . . . 6
⊢
(∃𝑣((𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔
(∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩)) |
101 | | 19.41v 1902 |
. . . . . 6
⊢
(∃𝑣((𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ↔ (∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
102 | 99, 100, 101 | 3bitr3i 210 |
. . . . 5
⊢
((∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔
(∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
103 | 102 | 2exbii 1606 |
. . . 4
⊢
(∃𝑧∃𝑤(∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔
∃𝑧∃𝑤(∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
104 | | 19.41vv 1903 |
. . . 4
⊢
(∃𝑧∃𝑤(∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔
(∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩)) |
105 | | 19.41vv 1903 |
. . . 4
⊢
(∃𝑧∃𝑤(∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ↔ (∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
106 | 103, 104,
105 | 3bitr3i 210 |
. . 3
⊢
((∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔
(∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
107 | | elxp 4643 |
. . . . 5
⊢ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶))) |
108 | | excom 1664 |
. . . . 5
⊢
(∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶))) |
109 | | elxp 4643 |
. . . . . . . . 9
⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑧∃𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵))) |
110 | 109 | anbi1i 458 |
. . . . . . . 8
⊢ ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (∃𝑧∃𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) |
111 | | an12 561 |
. . . . . . . 8
⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) |
112 | | 19.41vv 1903 |
. . . . . . . 8
⊢
(∃𝑧∃𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (∃𝑧∃𝑤(𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) |
113 | 110, 111,
112 | 3bitr4i 212 |
. . . . . . 7
⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑧∃𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) |
114 | 113 | 2exbii 1606 |
. . . . . 6
⊢
(∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑣∃𝑢∃𝑧∃𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) |
115 | | exrot4 1691 |
. . . . . 6
⊢
(∃𝑣∃𝑢∃𝑧∃𝑤((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) |
116 | | anass 401 |
. . . . . . . . 9
⊢ (((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))) |
117 | 116 | exbii 1605 |
. . . . . . . 8
⊢
(∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑢(𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))) |
118 | | opeq1 3778 |
. . . . . . . . . . . 12
⊢ (𝑢 = ⟨𝑧, 𝑤⟩ → ⟨𝑢, 𝑣⟩ = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩) |
119 | 118 | eqeq2d 2189 |
. . . . . . . . . . 11
⊢ (𝑢 = ⟨𝑧, 𝑤⟩ → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩)) |
120 | 119 | anbi1d 465 |
. . . . . . . . . 10
⊢ (𝑢 = ⟨𝑧, 𝑤⟩ → ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) |
121 | 120 | anbi2d 464 |
. . . . . . . . 9
⊢ (𝑢 = ⟨𝑧, 𝑤⟩ → (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)))) |
122 | 44, 121 | ceqsexv 2776 |
. . . . . . . 8
⊢
(∃𝑢(𝑢 = ⟨𝑧, 𝑤⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣 ∈ 𝐶))) |
123 | | an12 561 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶))) |
124 | 117, 122,
123 | 3bitri 206 |
. . . . . . 7
⊢
(∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ (𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶))) |
125 | 124 | 3exbii 1607 |
. . . . . 6
⊢
(∃𝑧∃𝑤∃𝑣∃𝑢((𝑢 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶))) |
126 | 114, 115,
125 | 3bitri 206 |
. . . . 5
⊢
(∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ 𝐶)) ↔ ∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶))) |
127 | 107, 108,
126 | 3bitri 206 |
. . . 4
⊢ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶))) |
128 | 127 | anbi1i 458 |
. . 3
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔
(∃𝑧∃𝑤∃𝑣(𝑥 = ⟨⟨𝑧, 𝑤⟩, 𝑣⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 ∈ 𝐶)) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩)) |
129 | | elxp 4643 |
. . . . 5
⊢ (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ↔ ∃𝑧∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶)))) |
130 | | elxp 4643 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (𝐵 × 𝐶) ↔ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) |
131 | 130 | anbi2i 457 |
. . . . . . . . 9
⊢ (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ 𝑢 ∈ (𝐵 × 𝐶)) ↔ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
132 | | anass 401 |
. . . . . . . . 9
⊢ (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ 𝑢 ∈ (𝐵 × 𝐶)) ↔ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶)))) |
133 | | 19.42vv 1911 |
. . . . . . . . . 10
⊢
(∃𝑤∃𝑣((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
134 | | an12 561 |
. . . . . . . . . . . 12
⊢ (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
135 | | anass 401 |
. . . . . . . . . . . . 13
⊢ (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)) ↔ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
136 | 135 | anbi2i 457 |
. . . . . . . . . . . 12
⊢ ((𝑢 = ⟨𝑤, 𝑣⟩ ∧ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))) |
137 | 134, 136 | bitri 184 |
. . . . . . . . . . 11
⊢ (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))) |
138 | 137 | 2exbii 1606 |
. . . . . . . . . 10
⊢
(∃𝑤∃𝑣((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ (𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))) |
139 | 133, 138 | bitr3i 186 |
. . . . . . . . 9
⊢ (((𝑦 = ⟨𝑧, 𝑢⟩ ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))) |
140 | 131, 132,
139 | 3bitr3i 210 |
. . . . . . . 8
⊢ ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))) |
141 | 140 | exbii 1605 |
. . . . . . 7
⊢
(∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑢∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))) |
142 | | exrot3 1690 |
. . . . . . 7
⊢
(∃𝑢∃𝑤∃𝑣(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) ↔ ∃𝑤∃𝑣∃𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))) |
143 | | opeq2 3779 |
. . . . . . . . . . 11
⊢ (𝑢 = ⟨𝑤, 𝑣⟩ → ⟨𝑧, 𝑢⟩ = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩) |
144 | 143 | eqeq2d 2189 |
. . . . . . . . . 10
⊢ (𝑢 = ⟨𝑤, 𝑣⟩ → (𝑦 = ⟨𝑧, 𝑢⟩ ↔ 𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩)) |
145 | 144 | anbi1d 465 |
. . . . . . . . 9
⊢ (𝑢 = ⟨𝑤, 𝑣⟩ → ((𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))))) |
146 | 69, 145 | ceqsexv 2776 |
. . . . . . . 8
⊢
(∃𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) ↔ (𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
147 | 146 | 2exbii 1606 |
. . . . . . 7
⊢
(∃𝑤∃𝑣∃𝑢(𝑢 = ⟨𝑤, 𝑣⟩ ∧ (𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) ↔ ∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
148 | 141, 142,
147 | 3bitri 206 |
. . . . . 6
⊢
(∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
149 | 148 | exbii 1605 |
. . . . 5
⊢
(∃𝑧∃𝑢(𝑦 = ⟨𝑧, 𝑢⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑢 ∈ (𝐵 × 𝐶))) ↔ ∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
150 | 129, 149 | bitri 184 |
. . . 4
⊢ (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ↔ ∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶)))) |
151 | 150 | anbi1i 458 |
. . 3
⊢ ((𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩) ↔ (∃𝑧∃𝑤∃𝑣(𝑦 = ⟨𝑧, ⟨𝑤, 𝑣⟩⟩ ∧ (𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐶))) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
152 | 106, 128,
151 | 3bitr4i 212 |
. 2
⊢ ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 = ⟨∪ dom
{∪ dom {𝑥}}, ⟨∪ ran
{∪ dom {𝑥}}, ∪ ran {𝑥}⟩⟩) ↔ (𝑦 ∈ (𝐴 × (𝐵 × 𝐶)) ∧ 𝑥 = ⟨⟨∪
dom {𝑦}, ∪ dom {∪ ran {𝑦}}⟩, ∪ ran {∪ ran {𝑦}}⟩)) |
153 | 5, 7, 21, 35, 152 | en2i 6769 |
1
⊢ ((𝐴 × 𝐵) × 𝐶) ≈ (𝐴 × (𝐵 × 𝐶)) |