Let X, A, B, Y, Tx, Ty, f and g be given.
Assume HTx: topology_on X Tx.
Assume HA: A ∈ Tx.
Assume HB: B ∈ Tx.
Assume Hdisj: A ∩ B = Empty.
Assume Hdomf: graph_domain_subset f A.
Assume Hdomg: graph_domain_subset g B.
Assume Hfunf: functional_graph f.
Assume Hfung: functional_graph g.
Assume Hf: continuous_map_total A (subspace_topology X Tx A) Y Ty f.
Assume Hg: continuous_map_total B (subspace_topology X Tx B) Y Ty g.
We will prove continuous_map_total (A ∪ B) (subspace_topology X Tx (A ∪ B)) Y Ty (f ∪ g).
We prove the intermediate claim Hf_left: (topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty) ∧ total_function_on f A Y.
An exact proof term for the current goal is (andEL ((topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty) ∧ total_function_on f A Y) (∀V : set, V ∈ Ty → preimage_of A f V ∈ subspace_topology X Tx A) Hf).
We prove the intermediate claim Hpreimg_f: ∀V : set, V ∈ Ty → preimage_of A f V ∈ subspace_topology X Tx A.
An exact proof term for the current goal is (andER ((topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty) ∧ total_function_on f A Y) (∀V : set, V ∈ Ty → preimage_of A f V ∈ subspace_topology X Tx A) Hf).
We prove the intermediate claim Hf_tops: topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty.
An exact proof term for the current goal is (andEL (topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty) (total_function_on f A Y) Hf_left).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andER (topology_on A (subspace_topology X Tx A)) (topology_on Y Ty) Hf_tops).
We prove the intermediate claim Htotf: total_function_on f A Y.
An exact proof term for the current goal is (andER (topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty) (total_function_on f A Y) Hf_left).
We prove the intermediate claim Hg_left: (topology_on B (subspace_topology X Tx B) ∧ topology_on Y Ty) ∧ total_function_on g B Y.
An exact proof term for the current goal is (andEL ((topology_on B (subspace_topology X Tx B) ∧ topology_on Y Ty) ∧ total_function_on g B Y) (∀V : set, V ∈ Ty → preimage_of B g V ∈ subspace_topology X Tx B) Hg).
We prove the intermediate claim Hpreimg_g: ∀V : set, V ∈ Ty → preimage_of B g V ∈ subspace_topology X Tx B.
An exact proof term for the current goal is (andER ((topology_on B (subspace_topology X Tx B) ∧ topology_on Y Ty) ∧ total_function_on g B Y) (∀V : set, V ∈ Ty → preimage_of B g V ∈ subspace_topology X Tx B) Hg).
We prove the intermediate claim Htotg: total_function_on g B Y.
An exact proof term for the current goal is (andER (topology_on B (subspace_topology X Tx B) ∧ topology_on Y Ty) (total_function_on g B Y) Hg_left).
We prove the intermediate claim HAB_sub: A ∪ B ⊆ X.
Apply binunion_Subq_min to the current goal.
An exact proof term for the current goal is (topology_elem_subset X Tx A HTx HA).
An exact proof term for the current goal is (topology_elem_subset X Tx B HTx HB).
We prove the intermediate claim HTsub: topology_on (A ∪ B) (subspace_topology X Tx (A ∪ B)).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx (A ∪ B) HTx HAB_sub).
We prove the intermediate claim Htotfg: total_function_on (f ∪ g) (A ∪ B) Y.
An exact proof term for the current goal is (total_function_union_on_disjoint_total_functional A B Y f g Hdisj Hdomf Hdomg Htotf Htotg Hfunf Hfung).
We prove the intermediate claim Hpreimg_fg: ∀V : set, V ∈ Ty → preimage_of (A ∪ B) (f ∪ g) V ∈ subspace_topology X Tx (A ∪ B).
Let V be given.
Assume HV: V ∈ Ty.
We prove the intermediate claim Heq: preimage_of (A ∪ B) (f ∪ g) V = (preimage_of A f V) ∪ (preimage_of B g V).
An exact proof term for the current goal is (preimage_of_union_functions_total A B Y f g V Hdisj Hdomf Hdomg Htotf Htotg Hfunf Hfung).
We prove the intermediate claim HfV: preimage_of A f V ∈ subspace_topology X Tx A.
An exact proof term for the current goal is (Hpreimg_f V HV).
We prove the intermediate claim HgV: preimage_of B g V ∈ subspace_topology X Tx B.
An exact proof term for the current goal is (Hpreimg_g V HV).
We prove the intermediate claim Hunion: (preimage_of A f V ∪ preimage_of B g V) ∈ subspace_topology X Tx (A ∪ B).
An exact proof term for the current goal is (subspace_union_of_opens X Tx A B (preimage_of A f V) (preimage_of B g V) HTx HA HB Hdisj HfV HgV).
We will prove preimage_of (A ∪ B) (f ∪ g) V ∈ subspace_topology X Tx (A ∪ B).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hunion.
We will prove ((topology_on (A ∪ B) (subspace_topology X Tx (A ∪ B)) ∧ topology_on Y Ty) ∧ total_function_on (f ∪ g) (A ∪ B) Y) ∧ (∀V : set, V ∈ Ty → preimage_of (A ∪ B) (f ∪ g) V ∈ subspace_topology X Tx (A ∪ B)).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTsub.
An exact proof term for the current goal is HTy.
An exact proof term for the current goal is Htotfg.
An exact proof term for the current goal is Hpreimg_fg.
∎