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