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 ( 𝜑 → ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) )
Assertion seppcld ( 𝜑 → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 seppsepf.1 ( 𝜑 → ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) )
2 simprl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) ) → 𝑆 = ( 𝑓 “ { 0 } ) )
3 simpl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) ) → 𝑓 ∈ ( 𝐽 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 ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ { 0 } ∈ ( Clsd ‘ II ) ) → ( 𝑓 “ { 0 } ) ∈ ( Clsd ‘ 𝐽 ) )
13 3 11 12 sylancl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) ) → ( 𝑓 “ { 0 } ) ∈ ( Clsd ‘ 𝐽 ) )
14 2 13 eqeltrd ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
15 simprr ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 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 ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ { 1 } ∈ ( Clsd ‘ II ) ) → ( 𝑓 “ { 1 } ) ∈ ( Clsd ‘ 𝐽 ) )
24 3 22 23 sylancl ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) ) → ( 𝑓 “ { 1 } ) ∈ ( Clsd ‘ 𝐽 ) )
25 15 24 eqeltrd ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) ) → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
26 14 25 jca ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) )
27 26 rexlimiva ( ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 = ( 𝑓 “ { 0 } ) ∧ 𝑇 = ( 𝑓 “ { 1 } ) ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) )
28 1 27 syl ( 𝜑 → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) )