Let X, Tx and x be given.
Assume HTx: topology_on X Tx.
Assume HxX: x ∈ X.
Set J to be the term {U ∈ Tx|x ∈ U}.
Set le to be the term rev_inclusion_rel J.
We will prove directed_set J le.
We will prove (J ≠ Empty ∧ partial_order_on J le) ∧ ∀a b : set, a ∈ J → b ∈ J → ∃c : set, c ∈ J ∧ (a,c) ∈ le ∧ (b,c) ∈ le.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HXJ: X ∈ J.
An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ x ∈ U0) X HXTx HxX).
An exact proof term for the current goal is (elem_implies_nonempty J X HXJ).
We will prove partial_order_on J le.
We will prove relation_on le J ∧ (∀a : set, a ∈ J → (a,a) ∈ le) ∧ (∀a b : set, a ∈ J → b ∈ J → (a,b) ∈ le → (b,a) ∈ le → a = b) ∧ (∀a b c : set, a ∈ J → b ∈ J → c ∈ J → (a,b) ∈ le → (b,c) ∈ le → (a,c) ∈ le).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove relation_on le J.
Let a and b be given.
Assume Hab: (a,b) ∈ le.
We will prove a ∈ J ∧ b ∈ J.
We prove the intermediate claim Hprod: (a,b) ∈ setprod J J.
An exact proof term for the current goal is (andEL ((a,b) ∈ setprod J J) (b ⊆ a) (rev_inclusion_relE J a b Hab)).
We prove the intermediate claim Ha0: (a,b) 0 ∈ J.
An exact proof term for the current goal is (ap0_Sigma J (λ_ : set ⇒ J) (a,b) Hprod).
We prove the intermediate claim Hb1: (a,b) 1 ∈ J.
An exact proof term for the current goal is (ap1_Sigma J (λ_ : set ⇒ J) (a,b) Hprod).
Apply andI to the current goal.
rewrite the current goal using (tuple_2_0_eq a b) (from right to left).
An exact proof term for the current goal is Ha0.
rewrite the current goal using (tuple_2_1_eq a b) (from right to left).
An exact proof term for the current goal is Hb1.
Let a be given.
Assume HaJ: a ∈ J.
We will prove (a,a) ∈ le.
Apply (rev_inclusion_relI J a a) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J J a a HaJ HaJ).
An exact proof term for the current goal is (Subq_ref a).
Let a and b be given.
Assume HaJ: a ∈ J.
Assume HbJ: b ∈ J.
Assume Hab: (a,b) ∈ le.
Assume Hba: (b,a) ∈ le.
We will prove a = b.
We prove the intermediate claim Hab_sub: b ⊆ a.
An exact proof term for the current goal is (andER ((a,b) ∈ setprod J J) (b ⊆ a) (rev_inclusion_relE J a b Hab)).
We prove the intermediate claim Hba_sub: a ⊆ b.
An exact proof term for the current goal is (andER ((b,a) ∈ setprod J J) (a ⊆ b) (rev_inclusion_relE J b a Hba)).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ a.
We will prove y ∈ b.
An exact proof term for the current goal is (Hba_sub y Hy).
Let y be given.
Assume Hy: y ∈ b.
We will prove y ∈ a.
An exact proof term for the current goal is (Hab_sub y Hy).
Let a, b and c be given.
Assume HaJ: a ∈ J.
Assume HbJ: b ∈ J.
Assume HcJ: c ∈ J.
Assume Hab: (a,b) ∈ le.
Assume Hbc: (b,c) ∈ le.
We will prove (a,c) ∈ le.
We prove the intermediate claim Hab_sub: b ⊆ a.
An exact proof term for the current goal is (andER ((a,b) ∈ setprod J J) (b ⊆ a) (rev_inclusion_relE J a b Hab)).
We prove the intermediate claim Hbc_sub: c ⊆ b.
An exact proof term for the current goal is (andER ((b,c) ∈ setprod J J) (c ⊆ b) (rev_inclusion_relE J b c Hbc)).
We prove the intermediate claim Hca: c ⊆ a.
An exact proof term for the current goal is (Subq_tra c b a Hbc_sub Hab_sub).
Apply (rev_inclusion_relI J a c) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J J a c HaJ HcJ).
An exact proof term for the current goal is Hca.
Let U and V be given.
Assume HUJ: U ∈ J.
Assume HVJ: V ∈ J.
We use (U ∩ V) to witness the existential quantifier.
We will prove U ∩ V ∈ J ∧ (U,U ∩ V) ∈ le ∧ (V,U ∩ V) ∈ le.
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ x ∈ U0) U HUJ).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ x ∈ U0) V HVJ).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ x ∈ U0) U HUJ).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ x ∈ U0) V HVJ).
We prove the intermediate claim HWTx: U ∩ V ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U V HTx HUTx HVTx).
We prove the intermediate claim HxW: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HWJ: U ∩ V ∈ J.
An exact proof term for the current goal is (SepI Tx (λU0 : set ⇒ x ∈ U0) (U ∩ V) HWTx HxW).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HWJ.
Apply (rev_inclusion_relI J U (U ∩ V)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J J U (U ∩ V) HUJ HWJ).
An exact proof term for the current goal is (binintersect_Subq_1 U V).
Apply (rev_inclusion_relI J V (U ∩ V)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J J V (U ∩ V) HVJ HWJ).
An exact proof term for the current goal is (binintersect_Subq_2 U V).
∎