Let X and Tx be given.
Assume HTx: topology_on X Tx.
We will prove let id ≔ {(x,x)|x ∈ X} in continuous_map X Tx X Tx id.
Set id to be the term {(x,x)|x ∈ X}.
We will prove continuous_map X Tx X Tx id.
We will prove topology_on X Tx ∧ topology_on X Tx ∧ function_on id X X ∧ ∀V : set, V ∈ Tx → preimage_of X id V ∈ Tx.
We prove the intermediate claim Hpart1: topology_on X Tx ∧ topology_on X Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HTx.
We prove the intermediate claim Hpart2: (topology_on X Tx ∧ topology_on X Tx) ∧ function_on id X X.
Apply andI to the current goal.
An exact proof term for the current goal is Hpart1.
We will prove function_on id X X.
We will prove ∀x : set, x ∈ X → apply_fun id x ∈ X.
Let x be given.
Assume Hx: x ∈ X.
We will prove apply_fun id x ∈ X.
We prove the intermediate claim Hid_x: apply_fun id x = x.
An exact proof term for the current goal is (identity_function_apply X x Hx).
rewrite the current goal using Hid_x (from left to right).
An exact proof term for the current goal is Hx.
Apply andI to the current goal.
An exact proof term for the current goal is Hpart2.
Let V be given.
Assume HV: V ∈ Tx.
We will prove preimage_of X id V ∈ Tx.
We prove the intermediate claim HVsub: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V HTx HV).
We prove the intermediate claim Hpreimg_eq: preimage_of X id V = V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X id V.
We will prove x ∈ V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λy ⇒ apply_fun id y ∈ V) x Hx).
We prove the intermediate claim Hidx_in_V: apply_fun id x ∈ V.
An exact proof term for the current goal is (SepE2 X (λy ⇒ apply_fun id y ∈ V) x Hx).
We prove the intermediate claim Hidx_eq: apply_fun id x = x.
An exact proof term for the current goal is (identity_function_apply X x HxX).
rewrite the current goal using Hidx_eq (from right to left).
An exact proof term for the current goal is Hidx_in_V.
Let x be given.
Assume Hx: x ∈ V.
We will prove x ∈ preimage_of X id V.
We will prove x ∈ {y ∈ X|apply_fun id y ∈ V}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HVsub x Hx).
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
We will prove apply_fun id x ∈ V.
We prove the intermediate claim Hidx_eq: apply_fun id x = x.
An exact proof term for the current goal is (identity_function_apply X x HxX).
rewrite the current goal using Hidx_eq (from left to right).
An exact proof term for the current goal is Hx.
rewrite the current goal using Hpreimg_eq (from left to right).
An exact proof term for the current goal is HV.
∎