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 ⊢ J ∈ Top ∧ K ∈ Top → J Cn K ∈ V

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 jctr ⊢ J ∈ Top → J ∈ Top ∧ ⋃ J = ⋃ J
3 istopon ⊢ J ∈ TopOn ⁡ ⋃ J ↔ J ∈ Top ∧ ⋃ J = ⋃ J
4 2 3 sylibr ⊢ J ∈ Top → J ∈ TopOn ⁡ ⋃ J
5 eqid ⊢ ⋃ K = ⋃ K
6 5 jctr ⊢ K ∈ Top → K ∈ Top ∧ ⋃ K = ⋃ K
7 istopon ⊢ K ∈ TopOn ⁡ ⋃ K ↔ K ∈ Top ∧ ⋃ K = ⋃ K
8 6 7 sylibr ⊢ K ∈ Top → K ∈ TopOn ⁡ ⋃ K
9 cnfval ⊢ J ∈ TopOn ⁡ ⋃ J ∧ K ∈ TopOn ⁡ ⋃ K → J Cn K = f ∈ ⋃ K ⋃ J | ∀ y ∈ K f -1 y ∈ J
10 4 8 9 syl2an ⊢ J ∈ Top ∧ K ∈ Top → J Cn K = f ∈ ⋃ K ⋃ J | ∀ y ∈ K f -1 y ∈ J
11 uniexg ⊢ K ∈ Top → ⋃ K ∈ V
12 uniexg ⊢ J ∈ Top → ⋃ J ∈ V
13 mapvalg ⊢ ⋃ K ∈ V ∧ ⋃ J ∈ V → ⋃ K ⋃ J = f | f : ⋃ J ⟶ ⋃ K
14 11 12 13 syl2anr ⊢ J ∈ Top ∧ K ∈ Top → ⋃ K ⋃ J = f | f : ⋃ J ⟶ ⋃ K
15 mapex ⊢ ⋃ J ∈ V ∧ ⋃ K ∈ V → f | f : ⋃ J ⟶ ⋃ K ∈ V
16 12 11 15 syl2an ⊢ J ∈ Top ∧ K ∈ Top → f | f : ⋃ J ⟶ ⋃ K ∈ V
17 14 16 eqeltrd ⊢ J ∈ Top ∧ K ∈ Top → ⋃ K ⋃ J ∈ V
18 rabexg ⊢ ⋃ K ⋃ J ∈ V → f ∈ ⋃ K ⋃ J | ∀ y ∈ K f -1 y ∈ J ∈ V
19 17 18 syl ⊢ J ∈ Top ∧ K ∈ Top → f ∈ ⋃ K ⋃ J | ∀ y ∈ K f -1 y ∈ J ∈ V
20 10 19 eqeltrd ⊢ J ∈ Top ∧ K ∈ Top → J Cn K ∈ V