Step |
Hyp |
Ref |
Expression |
1 |
|
refsum2cn.1 |
⊢ Ⅎ 𝑥 𝐹 |
2 |
|
refsum2cn.2 |
⊢ Ⅎ 𝑥 𝐺 |
3 |
|
refsum2cn.3 |
⊢ Ⅎ 𝑥 𝜑 |
4 |
|
refsum2cn.4 |
⊢ 𝐾 = ( topGen ‘ ran (,) ) |
5 |
|
refsum2cn.5 |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
6 |
|
refsum2cn.6 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |
7 |
|
refsum2cn.7 |
⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) ) |
8 |
|
nfcv |
⊢ Ⅎ 𝑥 { 1 , 2 } |
9 |
|
nfv |
⊢ Ⅎ 𝑥 𝑘 = 1 |
10 |
9 1 2
|
nfif |
⊢ Ⅎ 𝑥 if ( 𝑘 = 1 , 𝐹 , 𝐺 ) |
11 |
8 10
|
nfmpt |
⊢ Ⅎ 𝑥 ( 𝑘 ∈ { 1 , 2 } ↦ if ( 𝑘 = 1 , 𝐹 , 𝐺 ) ) |
12 |
|
eqid |
⊢ ( 𝑘 ∈ { 1 , 2 } ↦ if ( 𝑘 = 1 , 𝐹 , 𝐺 ) ) = ( 𝑘 ∈ { 1 , 2 } ↦ if ( 𝑘 = 1 , 𝐹 , 𝐺 ) ) |
13 |
11 1 2 3 12 4 5 6 7
|
refsum2cnlem1 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐾 ) ) |