Step |
Hyp |
Ref |
Expression |
1 |
|
dfmpo.1 |
⊢ 𝐶 ∈ V |
2 |
|
mpompts |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) |
3 |
1
|
csbex |
⊢ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ V |
4 |
3
|
csbex |
⊢ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ V |
5 |
4
|
dfmpt |
⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) = ∪ 𝑤 ∈ ( 𝐴 × 𝐵 ) { ⟨ 𝑤 , ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ } |
6 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑤 |
7 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 |
8 |
6 7
|
nfop |
⊢ Ⅎ 𝑥 ⟨ 𝑤 , ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ |
9 |
8
|
nfsn |
⊢ Ⅎ 𝑥 { ⟨ 𝑤 , ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ } |
10 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑤 |
11 |
|
nfcv |
⊢ Ⅎ 𝑦 ( 1st ‘ 𝑤 ) |
12 |
|
nfcsb1v |
⊢ Ⅎ 𝑦 ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 |
13 |
11 12
|
nfcsbw |
⊢ Ⅎ 𝑦 ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 |
14 |
10 13
|
nfop |
⊢ Ⅎ 𝑦 ⟨ 𝑤 , ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ |
15 |
14
|
nfsn |
⊢ Ⅎ 𝑦 { ⟨ 𝑤 , ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ } |
16 |
|
nfcv |
⊢ Ⅎ 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ } |
17 |
|
id |
⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) |
18 |
|
csbopeq1a |
⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 = 𝐶 ) |
19 |
17 18
|
opeq12d |
⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑤 , ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ ) |
20 |
19
|
sneqd |
⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → { ⟨ 𝑤 , ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ } ) |
21 |
9 15 16 20
|
iunxpf |
⊢ ∪ 𝑤 ∈ ( 𝐴 × 𝐵 ) { ⟨ 𝑤 , ⦋ ( 1st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ } = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ } |
22 |
2 5 21
|
3eqtri |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ } |