Theorem iccioo01

Description: The closed unit interval is equinumerous to the open unit interval. Based on a Mastodon post by Michael Kinyon. (Contributed by Jim Kingdon, 4-Jun-2024)

	Ref	Expression
Assertion	iccioo01	⊢ ( 0 [,] 1 ) ≈ ( 0 (,) 1 )

Proof

Step	Hyp	Ref	Expression
1		4nn	⊢ 4 ∈ ℕ
2		nnrecre	⊢ ( 4 ∈ ℕ → ( 1 / 4 ) ∈ ℝ )
3	1 2	ax-mp	⊢ ( 1 / 4 ) ∈ ℝ
4		halfre	⊢ ( 1 / 2 ) ∈ ℝ
5		2lt4	⊢ 2 < 4
6		2re	⊢ 2 ∈ ℝ
7		4re	⊢ 4 ∈ ℝ
8		2pos	⊢ 0 < 2
9		4pos	⊢ 0 < 4
10	6 7 8 9	ltrecii	⊢ ( 2 < 4 ↔ ( 1 / 4 ) < ( 1 / 2 ) )
11	5 10	mpbi	⊢ ( 1 / 4 ) < ( 1 / 2 )
12		iccen	⊢ ( ( ( 1 / 4 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ∧ ( 1 / 4 ) < ( 1 / 2 ) ) → ( 0 [,] 1 ) ≈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
13	3 4 11 12	mp3an	⊢ ( 0 [,] 1 ) ≈ ( ( 1 / 4 ) [,] ( 1 / 2 ) )
14		ovex	⊢ ( 0 (,) 1 ) ∈ V
15		0xr	⊢ 0 ∈ ℝ*
16		1xr	⊢ 1 ∈ ℝ*
17	7 9	recgt0ii	⊢ 0 < ( 1 / 4 )
18		halflt1	⊢ ( 1 / 2 ) < 1
19		iccssioo	⊢ ( ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) ∧ ( 0 < ( 1 / 4 ) ∧ ( 1 / 2 ) < 1 ) ) → ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ⊆ ( 0 (,) 1 ) )
20	15 16 17 18 19	mp4an	⊢ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ⊆ ( 0 (,) 1 )
21		ssdomg	⊢ ( ( 0 (,) 1 ) ∈ V → ( ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ⊆ ( 0 (,) 1 ) → ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ≼ ( 0 (,) 1 ) ) )
22	14 20 21	mp2	⊢ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ≼ ( 0 (,) 1 )
23		endomtr	⊢ ( ( ( 0 [,] 1 ) ≈ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ∧ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ≼ ( 0 (,) 1 ) ) → ( 0 [,] 1 ) ≼ ( 0 (,) 1 ) )
24	13 22 23	mp2an	⊢ ( 0 [,] 1 ) ≼ ( 0 (,) 1 )
25		ovex	⊢ ( 0 [,] 1 ) ∈ V
26		ioossicc	⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 )
27		ssdomg	⊢ ( ( 0 [,] 1 ) ∈ V → ( ( 0 (,) 1 ) ⊆ ( 0 [,] 1 ) → ( 0 (,) 1 ) ≼ ( 0 [,] 1 ) ) )
28	25 26 27	mp2	⊢ ( 0 (,) 1 ) ≼ ( 0 [,] 1 )
29		sbth	⊢ ( ( ( 0 [,] 1 ) ≼ ( 0 (,) 1 ) ∧ ( 0 (,) 1 ) ≼ ( 0 [,] 1 ) ) → ( 0 [,] 1 ) ≈ ( 0 (,) 1 ) )
30	24 28 29	mp2an	⊢ ( 0 [,] 1 ) ≈ ( 0 (,) 1 )