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] \approx (0, 1)$

Proof

Step	Hyp	Ref	Expression
1		4nn	$⊢ 4 \in ℕ$
2		nnrecre	$⊢ 4 \in ℕ \to \frac{1}{4} \in ℝ$
3	1 2	ax-mp	$⊢ \frac{1}{4} \in ℝ$
4		halfre	$⊢ \frac{1}{2} \in ℝ$
5		2lt4	$⊢ 2 < 4$
6		2re	$⊢ 2 \in ℝ$
7		4re	$⊢ 4 \in ℝ$
8		2pos	$⊢ 0 < 2$
9		4pos	$⊢ 0 < 4$
10	6 7 8 9	ltrecii	$⊢ 2 < 4 \leftrightarrow \frac{1}{4} < \frac{1}{2}$
11	5 10	mpbi	$⊢ \frac{1}{4} < \frac{1}{2}$
12		iccen	$⊢ (\frac{1}{4} \in ℝ \land \frac{1}{2} \in ℝ \land \frac{1}{4} < \frac{1}{2}) \to [0, 1] \approx [\frac{1}{4}, \frac{1}{2}]$
13	3 4 11 12	mp3an	$⊢ [0, 1] \approx [\frac{1}{4}, \frac{1}{2}]$
14		ovex	$⊢ (0, 1) \in V$
15		0xr	$⊢ 0 \in ℝ^{*}$
16		1xr	$⊢ 1 \in ℝ^{*}$
17	7 9	recgt0ii	$⊢ 0 < \frac{1}{4}$
18		halflt1	$⊢ \frac{1}{2} < 1$
19		iccssioo	$⊢ ((0 \in ℝ^{} \land 1 \in ℝ^{}) \land (0 < \frac{1}{4} \land \frac{1}{2} < 1)) \to [\frac{1}{4}, \frac{1}{2}] \subseteq (0, 1)$
20	15 16 17 18 19	mp4an	$⊢ [\frac{1}{4}, \frac{1}{2}] \subseteq (0, 1)$
21		ssdomg	$⊢ (0, 1) \in V \to ([\frac{1}{4}, \frac{1}{2}] \subseteq (0, 1) \to [\frac{1}{4}, \frac{1}{2}] ≼ (0, 1))$
22	14 20 21	mp2	$⊢ [\frac{1}{4}, \frac{1}{2}] ≼ (0, 1)$
23		endomtr	$⊢ ([0, 1] \approx [\frac{1}{4}, \frac{1}{2}] \land [\frac{1}{4}, \frac{1}{2}] ≼ (0, 1)) \to [0, 1] ≼ (0, 1)$
24	13 22 23	mp2an	$⊢ [0, 1] ≼ (0, 1)$
25		ovex	$⊢ [0, 1] \in V$
26		ioossicc	$⊢ (0, 1) \subseteq [0, 1]$
27		ssdomg	$⊢ [0, 1] \in V \to ((0, 1) \subseteq [0, 1] \to (0, 1) ≼ [0, 1])$
28	25 26 27	mp2	$⊢ (0, 1) ≼ [0, 1]$
29		sbth	$⊢ ([0, 1] ≼ (0, 1) \land (0, 1) ≼ [0, 1]) \to [0, 1] \approx (0, 1)$
30	24 28 29	mp2an	$⊢ [0, 1] \approx (0, 1)$

Metamath Proof Explorer

Theorem iccioo01

Proof