Metamath Proof Explorer

Theorem dfii5

Description: The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion dfii5 ⊢ II = ordTop ⁡ ≤ ∩ 0 1 × 0 1

Proof

Step Hyp Ref Expression
1 dfii2 ⊢ II = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
2 unitssre ⊢ 0 1 ⊆ ℝ
3 eqid ⊢ ordTop ⁡ ≤ = ordTop ⁡ ≤
4 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
5 3 4 xrrest ⊢ 0 1 ⊆ ℝ → ordTop ⁡ ≤ ↾ 𝑡 0 1 = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
6 2 5 ax-mp ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 1 = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
7 ordtresticc ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 1 = ordTop ⁡ ≤ ∩ 0 1 × 0 1
8 1 6 7 3eqtr2i ⊢ II = ordTop ⁡ ≤ ∩ 0 1 × 0 1