Theorem iscn2

Description: The predicate "the class F is a continuous function from topology J to topology K ". Definition of continuous function in Munkres p. 102. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	iscn.1	⊢ 𝑋 = ∪ 𝐽
	iscn.2	⊢ 𝑌 = ∪ 𝐾
Assertion	iscn2	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscn.1	⊢ 𝑋 = ∪ 𝐽
2		iscn.2	⊢ 𝑌 = ∪ 𝐾
3		df-cn	⊢ Cn = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 } )
4	3	elmpocl	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )
5	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6	2	toptopon	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
7		iscn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
8	5 6 7	syl2anb	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
9	4 8	biadanii	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )