# 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 syl5bb ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ { 𝑓 ∈ ( 𝑌m 𝑋 ) ∣ ∀ 𝑦𝐾 ( 𝑓𝑦 ) ∈ 𝐽 } ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑦𝐾 ( 𝐹𝑦 ) ∈ 𝐽 ) ) )
14 2 13 bitrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑦𝐾 ( 𝐹𝑦 ) ∈ 𝐽 ) ) )