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

Metamath Proof Explorer

Theorem cnima

Description: An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006)

Ref Expression
Assertion cnima ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
3 1 2 iscn2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
4 3 simprbi ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
5 4 simprd ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
6 imaeq2 ⊢ ( 𝑥 = 𝐴 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝐴 ) )
7 6 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 ) )
8 7 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ∧ 𝐴 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 )
9 5 8 sylan ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐽 )