This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfex

Description: The class of continuous functions between two topologies is a set. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Assertion cnfex ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn 𝐾 ) ∈ V )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 1 jctr ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Top ∧ ∪ 𝐽 = ∪ 𝐽 ) )
3 istopon ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ↔ ( 𝐽 ∈ Top ∧ ∪ 𝐽 = ∪ 𝐽 ) )
4 2 3 sylibr ⊢ ( 𝐽 ∈ Top → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
5 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
6 5 jctr ⊢ ( 𝐾 ∈ Top → ( 𝐾 ∈ Top ∧ ∪ 𝐾 = ∪ 𝐾 ) )
7 istopon ⊢ ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ↔ ( 𝐾 ∈ Top ∧ ∪ 𝐾 = ∪ 𝐾 ) )
8 6 7 sylibr ⊢ ( 𝐾 ∈ Top → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
9 cnfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → ( 𝐽 Cn 𝐾 ) = { 𝑓 ∈ ( ∪ 𝐾 ↑m ∪ 𝐽 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } )
10 4 8 9 syl2an ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn 𝐾 ) = { 𝑓 ∈ ( ∪ 𝐾 ↑m ∪ 𝐽 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } )
11 uniexg ⊢ ( 𝐾 ∈ Top → ∪ 𝐾 ∈ V )
12 uniexg ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
13 mapvalg ⊢ ( ( ∪ 𝐾 ∈ V ∧ ∪ 𝐽 ∈ V ) → ( ∪ 𝐾 ↑m ∪ 𝐽 ) = { 𝑓 ∣ 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 } )
14 11 12 13 syl2anr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( ∪ 𝐾 ↑m ∪ 𝐽 ) = { 𝑓 ∣ 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 } )
15 mapex ⊢ ( ( ∪ 𝐽 ∈ V ∧ ∪ 𝐾 ∈ V ) → { 𝑓 ∣ 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 } ∈ V )
16 12 11 15 syl2an ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → { 𝑓 ∣ 𝑓 : ∪ 𝐽 ⟶ ∪ 𝐾 } ∈ V )
17 14 16 eqeltrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( ∪ 𝐾 ↑m ∪ 𝐽 ) ∈ V )
18 rabexg ⊢ ( ( ∪ 𝐾 ↑m ∪ 𝐽 ) ∈ V → { 𝑓 ∈ ( ∪ 𝐾 ↑m ∪ 𝐽 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } ∈ V )
19 17 18 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → { 𝑓 ∈ ( ∪ 𝐾 ↑m ∪ 𝐽 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } ∈ V )
20 10 19 eqeltrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn 𝐾 ) ∈ V )