Let X, Tx, g and h be given.
Assume Hgcont: continuous_map X Tx R R_standard_topology g.
Assume Hhcont: continuous_map X Tx R R_standard_topology h.
We will prove {x ∈ X|Rlt (apply_fun g x) (apply_fun h x)} ∈ Tx.
We prove the intermediate claim HpairCont: continuous_map X Tx EuclidPlane R2_standard_topology (pair_map X g h).
rewrite the current goal using R2_standard_equals_product (from left to right).
An exact proof term for the current goal is (maps_into_products_axiom X Tx R R_standard_topology R R_standard_topology g h Hgcont Hhcont).
Set Lt to be the term {p ∈ EuclidPlane|Rlt (p 0) (p 1)}.
We prove the intermediate claim HLtOpen: Lt ∈ R2_standard_topology.
An exact proof term for the current goal is R2_strict_lt_open.
We prove the intermediate claim HpreOpen: preimage_of X (pair_map X g h) Lt ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx EuclidPlane R2_standard_topology (pair_map X g h) HpairCont Lt HLtOpen).
We prove the intermediate claim HpreEq: preimage_of X (pair_map X g h) Lt = {x ∈ X|Rlt (apply_fun g x) (apply_fun h x)}.
Apply set_ext to the current goal.
Let x be given.
Assume HxPre: x ∈ preimage_of X (pair_map X g h) Lt.
We will prove x ∈ {x0 ∈ X|Rlt (apply_fun g x0) (apply_fun h x0)}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (pair_map X g h) x0 ∈ Lt) x HxPre).
We prove the intermediate claim Himg: apply_fun (pair_map X g h) x ∈ Lt.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (pair_map X g h) x0 ∈ Lt) x HxPre).
We prove the intermediate claim Happ: apply_fun (pair_map X g h) x = (apply_fun g x,apply_fun h x).
An exact proof term for the current goal is (pair_map_apply X R R g h x HxX).
We prove the intermediate claim Himg2: (apply_fun g x,apply_fun h x) ∈ Lt.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is Himg.
We prove the intermediate claim HltPair: Rlt ((apply_fun g x,apply_fun h x) 0) ((apply_fun g x,apply_fun h x) 1).
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ Rlt (p0 0) (p0 1)) (apply_fun g x,apply_fun h x) Himg2).
We prove the intermediate claim Hlt: Rlt (apply_fun g x) (apply_fun h x).
rewrite the current goal using (tuple_2_0_eq (apply_fun g x) (apply_fun h x)) (from right to left) at position 1.
rewrite the current goal using (tuple_2_1_eq (apply_fun g x) (apply_fun h x)) (from right to left) at position 2.
An exact proof term for the current goal is HltPair.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ Rlt (apply_fun g x0) (apply_fun h x0)) x HxX Hlt).
Let x be given.
Assume HxLt: x ∈ {x0 ∈ X|Rlt (apply_fun g x0) (apply_fun h x0)}.
We will prove x ∈ preimage_of X (pair_map X g h) Lt.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ Rlt (apply_fun g x0) (apply_fun h x0)) x HxLt).
We prove the intermediate claim Hlt: Rlt (apply_fun g x) (apply_fun h x).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ Rlt (apply_fun g x0) (apply_fun h x0)) x HxLt).
We prove the intermediate claim HgxR: apply_fun g x ∈ R.
An exact proof term for the current goal is (RltE_left (apply_fun g x) (apply_fun h x) Hlt).
We prove the intermediate claim HhxR: apply_fun h x ∈ R.
An exact proof term for the current goal is (RltE_right (apply_fun g x) (apply_fun h x) Hlt).
We prove the intermediate claim HpPlane: (apply_fun g x,apply_fun h x) ∈ EuclidPlane.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (apply_fun g x) (apply_fun h x) HgxR HhxR).
We prove the intermediate claim HltPair: Rlt ((apply_fun g x,apply_fun h x) 0) ((apply_fun g x,apply_fun h x) 1).
rewrite the current goal using (tuple_2_0_eq (apply_fun g x) (apply_fun h x)) (from left to right).
rewrite the current goal using (tuple_2_1_eq (apply_fun g x) (apply_fun h x)) (from left to right).
An exact proof term for the current goal is Hlt.
We prove the intermediate claim HpLt: (apply_fun g x,apply_fun h x) ∈ Lt.
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ Rlt (p0 0) (p0 1)) (apply_fun g x,apply_fun h x) HpPlane HltPair).
We prove the intermediate claim Happ: apply_fun (pair_map X g h) x = (apply_fun g x,apply_fun h x).
An exact proof term for the current goal is (pair_map_apply X R R g h x HxX).
We prove the intermediate claim Himg: apply_fun (pair_map X g h) x ∈ Lt.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HpLt.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (pair_map X g h) x0 ∈ Lt) x HxX Himg).
rewrite the current goal using HpreEq (from right to left).
An exact proof term for the current goal is HpreOpen.
∎