Metamath Proof Explorer

Theorem iirevcn

Description: The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Assertion iirevcn ⊢ x ∈ 0 1 ⟼ 1 − x ∈ II Cn II

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
2 dfii2 ⊢ II = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
3 unitssre ⊢ 0 1 ⊆ ℝ
4 3 a1i ⊢ ⊤ → 0 1 ⊆ ℝ
5 iirev ⊢ x ∈ 0 1 → 1 − x ∈ 0 1
6 5 adantl ⊢ ⊤ ∧ x ∈ 0 1 → 1 − x ∈ 0 1
7 1 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
8 7 a1i ⊢ ⊤ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
9 1cnd ⊢ ⊤ → 1 ∈ ℂ
10 8 8 9 cnmptc ⊢ ⊤ → x ∈ ℂ ⟼ 1 ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
11 8 cnmptid ⊢ ⊤ → x ∈ ℂ ⟼ x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
12 1 subcn ⊢ − ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
13 12 a1i ⊢ ⊤ → − ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
14 8 10 11 13 cnmpt12f ⊢ ⊤ → x ∈ ℂ ⟼ 1 − x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
15 1 2 2 4 4 6 14 cnmptre ⊢ ⊤ → x ∈ 0 1 ⟼ 1 − x ∈ II Cn II
16 15 mptru ⊢ x ∈ 0 1 ⟼ 1 − x ∈ II Cn II