Step | Hyp | Ref
| Expression |
1 | | vex 2715 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
2 | | vex 2715 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
3 | 1, 2 | op1std 6099 |
. . . . . . 7
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (1st ‘𝑣) = 𝑧) |
4 | 3 | csbeq1d 3038 |
. . . . . 6
⊢ (𝑣 = 〈𝑧, 𝑤〉 → ⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 = ⦋𝑧 / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶) |
5 | 1, 2 | op2ndd 6100 |
. . . . . . . 8
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (2nd ‘𝑣) = 𝑤) |
6 | 5 | csbeq1d 3038 |
. . . . . . 7
⊢ (𝑣 = 〈𝑧, 𝑤〉 → ⦋(2nd
‘𝑣) / 𝑦⦌𝐶 = ⦋𝑤 / 𝑦⦌𝐶) |
7 | 6 | csbeq2dv 3057 |
. . . . . 6
⊢ (𝑣 = 〈𝑧, 𝑤〉 → ⦋𝑧 / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
8 | 4, 7 | eqtrd 2190 |
. . . . 5
⊢ (𝑣 = 〈𝑧, 𝑤〉 → ⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
9 | 8 | eleq1d 2226 |
. . . 4
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 ∈ 𝐷 ↔ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
10 | 9 | raliunxp 4730 |
. . 3
⊢
(∀𝑣 ∈
∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⦋(1st ‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 ∈ 𝐷 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷) |
11 | | nfv 1508 |
. . . . . . 7
⊢
Ⅎ𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) |
12 | | nfv 1508 |
. . . . . . 7
⊢
Ⅎ𝑤((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) |
13 | | nfv 1508 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
14 | | nfcsb1v 3064 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
15 | 14 | nfcri 2293 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 |
16 | 13, 15 | nfan 1545 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
17 | | nfcsb1v 3064 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 |
18 | 17 | nfeq2 2311 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 |
19 | 16, 18 | nfan 1545 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
20 | | nfv 1508 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
21 | | nfcv 2299 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝑧 |
22 | | nfcsb1v 3064 |
. . . . . . . . . 10
⊢
Ⅎ𝑦⦋𝑤 / 𝑦⦌𝐶 |
23 | 21, 22 | nfcsb 3068 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 |
24 | 23 | nfeq2 2311 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 |
25 | 20, 24 | nfan 1545 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
26 | | eleq1 2220 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
27 | 26 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
28 | | eleq1 2220 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵)) |
29 | | csbeq1a 3040 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
30 | 29 | eleq2d 2227 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
31 | 28, 30 | sylan9bbr 459 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
32 | 27, 31 | anbi12d 465 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵))) |
33 | | csbeq1a 3040 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → 𝐶 = ⦋𝑤 / 𝑦⦌𝐶) |
34 | | csbeq1a 3040 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ⦋𝑤 / 𝑦⦌𝐶 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
35 | 33, 34 | sylan9eqr 2212 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
36 | 35 | eqeq2d 2169 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = 𝐶 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶)) |
37 | 32, 36 | anbi12d 465 |
. . . . . . 7
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶))) |
38 | 11, 12, 19, 25, 37 | cbvoprab12 5898 |
. . . . . 6
⊢
{〈〈𝑥,
𝑦〉, 𝑣〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {〈〈𝑧, 𝑤〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶)} |
39 | | df-mpo 5832 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑣〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} |
40 | | df-mpo 5832 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴, 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ↦ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) = {〈〈𝑧, 𝑤〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶)} |
41 | 38, 39, 40 | 3eqtr4i 2188 |
. . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ↦ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
42 | | fmpox.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
43 | 8 | mpomptx 5915 |
. . . . 5
⊢ (𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) ↦ ⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ↦ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
44 | 41, 42, 43 | 3eqtr4i 2188 |
. . . 4
⊢ 𝐹 = (𝑣 ∈ ∪
𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) ↦ ⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶) |
45 | 44 | fmpt 5620 |
. . 3
⊢
(∀𝑣 ∈
∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⦋(1st ‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⟶𝐷) |
46 | 10, 45 | bitr3i 185 |
. 2
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⟶𝐷) |
47 | | nfv 1508 |
. . 3
⊢
Ⅎ𝑧∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 |
48 | 17 | nfel1 2310 |
. . . 4
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 |
49 | 14, 48 | nfralxy 2495 |
. . 3
⊢
Ⅎ𝑥∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 |
50 | | nfv 1508 |
. . . . 5
⊢
Ⅎ𝑤 𝐶 ∈ 𝐷 |
51 | 22 | nfel1 2310 |
. . . . 5
⊢
Ⅎ𝑦⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 |
52 | 33 | eleq1d 2226 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝐶 ∈ 𝐷 ↔ ⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
53 | 50, 51, 52 | cbvral 2676 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 𝐶 ∈ 𝐷 ↔ ∀𝑤 ∈ 𝐵 ⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷) |
54 | 34 | eleq1d 2226 |
. . . . 5
⊢ (𝑥 = 𝑧 → (⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 ↔ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
55 | 29, 54 | raleqbidv 2664 |
. . . 4
⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐵 ⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 ↔ ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
56 | 53, 55 | syl5bb 191 |
. . 3
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
57 | 47, 49, 56 | cbvral 2676 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷) |
58 | | nfcv 2299 |
. . . 4
⊢
Ⅎ𝑧({𝑥} × 𝐵) |
59 | | nfcv 2299 |
. . . . 5
⊢
Ⅎ𝑥{𝑧} |
60 | 59, 14 | nfxp 4616 |
. . . 4
⊢
Ⅎ𝑥({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) |
61 | | sneq 3572 |
. . . . 5
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
62 | 61, 29 | xpeq12d 4614 |
. . . 4
⊢ (𝑥 = 𝑧 → ({𝑥} × 𝐵) = ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) |
63 | 58, 60, 62 | cbviun 3888 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = ∪
𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) |
64 | 63 | feq2i 5316 |
. 2
⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⟶𝐷) |
65 | 46, 57, 64 | 3bitr4i 211 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷) |