Metamath Proof Explorer

Theorem iccen

Description: Any nontrivial closed interval is equinumerous to the unit interval. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Assertion iccen ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → 0 1 ≈ A B

Proof

Step Hyp Ref Expression
1 ovex ⊢ 0 1 ∈ V
2 ovex ⊢ A B ∈ V
3 eqid ⊢ x ∈ 0 1 ⟼ x ⁢ B + 1 − x ⁢ A = x ∈ 0 1 ⟼ x ⁢ B + 1 − x ⁢ A
4 3 iccf1o ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → x ∈ 0 1 ⟼ x ⁢ B + 1 − x ⁢ A : 0 1 ⟶ 1-1 onto A B ∧ x ∈ 0 1 ⟼ x ⁢ B + 1 − x ⁢ A -1 = y ∈ A B ⟼ y − A B − A
5 4 simpld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → x ∈ 0 1 ⟼ x ⁢ B + 1 − x ⁢ A : 0 1 ⟶ 1-1 onto A B
6 f1oen2g ⊢ 0 1 ∈ V ∧ A B ∈ V ∧ x ∈ 0 1 ⟼ x ⁢ B + 1 − x ⁢ A : 0 1 ⟶ 1-1 onto A B → 0 1 ≈ A B
7 1 2 5 6 mp3an12i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → 0 1 ≈ A B