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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )

Proof

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