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

Proof

Step	Hyp	Ref	Expression
1		seppsepf.1	⊢ ( 𝜑 → ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) )
2		eqimss	⊢ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) → 𝑆 ⊆ ( ◡ 𝑓 “ { 0 } ) )
3		eqimss	⊢ ( 𝑇 = ( ◡ 𝑓 “ { 1 } ) → 𝑇 ⊆ ( ◡ 𝑓 “ { 1 } ) )
4	2 3	anim12i	⊢ ( ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) → ( 𝑆 ⊆ ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( ◡ 𝑓 “ { 1 } ) ) )
5	4	reximi	⊢ ( ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) → ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 ⊆ ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( ◡ 𝑓 “ { 1 } ) ) )
6	1 5	syl	⊢ ( 𝜑 → ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 ⊆ ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 ⊆ ( ◡ 𝑓 “ { 1 } ) ) )