Metamath Proof Explorer

Theorem iscncl

Description: A characterization of a continuity function using closed sets. Theorem 1(d) of BourbakiTop1 p. I.9. (Contributed by FL, 19-Nov-2006) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion iscncl ⊢J∈TopOn⁡X∧K∈TopOn⁡Y→F∈JCnK↔F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J

Proof

Step Hyp Ref Expression
1 cnf2 ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F∈JCnK→F:X⟶Y
2 1 3expa ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F∈JCnK→F:X⟶Y
3 cnclima ⊢F∈JCnK∧y∈Clsd⁡K→F-1y∈Clsd⁡J
4 3 ralrimiva ⊢F∈JCnK→∀y∈Clsd⁡KF-1y∈Clsd⁡J
5 4 adantl ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F∈JCnK→∀y∈Clsd⁡KF-1y∈Clsd⁡J
6 2 5 jca ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F∈JCnK→F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J
7 simprl ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J→F:X⟶Y
8 toponuni ⊢J∈TopOn⁡X→X=⋃J
9 8 ad3antrrr ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→X=⋃J
10 simplrl ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→F:X⟶Y
11 fimacnv ⊢F:X⟶Y→F-1Y=X
12 11 eqcomd ⊢F:X⟶Y→X=F-1Y
13 10 12 syl ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→X=F-1Y
14 9 13 eqtr3d ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→⋃J=F-1Y
15 14 difeq1d ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→⋃J∖F-1x=F-1Y∖F-1x
16 ffun ⊢F:X⟶Y→Fun⁡F
17 funcnvcnv ⊢Fun⁡F→Fun⁡F-1-1
18 imadif ⊢Fun⁡F-1-1→F-1Y∖x=F-1Y∖F-1x
19 10 16 17 18 4syl ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→F-1Y∖x=F-1Y∖F-1x
20 15 19 eqtr4d ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→⋃J∖F-1x=F-1Y∖x
21 imaeq2 ⊢y=Y∖x→F-1y=F-1Y∖x
22 21 eleq1d ⊢y=Y∖x→F-1y∈Clsd⁡J↔F-1Y∖x∈Clsd⁡J
23 simplrr ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→∀y∈Clsd⁡KF-1y∈Clsd⁡J
24 toponuni ⊢K∈TopOn⁡Y→Y=⋃K
25 24 ad3antlr ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→Y=⋃K
26 25 difeq1d ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→Y∖x=⋃K∖x
27 topontop ⊢K∈TopOn⁡Y→K∈Top
28 27 ad3antlr ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→K∈Top
29 eqid ⊢⋃K=⋃K
30 29 opncld ⊢K∈Top∧x∈K→⋃K∖x∈Clsd⁡K
31 28 30 sylancom ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→⋃K∖x∈Clsd⁡K
32 26 31 eqeltrd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→Y∖x∈Clsd⁡K
33 22 23 32 rspcdva ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→F-1Y∖x∈Clsd⁡J
34 20 33 eqeltrd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→⋃J∖F-1x∈Clsd⁡J
35 topontop ⊢J∈TopOn⁡X→J∈Top
36 35 ad3antrrr ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→J∈Top
37 cnvimass ⊢F-1x⊆dom⁡F
38 37 10 fssdm ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→F-1x⊆X
39 38 9 sseqtrd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→F-1x⊆⋃J
40 eqid ⊢⋃J=⋃J
41 40 isopn2 ⊢J∈Top∧F-1x⊆⋃J→F-1x∈J↔⋃J∖F-1x∈Clsd⁡J
42 36 39 41 syl2anc ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→F-1x∈J↔⋃J∖F-1x∈Clsd⁡J
43 34 42 mpbird ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J∧x∈K→F-1x∈J
44 43 ralrimiva ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J→∀x∈KF-1x∈J
45 iscn ⊢J∈TopOn⁡X∧K∈TopOn⁡Y→F∈JCnK↔F:X⟶Y∧∀x∈KF-1x∈J
46 45 adantr ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J→F∈JCnK↔F:X⟶Y∧∀x∈KF-1x∈J
47 7 44 46 mpbir2and ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J→F∈JCnK
48 6 47 impbida ⊢J∈TopOn⁡X∧K∈TopOn⁡Y→F∈JCnK↔F:X⟶Y∧∀y∈Clsd⁡KF-1y∈Clsd⁡J