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

Proof

Step	Hyp	Ref	Expression
1		seppsepf.1	|- ( ph -> E. f e. ( J Cn II ) ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) )
2		eqimss	|- ( S = ( `' f " { 0 } ) -> S C_ ( `' f " { 0 } ) )
3		eqimss	|- ( T = ( `' f " { 1 } ) -> T C_ ( `' f " { 1 } ) )
4	2 3	anim12i	|- ( ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) -> ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) )
5	4	reximi	|- ( E. f e. ( J Cn II ) ( S = ( `' f " { 0 } ) /\ T = ( `' f " { 1 } ) ) -> E. f e. ( J Cn II ) ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) )
6	1 5	syl	|- ( ph -> E. f e. ( J Cn II ) ( S C_ ( `' f " { 0 } ) /\ T C_ ( `' f " { 1 } ) ) )