Step | Hyp | Ref
| Expression |
1 | | vex 2554 |
. . . . . 6
⊢ u ∈
V |
2 | | vex 2554 |
. . . . . 6
⊢ v ∈
V |
3 | 1, 2 | op1std 5717 |
. . . . 5
⊢ (z = 〈u,
v〉 → (1st
‘z) = u) |
4 | 3 | csbeq1d 2852 |
. . . 4
⊢ (z = 〈u,
v〉 →
⦋(1st ‘z) /
x⦌⦋(2nd
‘z) / y⦌𝐶 = ⦋u / x⦌⦋(2nd
‘z) / y⦌𝐶) |
5 | 1, 2 | op2ndd 5718 |
. . . . . 6
⊢ (z = 〈u,
v〉 → (2nd
‘z) = v) |
6 | 5 | csbeq1d 2852 |
. . . . 5
⊢ (z = 〈u,
v〉 →
⦋(2nd ‘z) /
y⦌𝐶 = ⦋v / y⦌𝐶) |
7 | 6 | csbeq2dv 2869 |
. . . 4
⊢ (z = 〈u,
v〉 → ⦋u / x⦌⦋(2nd
‘z) / y⦌𝐶 = ⦋u / x⦌⦋v / y⦌𝐶) |
8 | 4, 7 | eqtrd 2069 |
. . 3
⊢ (z = 〈u,
v〉 →
⦋(1st ‘z) /
x⦌⦋(2nd
‘z) / y⦌𝐶 = ⦋u / x⦌⦋v / y⦌𝐶) |
9 | 8 | mpt2mptx 5537 |
. 2
⊢ (z ∈ ∪ u ∈ A ({u} × ⦋u / x⦌B) ↦ ⦋(1st
‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶) = (u
∈ A,
v ∈
⦋u / x⦌B ↦ ⦋u / x⦌⦋v / y⦌𝐶) |
10 | | nfcv 2175 |
. . . 4
⊢
Ⅎu({x} × B) |
11 | | nfcv 2175 |
. . . . 5
⊢
Ⅎx{u} |
12 | | nfcsb1v 2876 |
. . . . 5
⊢
Ⅎx⦋u / x⦌B |
13 | 11, 12 | nfxp 4314 |
. . . 4
⊢
Ⅎx({u} × ⦋u / x⦌B) |
14 | | sneq 3378 |
. . . . 5
⊢ (x = u →
{x} = {u}) |
15 | | csbeq1a 2854 |
. . . . 5
⊢ (x = u →
B = ⦋u / x⦌B) |
16 | 14, 15 | xpeq12d 4313 |
. . . 4
⊢ (x = u →
({x} × B) = ({u}
× ⦋u / x⦌B)) |
17 | 10, 13, 16 | cbviun 3685 |
. . 3
⊢ ∪ x ∈ A ({x} × B) =
∪ u ∈ A ({u} × ⦋u / x⦌B) |
18 | | mpteq1 3832 |
. . 3
⊢ (∪ x ∈ A ({x} × B) =
∪ u ∈ A ({u} × ⦋u / x⦌B) → (z
∈ ∪
x ∈
A ({x}
× B) ↦
⦋(1st ‘z) /
x⦌⦋(2nd
‘z) / y⦌𝐶) = (z
∈ ∪
u ∈
A ({u}
× ⦋u / x⦌B) ↦ ⦋(1st
‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶)) |
19 | 17, 18 | ax-mp 7 |
. 2
⊢ (z ∈ ∪ x ∈ A ({x} × B)
↦ ⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶) = (z
∈ ∪
u ∈
A ({u}
× ⦋u / x⦌B) ↦ ⦋(1st
‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶) |
20 | | nfcv 2175 |
. . 3
⊢
ℲuB |
21 | | nfcv 2175 |
. . 3
⊢
Ⅎu𝐶 |
22 | | nfcv 2175 |
. . 3
⊢
Ⅎv𝐶 |
23 | | nfcsb1v 2876 |
. . 3
⊢
Ⅎx⦋u / x⦌⦋v / y⦌𝐶 |
24 | | nfcv 2175 |
. . . 4
⊢
Ⅎyu |
25 | | nfcsb1v 2876 |
. . . 4
⊢
Ⅎy⦋v / y⦌𝐶 |
26 | 24, 25 | nfcsb 2878 |
. . 3
⊢
Ⅎy⦋u / x⦌⦋v / y⦌𝐶 |
27 | | csbeq1a 2854 |
. . . 4
⊢ (y = v →
𝐶 = ⦋v / y⦌𝐶) |
28 | | csbeq1a 2854 |
. . . 4
⊢ (x = u →
⦋v / y⦌𝐶 = ⦋u / x⦌⦋v / y⦌𝐶) |
29 | 27, 28 | sylan9eqr 2091 |
. . 3
⊢
((x = u ∧ y = v) →
𝐶 = ⦋u / x⦌⦋v / y⦌𝐶) |
30 | 20, 12, 21, 22, 23, 26, 15, 29 | cbvmpt2x 5524 |
. 2
⊢ (x ∈ A, y ∈ B ↦
𝐶) = (u ∈ A, v ∈ ⦋u / x⦌B ↦ ⦋u / x⦌⦋v / y⦌𝐶) |
31 | 9, 19, 30 | 3eqtr4ri 2068 |
1
⊢ (x ∈ A, y ∈ B ↦
𝐶) = (z ∈ ∪ x ∈ A ({x} × B)
↦ ⦋(1st ‘z) / x⦌⦋(2nd
‘z) / y⦌𝐶) |