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 \in ℝ \land B \in ℝ \land A < B) \to [0, 1] \approx [A, B]$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ [0, 1] \in V$
2		ovex	$⊢ [A, B] \in V$
3		eqid	$⊢ (x \in [0, 1] ⟼ x B + (1 - x) A) = (x \in [0, 1] ⟼ x B + (1 - x) A)$
4	3	iccf1o	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to ((x \in [0, 1] ⟼ x B + (1 - x) A) : [0, 1] \underset{1-1 onto}{⟶} [A, B] \land {(x \in [0, 1] ⟼ x B + (1 - x) A)}^{-1} = (y \in [A, B] ⟼ \frac{y - A}{B - A}))$
5	4	simpld	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ x B + (1 - x) A) : [0, 1] \underset{1-1 onto}{⟶} [A, B]$
6		f1oen2g	$⊢ ([0, 1] \in V \land [A, B] \in V \land (x \in [0, 1] ⟼ x B + (1 - x) A) : [0, 1] \underset{1-1 onto}{⟶} [A, B]) \to [0, 1] \approx [A, B]$
7	1 2 5 6	mp3an12i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to [0, 1] \approx [A, B]$