Metamath Proof Explorer

Theorem seppcld

Description: If two sets are precisely separated by a continuous function, then they are closed. An alternate proof involves II e. Fre . (Contributed by Zhi Wang, 9-Sep-2024)

Ref Expression
Hypothesis seppsepf.1 ⊢ φ → ∃ f ∈ J Cn II S = f -1 0 ∧ T = f -1 1
Assertion seppcld ⊢ φ → S ∈ Clsd ⁡ J ∧ T ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 seppsepf.1 ⊢ φ → ∃ f ∈ J Cn II S = f -1 0 ∧ T = f -1 1
2 simprl ⊢ f ∈ J Cn II ∧ S = f -1 0 ∧ T = f -1 1 → S = f -1 0
3 simpl ⊢ f ∈ J Cn II ∧ S = f -1 0 ∧ T = f -1 1 → f ∈ J Cn II
4 0xr ⊢ 0 ∈ ℝ *
5 iccid ⊢ 0 ∈ ℝ * → 0 0 = 0
6 4 5 ax-mp ⊢ 0 0 = 0
7 0le0 ⊢ 0 ≤ 0
8 0le1 ⊢ 0 ≤ 1
9 icccldii ⊢ 0 ≤ 0 ∧ 0 ≤ 1 → 0 0 ∈ Clsd ⁡ II
10 7 8 9 mp2an ⊢ 0 0 ∈ Clsd ⁡ II
11 6 10 eqeltrri ⊢ 0 ∈ Clsd ⁡ II
12 cnclima ⊢ f ∈ J Cn II ∧ 0 ∈ Clsd ⁡ II → f -1 0 ∈ Clsd ⁡ J
13 3 11 12 sylancl ⊢ f ∈ J Cn II ∧ S = f -1 0 ∧ T = f -1 1 → f -1 0 ∈ Clsd ⁡ J
14 2 13 eqeltrd ⊢ f ∈ J Cn II ∧ S = f -1 0 ∧ T = f -1 1 → S ∈ Clsd ⁡ J
15 simprr ⊢ f ∈ J Cn II ∧ S = f -1 0 ∧ T = f -1 1 → T = f -1 1
16 1xr ⊢ 1 ∈ ℝ *
17 iccid ⊢ 1 ∈ ℝ * → 1 1 = 1
18 16 17 ax-mp ⊢ 1 1 = 1
19 1le1 ⊢ 1 ≤ 1
20 icccldii ⊢ 0 ≤ 1 ∧ 1 ≤ 1 → 1 1 ∈ Clsd ⁡ II
21 8 19 20 mp2an ⊢ 1 1 ∈ Clsd ⁡ II
22 18 21 eqeltrri ⊢ 1 ∈ Clsd ⁡ II
23 cnclima ⊢ f ∈ J Cn II ∧ 1 ∈ Clsd ⁡ II → f -1 1 ∈ Clsd ⁡ J
24 3 22 23 sylancl ⊢ f ∈ J Cn II ∧ S = f -1 0 ∧ T = f -1 1 → f -1 1 ∈ Clsd ⁡ J
25 15 24 eqeltrd ⊢ f ∈ J Cn II ∧ S = f -1 0 ∧ T = f -1 1 → T ∈ Clsd ⁡ J
26 14 25 jca ⊢ f ∈ J Cn II ∧ S = f -1 0 ∧ T = f -1 1 → S ∈ Clsd ⁡ J ∧ T ∈ Clsd ⁡ J
27 26 rexlimiva ⊢ ∃ f ∈ J Cn II S = f -1 0 ∧ T = f -1 1 → S ∈ Clsd ⁡ J ∧ T ∈ Clsd ⁡ J
28 1 27 syl ⊢ φ → S ∈ Clsd ⁡ J ∧ T ∈ Clsd ⁡ J