Metamath Proof Explorer

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