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 ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ Clsd ⁡ K F -1 y ∈ Clsd ⁡ J

Proof

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