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 
|- ( ph -> E. f e. ( J Cn II ) ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) )
Assertion seppcld 
|- ( ph -> ( S e. ( Clsd ` J ) /\ T e. ( Clsd ` J ) ) )

Proof

Step Hyp Ref Expression
1 seppsepf.1 
 |-  ( ph -> E. f e. ( J Cn II ) ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) )
2 simprl 
 |-  ( ( f e. ( J Cn II ) /\ ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) ) -> S = ( `' f " { 0 } ) )
3 simpl 
 |-  ( ( f e. ( J Cn II ) /\ ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) ) -> f e. ( J Cn II ) )
4 0xr 
 |-  0 e. RR*
5 iccid 
 |-  ( 0 e. RR* -> ( 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 ) e. ( Clsd ` II ) )
10 7 8 9 mp2an 
 |-  ( 0 [,] 0 ) e. ( Clsd ` II )
11 6 10 eqeltrri 
 |-  { 0 } e. ( Clsd ` II )
12 cnclima 
 |-  ( ( f e. ( J Cn II ) /\ { 0 } e. ( Clsd ` II ) ) -> ( `' f " { 0 } ) e. ( Clsd ` J ) )
13 3 11 12 sylancl 
 |-  ( ( f e. ( J Cn II ) /\ ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) ) -> ( `' f " { 0 } ) e. ( Clsd ` J ) )
14 2 13 eqeltrd 
 |-  ( ( f e. ( J Cn II ) /\ ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) ) -> S e. ( Clsd ` J ) )
15 simprr 
 |-  ( ( f e. ( J Cn II ) /\ ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) ) -> T = ( `' f " { 1 } ) )
16 1xr 
 |-  1 e. RR*
17 iccid 
 |-  ( 1 e. RR* -> ( 1 [,] 1 ) = { 1 } )
18 16 17 ax-mp 
 |-  ( 1 [,] 1 ) = { 1 }
19 1le1 
 |-  1 <_ 1
20 icccldii 
 |-  ( ( 0 <_ 1 /\ 1 <_ 1 ) -> ( 1 [,] 1 ) e. ( Clsd ` II ) )
21 8 19 20 mp2an 
 |-  ( 1 [,] 1 ) e. ( Clsd ` II )
22 18 21 eqeltrri 
 |-  { 1 } e. ( Clsd ` II )
23 cnclima 
 |-  ( ( f e. ( J Cn II ) /\ { 1 } e. ( Clsd ` II ) ) -> ( `' f " { 1 } ) e. ( Clsd ` J ) )
24 3 22 23 sylancl 
 |-  ( ( f e. ( J Cn II ) /\ ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) ) -> ( `' f " { 1 } ) e. ( Clsd ` J ) )
25 15 24 eqeltrd 
 |-  ( ( f e. ( J Cn II ) /\ ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) ) -> T e. ( Clsd ` J ) )
26 14 25 jca 
 |-  ( ( f e. ( J Cn II ) /\ ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) ) -> ( S e. ( Clsd ` J ) /\ T e. ( Clsd ` J ) ) )
27 26 rexlimiva 
 |-  ( E. f e. ( J Cn II ) ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) -> ( S e. ( Clsd ` J ) /\ T e. ( Clsd ` J ) ) )
28 1 27 syl 
 |-  ( ph -> ( S e. ( Clsd ` J ) /\ T e. ( Clsd ` J ) ) )