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