Metamath Proof Explorer


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 ) ∧ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑦𝐾 ( 𝐹𝑦 ) ∈ 𝐽 ) ) )