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

Metamath Proof Explorer

Theorem iscn

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 NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion iscn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 cnfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 Cn 𝐾 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } )
2 1 eleq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } ) )
3 cnveq ⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
4 3 imaeq1d ⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ 𝑦 ) = ( ◡ 𝐹 “ 𝑦 ) )
5 4 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
6 5 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 ↔ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
7 6 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } ↔ ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
8 toponmax ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝐾 )
9 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
10 elmapg ⊢ ( ( 𝑌 ∈ 𝐾 ∧ 𝑋 ∈ 𝐽 ) → ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
11 8 9 10 syl2anr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
12 11 anbi1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
13 7 12 bitrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
14 2 13 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )