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 )