We will prove path_connected_space (EuclidPlane ∖ {(0,0)}) (subspace_topology EuclidPlane R2_standard_topology (EuclidPlane ∖ {(0,0)})).
Set X to be the term EuclidPlane ∖ {(0,0)}.
Set Tx to be the term subspace_topology EuclidPlane R2_standard_topology X.
We will prove topology_on X Tx ∧ ∀x y : set, x ∈ X → y ∈ X → ∃p : set, path_between X x y p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
Apply andI to the current goal.
We prove the intermediate claim HtopPlane: topology_on EuclidPlane R2_standard_topology.
An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology R_standard_topology_is_topology R_standard_topology_is_topology).
We prove the intermediate claim HXsub: X ⊆ EuclidPlane.
An exact proof term for the current goal is (setminus_Subq EuclidPlane {(0,0)}).
An exact proof term for the current goal is (subspace_topology_is_topology EuclidPlane R2_standard_topology X HtopPlane HXsub).
Let x and y be given.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
We will prove ∃p : set, path_between X x y p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
We prove the intermediate claim HTx: topology_on X Tx.
We prove the intermediate claim HtopPlane: topology_on EuclidPlane R2_standard_topology.
An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology R_standard_topology_is_topology R_standard_topology_is_topology).
We prove the intermediate claim HXsub: X ⊆ EuclidPlane.
An exact proof term for the current goal is (setminus_Subq EuclidPlane {(0,0)}).
An exact proof term for the current goal is (subspace_topology_is_topology EuclidPlane R2_standard_topology X HtopPlane HXsub).
Set base to be the term (1,1).
We prove the intermediate claim HbaseX: base ∈ X.
Apply (setminusI EuclidPlane {(0,0)} base) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R 1 1 real_1 real_1).
Assume Hbase0: base ∈ {(0,0)}.
We prove the intermediate claim Heq: base = (0,0).
An exact proof term for the current goal is (SingE (0,0) base Hbase0).
We prove the intermediate claim Hcoords: 1 = 0 ∧ 1 = 0.
An exact proof term for the current goal is (tuple_eq_coords_R2 1 1 0 0 Heq).
An exact proof term for the current goal is (neq_1_0 (andEL (1 = 0) (1 = 0) Hcoords)).
We prove the intermediate claim Hhor_pc: ∀x0 x1 y0 : set, y0 ∈ R → y0 ≠ 0 → x0 ∈ R → x1 ∈ R → (x0,y0) ∈ path_component_of X Tx (x1,y0).
Let x0, x1 and y0 be given.
Assume Hy0R: y0 ∈ R.
Assume Hy0ne: y0 ≠ 0.
Assume Hx0R: x0 ∈ R.
Assume Hx1R: x1 ∈ R.
An exact proof term for the current goal is (punctured_horizontal_slice_path_component x0 x1 y0 Hy0R Hy0ne Hx0R Hx1R).
We prove the intermediate claim Hver_pc: ∀x0 y0 y1 : set, x0 ∈ R → x0 ≠ 0 → y0 ∈ R → y1 ∈ R → (x0,y0) ∈ path_component_of X Tx (x0,y1).
Let x0, y0 and y1 be given.
Assume Hx0R: x0 ∈ R.
Assume Hx0ne: x0 ≠ 0.
Assume Hy0R: y0 ∈ R.
Assume Hy1R: y1 ∈ R.
An exact proof term for the current goal is (punctured_vertical_slice_path_component x0 y0 y1 Hx0R Hx0ne Hy0R Hy1R).
We prove the intermediate claim Hpc_to_base: ∀z : set, z ∈ X → z ∈ path_component_of X Tx base.
Let z be given.
Assume HzX: z ∈ X.
Set a to be the term R2_xcoord z.
Set b to be the term R2_ycoord z.
We prove the intermediate claim Hzpair: z ∈ EuclidPlane ∧ z ∉ {(0,0)}.
An exact proof term for the current goal is (setminusE EuclidPlane {(0,0)} z HzX).
We prove the intermediate claim HzPlane: z ∈ EuclidPlane.
An exact proof term for the current goal is (andEL (z ∈ EuclidPlane) (z ∉ {(0,0)}) Hzpair).
We prove the intermediate claim HzNotO: z ∉ {(0,0)}.
An exact proof term for the current goal is (andER (z ∈ EuclidPlane) (z ∉ {(0,0)}) Hzpair).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R z HzPlane).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R z HzPlane).
Apply (xm (a = 0)) to the current goal.
Assume Ha0: a = 0.
We prove the intermediate claim Hb0ne: b ≠ 0.
Assume Hb0: b = 0.
Apply HzNotO to the current goal.
We will prove z ∈ {(0,0)}.
We prove the intermediate claim Hzeta: (a,b) = z.
An exact proof term for the current goal is (EuclidPlane_eta z HzPlane).
We prove the intermediate claim Hz0: z = (0,0).
We will prove z = (0,0).
rewrite the current goal using Hzeta (from right to left).
rewrite the current goal using Ha0 (from left to right).
rewrite the current goal using Hb0 (from left to right).
Use reflexivity.
rewrite the current goal using Hz0 (from left to right).
An exact proof term for the current goal is (SingI (0,0)).
We prove the intermediate claim HwX: (1,b) ∈ X.
Apply (setminusI EuclidPlane {(0,0)} (1,b)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R 1 b real_1 HbR).
Assume Hw0: (1,b) ∈ {(0,0)}.
We prove the intermediate claim Heq: (1,b) = (0,0).
An exact proof term for the current goal is (SingE (0,0) (1,b) Hw0).
We prove the intermediate claim Hcoords: 1 = 0 ∧ b = 0.
An exact proof term for the current goal is (tuple_eq_coords_R2 1 b 0 0 Heq).
An exact proof term for the current goal is (neq_1_0 (andEL (1 = 0) (b = 0) Hcoords)).
We prove the intermediate claim HwPc: (1,b) ∈ path_component_of X Tx base.
An exact proof term for the current goal is (Hver_pc 1 b 1 real_1 neq_1_0 HbR real_1).
We prove the intermediate claim HzPc: z ∈ path_component_of X Tx (1,b).
We prove the intermediate claim Hzeta: (a,b) = z.
An exact proof term for the current goal is (EuclidPlane_eta z HzPlane).
rewrite the current goal using Hzeta (from right to left) at position 1.
rewrite the current goal using Ha0 (from left to right).
An exact proof term for the current goal is (Hhor_pc 0 1 b HbR Hb0ne real_0 real_1).
An exact proof term for the current goal is (path_component_transitive_axiom X Tx base (1,b) z HTx HbaseX HwX HzX HwPc HzPc).
Assume Ha0: ¬ (a = 0).
We prove the intermediate claim HwX: (a,1) ∈ X.
Apply (setminusI EuclidPlane {(0,0)} (a,1)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R a 1 HaR real_1).
Assume Hw0: (a,1) ∈ {(0,0)}.
We prove the intermediate claim Heq: (a,1) = (0,0).
An exact proof term for the current goal is (SingE (0,0) (a,1) Hw0).
We prove the intermediate claim Hcoords: a = 0 ∧ 1 = 0.
An exact proof term for the current goal is (tuple_eq_coords_R2 a 1 0 0 Heq).
Apply Ha0 to the current goal.
An exact proof term for the current goal is (andEL (a = 0) (1 = 0) Hcoords).
We prove the intermediate claim HwPc: (a,1) ∈ path_component_of X Tx base.
An exact proof term for the current goal is (Hhor_pc a 1 1 real_1 neq_1_0 HaR real_1).
We prove the intermediate claim HzPc: z ∈ path_component_of X Tx (a,1).
We prove the intermediate claim Hzeta: (a,b) = z.
An exact proof term for the current goal is (EuclidPlane_eta z HzPlane).
rewrite the current goal using Hzeta (from right to left) at position 1.
An exact proof term for the current goal is (Hver_pc a b 1 HaR Ha0 HbR real_1).
An exact proof term for the current goal is (path_component_transitive_axiom X Tx base (a,1) z HTx HbaseX HwX HzX HwPc HzPc).
We prove the intermediate claim HxPcBase: x ∈ path_component_of X Tx base.
An exact proof term for the current goal is (Hpc_to_base x Hx).
We prove the intermediate claim HyPcBase: y ∈ path_component_of X Tx base.
An exact proof term for the current goal is (Hpc_to_base y Hy).
We prove the intermediate claim HbasePcx: base ∈ path_component_of X Tx x.
An exact proof term for the current goal is (path_component_symmetric_axiom X Tx base x HTx HbaseX Hx HxPcBase).
We prove the intermediate claim HyPcx: y ∈ path_component_of X Tx x.
An exact proof term for the current goal is (path_component_transitive_axiom X Tx x base y HTx Hx HbaseX Hy HbasePcx HyPcBase).
We prove the intermediate claim Hex: ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y0) y HyPcx).
Apply Hex to the current goal.
Let p be given.
Assume Hp.
We use p to witness the existential quantifier.
We will prove path_between X x y p ∧ continuous_map unit_interval unit_interval_topology X Tx p.
Apply andI to the current goal.
We prove the intermediate claim HpA: ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) ∧ apply_fun p 1 = y.
An exact proof term for the current goal is Hp.
We prove the intermediate claim HpB: (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x.
An exact proof term for the current goal is (andEL ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) HpA).
We prove the intermediate claim HpC: function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p.
An exact proof term for the current goal is (andEL (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) (apply_fun p 0 = x) HpB).
We prove the intermediate claim Hp_fun: function_on p unit_interval X.
An exact proof term for the current goal is (andEL (function_on p unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx p) HpC).
We prove the intermediate claim Hp0eq: apply_fun p 0 = x.
An exact proof term for the current goal is (andER (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) (apply_fun p 0 = x) HpB).
We prove the intermediate claim Hp1eq: apply_fun p 1 = y.
An exact proof term for the current goal is (andER ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) HpA).
An exact proof term for the current goal is (path_betweenI X x y p Hp_fun Hp0eq Hp1eq).
We prove the intermediate claim HpA: ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) ∧ apply_fun p 1 = y.
An exact proof term for the current goal is Hp.
We prove the intermediate claim HpB: (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x.
An exact proof term for the current goal is (andEL ((function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) HpA).
We prove the intermediate claim HpC: function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p.
An exact proof term for the current goal is (andEL (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) (apply_fun p 0 = x) HpB).
An exact proof term for the current goal is (andER (function_on p unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx p) HpC).
∎