Metamath Proof Explorer


Theorem seppsepf

Description: If two sets are precisely separated by a continuous function, then they are separated by the continuous function. (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 seppsepf φ f J Cn II S f -1 0 T f -1 1

Proof

Step Hyp Ref Expression
1 seppsepf.1 φ f J Cn II S = f -1 0 T = f -1 1
2 eqimss S = f -1 0 S f -1 0
3 eqimss T = f -1 1 T f -1 1
4 2 3 anim12i S = f -1 0 T = f -1 1 S f -1 0 T f -1 1
5 4 reximi f J Cn II S = f -1 0 T = f -1 1 f J Cn II S f -1 0 T f -1 1
6 1 5 syl φ f J Cn II S f -1 0 T f -1 1