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

Proof

Step	Hyp	Ref	Expression
1		seppsepf.1	⊢ ( 𝜑 → ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) )
2		simprl	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) ) → 𝑆 = ( ◡ 𝑓 “ { 0 } ) )
3		simpl	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) ) → 𝑓 ∈ ( 𝐽 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	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ { 0 } ∈ ( Clsd ‘ II ) ) → ( ◡ 𝑓 “ { 0 } ) ∈ ( Clsd ‘ 𝐽 ) )
13	3 11 12	sylancl	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) ) → ( ◡ 𝑓 “ { 0 } ) ∈ ( Clsd ‘ 𝐽 ) )
14	2 13	eqeltrd	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
15		simprr	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 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	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ { 1 } ∈ ( Clsd ‘ II ) ) → ( ◡ 𝑓 “ { 1 } ) ∈ ( Clsd ‘ 𝐽 ) )
24	3 22 23	sylancl	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) ) → ( ◡ 𝑓 “ { 1 } ) ∈ ( Clsd ‘ 𝐽 ) )
25	15 24	eqeltrd	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) ) → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
26	14 25	jca	⊢ ( ( 𝑓 ∈ ( 𝐽 Cn II ) ∧ ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) )
27	26	rexlimiva	⊢ ( ∃ 𝑓 ∈ ( 𝐽 Cn II ) ( 𝑆 = ( ◡ 𝑓 “ { 0 } ) ∧ 𝑇 = ( ◡ 𝑓 “ { 1 } ) ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) )
28	1 27	syl	⊢ ( 𝜑 → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) )