Step | Hyp | Ref
| Expression |
1 | | vex 3434 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
2 | | vex 3434 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
3 | 1, 2 | op1std 7827 |
. . . . . . 7
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (1st ‘𝑣) = 𝑧) |
4 | 3 | csbeq1d 3840 |
. . . . . 6
⊢ (𝑣 = 〈𝑧, 𝑤〉 → ⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 = ⦋𝑧 / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶) |
5 | 1, 2 | op2ndd 7828 |
. . . . . . . 8
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (2nd ‘𝑣) = 𝑤) |
6 | 5 | csbeq1d 3840 |
. . . . . . 7
⊢ (𝑣 = 〈𝑧, 𝑤〉 → ⦋(2nd
‘𝑣) / 𝑦⦌𝐶 = ⦋𝑤 / 𝑦⦌𝐶) |
7 | 6 | csbeq2dv 3843 |
. . . . . 6
⊢ (𝑣 = 〈𝑧, 𝑤〉 → ⦋𝑧 / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
8 | 4, 7 | eqtrd 2779 |
. . . . 5
⊢ (𝑣 = 〈𝑧, 𝑤〉 → ⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
9 | 8 | eleq1d 2824 |
. . . 4
⊢ (𝑣 = 〈𝑧, 𝑤〉 → (⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 ∈ 𝐷 ↔ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
10 | 9 | raliunxp 5745 |
. . 3
⊢
(∀𝑣 ∈
∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⦋(1st ‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 ∈ 𝐷 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷) |
11 | | nfv 1920 |
. . . . . . 7
⊢
Ⅎ𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) |
12 | | nfv 1920 |
. . . . . . 7
⊢
Ⅎ𝑤((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) |
13 | | nfv 1920 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑧 ∈ 𝐴 |
14 | | nfcsb1v 3861 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
15 | 14 | nfcri 2895 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 |
16 | 13, 15 | nfan 1905 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
17 | | nfcsb1v 3861 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 |
18 | 17 | nfeq2 2925 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 |
19 | 16, 18 | nfan 1905 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
20 | | nfv 1920 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
21 | | nfcv 2908 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝑧 |
22 | | nfcsb1v 3861 |
. . . . . . . . . 10
⊢
Ⅎ𝑦⦋𝑤 / 𝑦⦌𝐶 |
23 | 21, 22 | nfcsbw 3863 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 |
24 | 23 | nfeq2 2925 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 |
25 | 20, 24 | nfan 1905 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
26 | | eleq1w 2822 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
28 | | eleq1w 2822 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵)) |
29 | | csbeq1a 3850 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
30 | 29 | eleq2d 2825 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
31 | 28, 30 | sylan9bbr 510 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
32 | 27, 31 | anbi12d 630 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵))) |
33 | | csbeq1a 3850 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → 𝐶 = ⦋𝑤 / 𝑦⦌𝐶) |
34 | | csbeq1a 3850 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ⦋𝑤 / 𝑦⦌𝐶 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
35 | 33, 34 | sylan9eqr 2801 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
36 | 35 | eqeq2d 2750 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = 𝐶 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶)) |
37 | 32, 36 | anbi12d 630 |
. . . . . . 7
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶))) |
38 | 11, 12, 19, 25, 37 | cbvoprab12 7355 |
. . . . . 6
⊢
{〈〈𝑥,
𝑦〉, 𝑣〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {〈〈𝑧, 𝑤〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶)} |
39 | | df-mpo 7273 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑣〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} |
40 | | df-mpo 7273 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴, 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ↦ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) = {〈〈𝑧, 𝑤〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵) ∧ 𝑣 = ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶)} |
41 | 38, 39, 40 | 3eqtr4i 2777 |
. . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ↦ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
42 | | fmpox.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
43 | 8 | mpomptx 7378 |
. . . . 5
⊢ (𝑣 ∈ ∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) ↦ ⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ↦ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶) |
44 | 41, 42, 43 | 3eqtr4i 2777 |
. . . 4
⊢ 𝐹 = (𝑣 ∈ ∪
𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) ↦ ⦋(1st
‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶) |
45 | 44 | fmpt 6978 |
. . 3
⊢
(∀𝑣 ∈
∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⦋(1st ‘𝑣) / 𝑥⦌⦋(2nd
‘𝑣) / 𝑦⦌𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⟶𝐷) |
46 | 10, 45 | bitr3i 276 |
. 2
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⟶𝐷) |
47 | | nfv 1920 |
. . 3
⊢
Ⅎ𝑧∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 |
48 | 17 | nfel1 2924 |
. . . 4
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 |
49 | 14, 48 | nfralw 3151 |
. . 3
⊢
Ⅎ𝑥∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 |
50 | | nfv 1920 |
. . . . 5
⊢
Ⅎ𝑤 𝐶 ∈ 𝐷 |
51 | 22 | nfel1 2924 |
. . . . 5
⊢
Ⅎ𝑦⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 |
52 | 33 | eleq1d 2824 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝐶 ∈ 𝐷 ↔ ⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
53 | 50, 51, 52 | cbvralw 3371 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 𝐶 ∈ 𝐷 ↔ ∀𝑤 ∈ 𝐵 ⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷) |
54 | 34 | eleq1d 2824 |
. . . . 5
⊢ (𝑥 = 𝑧 → (⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 ↔ ⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
55 | 29, 54 | raleqbidv 3334 |
. . . 4
⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐵 ⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷 ↔ ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
56 | 53, 55 | syl5bb 282 |
. . 3
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷)) |
57 | 47, 49, 56 | cbvralw 3371 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ ⦋ 𝑧 / 𝑥⦌𝐵⦋𝑧 / 𝑥⦌⦋𝑤 / 𝑦⦌𝐶 ∈ 𝐷) |
58 | | nfcv 2908 |
. . . 4
⊢
Ⅎ𝑧({𝑥} × 𝐵) |
59 | | nfcv 2908 |
. . . . 5
⊢
Ⅎ𝑥{𝑧} |
60 | 59, 14 | nfxp 5621 |
. . . 4
⊢
Ⅎ𝑥({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) |
61 | | sneq 4576 |
. . . . 5
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
62 | 61, 29 | xpeq12d 5619 |
. . . 4
⊢ (𝑥 = 𝑧 → ({𝑥} × 𝐵) = ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)) |
63 | 58, 60, 62 | cbviun 4970 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = ∪
𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵) |
64 | 63 | feq2i 6588 |
. 2
⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:∪ 𝑧 ∈ 𝐴 ({𝑧} × ⦋𝑧 / 𝑥⦌𝐵)⟶𝐷) |
65 | 46, 57, 64 | 3bitr4i 302 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷) |