Metamath Proof Explorer

Theorem iscnp3

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". (Contributed by NM, 15-May-2007)

Ref Expression
Assertion iscnp3 ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧P∈X→F∈JCnPK⁡P↔F:X⟶Y∧∀y∈KF⁡P∈y→∃x∈JP∈x∧x⊆F-1y

Proof

Step Hyp Ref Expression
1 iscnp ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧P∈X→F∈JCnPK⁡P↔F:X⟶Y∧∀y∈KF⁡P∈y→∃x∈JP∈x∧Fx⊆y
2 ffun ⊢F:X⟶Y→Fun⁡F
3 2 ad2antlr ⊢J∈TopOn⁡X∧F:X⟶Y∧x∈J→Fun⁡F
4 toponss ⊢J∈TopOn⁡X∧x∈J→x⊆X
5 4 adantlr ⊢J∈TopOn⁡X∧F:X⟶Y∧x∈J→x⊆X
6 fdm ⊢F:X⟶Y→dom⁡F=X
7 6 ad2antlr ⊢J∈TopOn⁡X∧F:X⟶Y∧x∈J→dom⁡F=X
8 5 7 sseqtrrd ⊢J∈TopOn⁡X∧F:X⟶Y∧x∈J→x⊆dom⁡F
9 funimass3 ⊢Fun⁡F∧x⊆dom⁡F→Fx⊆y↔x⊆F-1y
10 3 8 9 syl2anc ⊢J∈TopOn⁡X∧F:X⟶Y∧x∈J→Fx⊆y↔x⊆F-1y
11 10 anbi2d ⊢J∈TopOn⁡X∧F:X⟶Y∧x∈J→P∈x∧Fx⊆y↔P∈x∧x⊆F-1y
12 11 rexbidva ⊢J∈TopOn⁡X∧F:X⟶Y→∃x∈JP∈x∧Fx⊆y↔∃x∈JP∈x∧x⊆F-1y
13 12 imbi2d ⊢J∈TopOn⁡X∧F:X⟶Y→F⁡P∈y→∃x∈JP∈x∧Fx⊆y↔F⁡P∈y→∃x∈JP∈x∧x⊆F-1y
14 13 ralbidv ⊢J∈TopOn⁡X∧F:X⟶Y→∀y∈KF⁡P∈y→∃x∈JP∈x∧Fx⊆y↔∀y∈KF⁡P∈y→∃x∈JP∈x∧x⊆F-1y
15 14 pm5.32da ⊢J∈TopOn⁡X→F:X⟶Y∧∀y∈KF⁡P∈y→∃x∈JP∈x∧Fx⊆y↔F:X⟶Y∧∀y∈KF⁡P∈y→∃x∈JP∈x∧x⊆F-1y
16 15 3ad2ant1 ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧P∈X→F:X⟶Y∧∀y∈KF⁡P∈y→∃x∈JP∈x∧Fx⊆y↔F:X⟶Y∧∀y∈KF⁡P∈y→∃x∈JP∈x∧x⊆F-1y
17 1 16 bitrd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧P∈X→F∈JCnPK⁡P↔F:X⟶Y∧∀y∈KF⁡P∈y→∃x∈JP∈x∧x⊆F-1y