Step |
Hyp |
Ref |
Expression |
1 |
|
cnmpt21.j |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
2 |
|
cnmpt21.k |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
3 |
|
cnmpt21.a |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) |
4 |
|
cnmpt21f.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐿 Cn 𝑀 ) ) |
5 |
|
cntop1 |
⊢ ( 𝐹 ∈ ( 𝐿 Cn 𝑀 ) → 𝐿 ∈ Top ) |
6 |
4 5
|
syl |
⊢ ( 𝜑 → 𝐿 ∈ Top ) |
7 |
|
toptopon2 |
⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ) |
8 |
6 7
|
sylib |
⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ) |
9 |
|
eqid |
⊢ ∪ 𝐿 = ∪ 𝐿 |
10 |
|
eqid |
⊢ ∪ 𝑀 = ∪ 𝑀 |
11 |
9 10
|
cnf |
⊢ ( 𝐹 ∈ ( 𝐿 Cn 𝑀 ) → 𝐹 : ∪ 𝐿 ⟶ ∪ 𝑀 ) |
12 |
4 11
|
syl |
⊢ ( 𝜑 → 𝐹 : ∪ 𝐿 ⟶ ∪ 𝑀 ) |
13 |
12
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ∪ 𝐿 ↦ ( 𝐹 ‘ 𝑧 ) ) ) |
14 |
13 4
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝐿 ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐿 Cn 𝑀 ) ) |
15 |
|
fveq2 |
⊢ ( 𝑧 = 𝐴 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) ) |
16 |
1 2 3 8 14 15
|
cnmpt21 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) ) |