Step | Hyp | Ref
| Expression |
1 | | vex 2554 |
. . . . . . . 8
⊢ z ∈
V |
2 | | vex 2554 |
. . . . . . . 8
⊢ w ∈
V |
3 | 1, 2 | op1std 5717 |
. . . . . . 7
⊢ (v = 〈z,
w〉 → (1st
‘v) = z) |
4 | 3 | csbeq1d 2852 |
. . . . . 6
⊢ (v = 〈z,
w〉 →
⦋(1st ‘v) /
x⦌⦋(2nd
‘v) / y⦌𝐶 = ⦋z / x⦌⦋(2nd
‘v) / y⦌𝐶) |
5 | 1, 2 | op2ndd 5718 |
. . . . . . . 8
⊢ (v = 〈z,
w〉 → (2nd
‘v) = w) |
6 | 5 | csbeq1d 2852 |
. . . . . . 7
⊢ (v = 〈z,
w〉 →
⦋(2nd ‘v) /
y⦌𝐶 = ⦋w / y⦌𝐶) |
7 | 6 | csbeq2dv 2869 |
. . . . . 6
⊢ (v = 〈z,
w〉 → ⦋z / x⦌⦋(2nd
‘v) / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶) |
8 | 4, 7 | eqtrd 2069 |
. . . . 5
⊢ (v = 〈z,
w〉 →
⦋(1st ‘v) /
x⦌⦋(2nd
‘v) / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶) |
9 | 8 | eleq1d 2103 |
. . . 4
⊢ (v = 〈z,
w〉 →
(⦋(1st ‘v) /
x⦌⦋(2nd
‘v) / y⦌𝐶 ∈ 𝐷 ↔ ⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷)) |
10 | 9 | raliunxp 4420 |
. . 3
⊢ (∀v ∈ ∪ z ∈ A ({z} ×
⦋z / x⦌B)⦋(1st ‘v) / x⦌⦋(2nd
‘v) / y⦌𝐶 ∈ 𝐷 ↔ ∀z ∈ A ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷) |
11 | | nfv 1418 |
. . . . . . 7
⊢
Ⅎz((x ∈ A ∧ y ∈ B) ∧ v = 𝐶) |
12 | | nfv 1418 |
. . . . . . 7
⊢
Ⅎw((x ∈ A ∧ y ∈ B) ∧ v = 𝐶) |
13 | | nfv 1418 |
. . . . . . . . 9
⊢
Ⅎx z ∈ A |
14 | | nfcsb1v 2876 |
. . . . . . . . . 10
⊢
Ⅎx⦋z / x⦌B |
15 | 14 | nfcri 2169 |
. . . . . . . . 9
⊢
Ⅎx w ∈
⦋z / x⦌B |
16 | 13, 15 | nfan 1454 |
. . . . . . . 8
⊢
Ⅎx(z ∈ A ∧ w ∈
⦋z / x⦌B) |
17 | | nfcsb1v 2876 |
. . . . . . . . 9
⊢
Ⅎx⦋z / x⦌⦋w / y⦌𝐶 |
18 | 17 | nfeq2 2186 |
. . . . . . . 8
⊢
Ⅎx v = ⦋z / x⦌⦋w / y⦌𝐶 |
19 | 16, 18 | nfan 1454 |
. . . . . . 7
⊢
Ⅎx((z ∈ A ∧ w ∈
⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶) |
20 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎy(z ∈ A ∧ w ∈
⦋z / x⦌B) |
21 | | nfcv 2175 |
. . . . . . . . . 10
⊢
Ⅎyz |
22 | | nfcsb1v 2876 |
. . . . . . . . . 10
⊢
Ⅎy⦋w / y⦌𝐶 |
23 | 21, 22 | nfcsb 2878 |
. . . . . . . . 9
⊢
Ⅎy⦋z / x⦌⦋w / y⦌𝐶 |
24 | 23 | nfeq2 2186 |
. . . . . . . 8
⊢
Ⅎy v = ⦋z / x⦌⦋w / y⦌𝐶 |
25 | 20, 24 | nfan 1454 |
. . . . . . 7
⊢
Ⅎy((z ∈ A ∧ w ∈
⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶) |
26 | | eleq1 2097 |
. . . . . . . . . 10
⊢ (x = z →
(x ∈
A ↔ z ∈ A)) |
27 | 26 | adantr 261 |
. . . . . . . . 9
⊢
((x = z ∧ y = w) →
(x ∈
A ↔ z ∈ A)) |
28 | | eleq1 2097 |
. . . . . . . . . 10
⊢ (y = w →
(y ∈
B ↔ w ∈ B)) |
29 | | csbeq1a 2854 |
. . . . . . . . . . 11
⊢ (x = z →
B = ⦋z / x⦌B) |
30 | 29 | eleq2d 2104 |
. . . . . . . . . 10
⊢ (x = z →
(w ∈
B ↔ w ∈
⦋z / x⦌B)) |
31 | 28, 30 | sylan9bbr 436 |
. . . . . . . . 9
⊢
((x = z ∧ y = w) →
(y ∈
B ↔ w ∈
⦋z / x⦌B)) |
32 | 27, 31 | anbi12d 442 |
. . . . . . . 8
⊢
((x = z ∧ y = w) →
((x ∈
A ∧
y ∈
B) ↔ (z ∈ A ∧ w ∈
⦋z / x⦌B))) |
33 | | csbeq1a 2854 |
. . . . . . . . . 10
⊢ (y = w →
𝐶 = ⦋w / y⦌𝐶) |
34 | | csbeq1a 2854 |
. . . . . . . . . 10
⊢ (x = z →
⦋w / y⦌𝐶 = ⦋z / x⦌⦋w / y⦌𝐶) |
35 | 33, 34 | sylan9eqr 2091 |
. . . . . . . . 9
⊢
((x = z ∧ y = w) →
𝐶 = ⦋z / x⦌⦋w / y⦌𝐶) |
36 | 35 | eqeq2d 2048 |
. . . . . . . 8
⊢
((x = z ∧ y = w) →
(v = 𝐶 ↔ v = ⦋z / x⦌⦋w / y⦌𝐶)) |
37 | 32, 36 | anbi12d 442 |
. . . . . . 7
⊢
((x = z ∧ y = w) →
(((x ∈
A ∧
y ∈
B) ∧
v = 𝐶) ↔ ((z ∈ A ∧ w ∈
⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶))) |
38 | 11, 12, 19, 25, 37 | cbvoprab12 5520 |
. . . . . 6
⊢
{〈〈x, y〉, v〉
∣ ((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)} = {〈〈z, w〉,
v〉 ∣ ((z ∈ A ∧ w ∈
⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)} |
39 | | df-mpt2 5460 |
. . . . . 6
⊢ (x ∈ A, y ∈ B ↦
𝐶) = {〈〈x, y〉,
v〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ v = 𝐶)} |
40 | | df-mpt2 5460 |
. . . . . 6
⊢ (z ∈ A, w ∈ ⦋z / x⦌B ↦ ⦋z / x⦌⦋w / y⦌𝐶) = {〈〈z, w〉,
v〉 ∣ ((z ∈ A ∧ w ∈
⦋z / x⦌B) ∧ v = ⦋z / x⦌⦋w / y⦌𝐶)} |
41 | 38, 39, 40 | 3eqtr4i 2067 |
. . . . 5
⊢ (x ∈ A, y ∈ B ↦
𝐶) = (z ∈ A, w ∈ ⦋z / x⦌B ↦ ⦋z / x⦌⦋w / y⦌𝐶) |
42 | | fmpt2x.1 |
. . . . 5
⊢ 𝐹 = (x ∈ A, y ∈ B ↦
𝐶) |
43 | 8 | mpt2mptx 5537 |
. . . . 5
⊢ (v ∈ ∪ z ∈ A ({z} × ⦋z / x⦌B) ↦ ⦋(1st
‘v) / x⦌⦋(2nd
‘v) / y⦌𝐶) = (z
∈ A,
w ∈
⦋z / x⦌B ↦ ⦋z / x⦌⦋w / y⦌𝐶) |
44 | 41, 42, 43 | 3eqtr4i 2067 |
. . . 4
⊢ 𝐹 = (v ∈ ∪ z ∈ A ({z} × ⦋z / x⦌B) ↦ ⦋(1st
‘v) / x⦌⦋(2nd
‘v) / y⦌𝐶) |
45 | 44 | fmpt 5262 |
. . 3
⊢ (∀v ∈ ∪ z ∈ A ({z} ×
⦋z / x⦌B)⦋(1st ‘v) / x⦌⦋(2nd
‘v) / y⦌𝐶 ∈ 𝐷 ↔ 𝐹:∪
z ∈
A ({z}
× ⦋z / x⦌B)⟶𝐷) |
46 | 10, 45 | bitr3i 175 |
. 2
⊢ (∀z ∈ A ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷 ↔ 𝐹:∪
z ∈
A ({z}
× ⦋z / x⦌B)⟶𝐷) |
47 | | nfv 1418 |
. . 3
⊢
Ⅎz∀y ∈ B 𝐶 ∈ 𝐷 |
48 | 17 | nfel1 2185 |
. . . 4
⊢
Ⅎx⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷 |
49 | 14, 48 | nfralxy 2354 |
. . 3
⊢
Ⅎx∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷 |
50 | | nfv 1418 |
. . . . 5
⊢
Ⅎw 𝐶 ∈ 𝐷 |
51 | 22 | nfel1 2185 |
. . . . 5
⊢
Ⅎy⦋w / y⦌𝐶 ∈ 𝐷 |
52 | 33 | eleq1d 2103 |
. . . . 5
⊢ (y = w →
(𝐶 ∈ 𝐷 ↔ ⦋w / y⦌𝐶 ∈ 𝐷)) |
53 | 50, 51, 52 | cbvral 2523 |
. . . 4
⊢ (∀y ∈ B 𝐶 ∈ 𝐷 ↔ ∀w ∈ B
⦋w / y⦌𝐶 ∈ 𝐷) |
54 | 34 | eleq1d 2103 |
. . . . 5
⊢ (x = z →
(⦋w / y⦌𝐶 ∈ 𝐷 ↔ ⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷)) |
55 | 29, 54 | raleqbidv 2511 |
. . . 4
⊢ (x = z →
(∀w
∈ B
⦋w / y⦌𝐶 ∈ 𝐷 ↔ ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷)) |
56 | 53, 55 | syl5bb 181 |
. . 3
⊢ (x = z →
(∀y
∈ B 𝐶 ∈ 𝐷 ↔ ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷)) |
57 | 47, 49, 56 | cbvral 2523 |
. 2
⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝐷 ↔ ∀z ∈ A ∀w ∈ ⦋ z / x⦌B⦋z / x⦌⦋w / y⦌𝐶 ∈ 𝐷) |
58 | | nfcv 2175 |
. . . 4
⊢
Ⅎz({x} × B) |
59 | | nfcv 2175 |
. . . . 5
⊢
Ⅎx{z} |
60 | 59, 14 | nfxp 4314 |
. . . 4
⊢
Ⅎx({z} × ⦋z / x⦌B) |
61 | | sneq 3378 |
. . . . 5
⊢ (x = z →
{x} = {z}) |
62 | 61, 29 | xpeq12d 4313 |
. . . 4
⊢ (x = z →
({x} × B) = ({z}
× ⦋z / x⦌B)) |
63 | 58, 60, 62 | cbviun 3685 |
. . 3
⊢ ∪ x ∈ A ({x} × B) =
∪ z ∈ A ({z} × ⦋z / x⦌B) |
64 | 63 | feq2i 4983 |
. 2
⊢ (𝐹:∪ x ∈ A ({x} × B)⟶𝐷 ↔ 𝐹:∪
z ∈
A ({z}
× ⦋z / x⦌B)⟶𝐷) |
65 | 46, 57, 64 | 3bitr4i 201 |
1
⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝐷 ↔ 𝐹:∪
x ∈
A ({x}
× B)⟶𝐷) |