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 ⊢ F ∈ J Cn K ∧ A ∈ K → F -1 A ∈ J

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 eqid ⊢ ⋃ K = ⋃ K
3 1 2 iscn2 ⊢ F ∈ J Cn K ↔ J ∈ Top ∧ K ∈ Top ∧ F : ⋃ J ⟶ ⋃ K ∧ ∀ x ∈ K F -1 x ∈ J
4 3 simprbi ⊢ F ∈ J Cn K → F : ⋃ J ⟶ ⋃ K ∧ ∀ x ∈ K F -1 x ∈ J
5 4 simprd ⊢ F ∈ J Cn K → ∀ x ∈ K F -1 x ∈ J
6 imaeq2 ⊢ x = A → F -1 x = F -1 A
7 6 eleq1d ⊢ x = A → F -1 x ∈ J ↔ F -1 A ∈ J
8 7 rspccva ⊢ ∀ x ∈ K F -1 x ∈ J ∧ A ∈ K → F -1 A ∈ J
9 5 8 sylan ⊢ F ∈ J Cn K ∧ A ∈ K → F -1 A ∈ J