We prove the intermediate claim HtopStd: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HtopUpper: topology_on R R_upper_limit_topology.
An exact proof term for the current goal is R_upper_limit_topology_is_topology_local.
We prove the intermediate claim HcontAll: finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology ∧ finer_than R_standard_topology R_finite_complement_topology ∧ finer_than R_standard_topology R_ray_topology.
An exact proof term for the current goal is ex13_7_R_topology_containments.
We prove the intermediate claim Hleft1: (finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) ∧ finer_than R_standard_topology R_finite_complement_topology.
An exact proof term for the current goal is (andEL ((finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) ∧ finer_than R_standard_topology R_finite_complement_topology) (finer_than R_standard_topology R_ray_topology) HcontAll).
We prove the intermediate claim Hleft2: finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology.
An exact proof term for the current goal is (andEL (finer_than R_upper_limit_topology R_standard_topology ∧ finer_than R_K_topology R_standard_topology) (finer_than R_standard_topology R_finite_complement_topology) Hleft1).
We prove the intermediate claim Hsub: R_standard_topology ⊆ R_upper_limit_topology.
An exact proof term for the current goal is (andEL (finer_than R_upper_limit_topology R_standard_topology) (finer_than R_K_topology R_standard_topology) Hleft2).
We prove the intermediate claim HpropStd: ∀x y : set, x ∈ R → y ∈ R → x ≠ y → (∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ y ∉ U) ∧ (∃V : set, V ∈ R_standard_topology ∧ y ∈ V ∧ x ∉ V).
An exact proof term for the current goal is (iffEL (T1_space R R_standard_topology) (∀x y : set, x ∈ R → y ∈ R → x ≠ y → (∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ y ∉ U) ∧ (∃V : set, V ∈ R_standard_topology ∧ y ∈ V ∧ x ∉ V)) (ex17_15_T1_characterization R R_standard_topology HtopStd) R_standard_topology_T1).
Apply (iffER (T1_space R R_upper_limit_topology) (∀x y : set, x ∈ R → y ∈ R → x ≠ y → (∃U : set, U ∈ R_upper_limit_topology ∧ x ∈ U ∧ y ∉ U) ∧ (∃V : set, V ∈ R_upper_limit_topology ∧ y ∈ V ∧ x ∉ V)) (ex17_15_T1_characterization R R_upper_limit_topology HtopUpper)) to the current goal.
Let x and y be given.
Assume HxR: x ∈ R.
Assume HyR: y ∈ R.
Assume Hne: x ≠ y.
We prove the intermediate claim Hprop: (∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ y ∉ U) ∧ (∃V : set, V ∈ R_standard_topology ∧ y ∈ V ∧ x ∉ V).
An exact proof term for the current goal is (HpropStd x y HxR HyR Hne).
Apply andI to the current goal.
We prove the intermediate claim HexU: ∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ y ∉ U.
An exact proof term for the current goal is (andEL (∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ y ∉ U) (∃V : set, V ∈ R_standard_topology ∧ y ∈ V ∧ x ∉ V) Hprop).
Apply HexU to the current goal.
Let U be given.
Assume HU.
We use U to witness the existential quantifier.
We prove the intermediate claim Hpre: U ∈ R_standard_topology ∧ x ∈ U.
An exact proof term for the current goal is (andEL (U ∈ R_standard_topology ∧ x ∈ U) (y ∉ U) HU).
We prove the intermediate claim HUinStd: U ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (U ∈ R_standard_topology) (x ∈ U) Hpre).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ R_standard_topology) (x ∈ U) Hpre).
We prove the intermediate claim Hnoty: y ∉ U.
An exact proof term for the current goal is (andER (U ∈ R_standard_topology ∧ x ∈ U) (y ∉ U) HU).
We prove the intermediate claim HUinUpper: U ∈ R_upper_limit_topology.
An exact proof term for the current goal is (Hsub U HUinStd).
We will prove U ∈ R_upper_limit_topology ∧ x ∈ U ∧ y ∉ U.
Apply andI to the current goal.
We will prove U ∈ R_upper_limit_topology ∧ x ∈ U.
Apply andI to the current goal.
An exact proof term for the current goal is HUinUpper.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is Hnoty.
We prove the intermediate claim HexV: ∃V : set, V ∈ R_standard_topology ∧ y ∈ V ∧ x ∉ V.
An exact proof term for the current goal is (andER (∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ y ∉ U) (∃V : set, V ∈ R_standard_topology ∧ y ∈ V ∧ x ∉ V) Hprop).
Apply HexV to the current goal.
Let V be given.
Assume HV.
We use V to witness the existential quantifier.
We prove the intermediate claim Hpre: V ∈ R_standard_topology ∧ y ∈ V.
An exact proof term for the current goal is (andEL (V ∈ R_standard_topology ∧ y ∈ V) (x ∉ V) HV).
We prove the intermediate claim HVinStd: V ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (V ∈ R_standard_topology) (y ∈ V) Hpre).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andER (V ∈ R_standard_topology) (y ∈ V) Hpre).
We prove the intermediate claim Hnotx: x ∉ V.
An exact proof term for the current goal is (andER (V ∈ R_standard_topology ∧ y ∈ V) (x ∉ V) HV).
We prove the intermediate claim HVinUpper: V ∈ R_upper_limit_topology.
An exact proof term for the current goal is (Hsub V HVinStd).
We will prove V ∈ R_upper_limit_topology ∧ y ∈ V ∧ x ∉ V.
Apply andI to the current goal.
We will prove V ∈ R_upper_limit_topology ∧ y ∈ V.
Apply andI to the current goal.
An exact proof term for the current goal is HVinUpper.
An exact proof term for the current goal is HyV.
An exact proof term for the current goal is Hnotx.
∎