Let A, B, Y, f, g and V be given.
Assume Hdisj: A ∩ B = Empty.
Assume Hdomf: graph_domain_subset f A.
Assume Hdomg: graph_domain_subset g B.
Assume Htotf: total_function_on f A Y.
Assume Htotg: total_function_on g B Y.
Assume Hfunf: functional_graph f.
Assume Hfung: functional_graph g.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of (A ∪ B) (f ∪ g) V.
We will prove x ∈ (preimage_of A f V) ∪ (preimage_of B g V).
We prove the intermediate claim HxAB: x ∈ (A ∪ B).
An exact proof term for the current goal is (SepE1 (A ∪ B) (λx0 : set ⇒ apply_fun (f ∪ g) x0 ∈ V) x Hx).
We prove the intermediate claim HfxV: apply_fun (f ∪ g) x ∈ V.
An exact proof term for the current goal is (SepE2 (A ∪ B) (λx0 : set ⇒ apply_fun (f ∪ g) x0 ∈ V) x Hx).
Apply (binunionE A B x HxAB) to the current goal.
Assume HxA: x ∈ A.
We prove the intermediate claim Happ: apply_fun (f ∪ g) x = apply_fun f x.
An exact proof term for the current goal is (apply_fun_union_left A B Y f g x Hdisj Hdomf Hdomg Htotf Htotg Hfunf Hfung HxA).
We prove the intermediate claim Hfx: apply_fun f x ∈ V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HfxV.
We prove the intermediate claim HxPre: x ∈ preimage_of A f V.
An exact proof term for the current goal is (SepI A (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxA Hfx).
An exact proof term for the current goal is (binunionI1 (preimage_of A f V) (preimage_of B g V) x HxPre).
Assume HxB: x ∈ B.
We prove the intermediate claim Happ: apply_fun (f ∪ g) x = apply_fun g x.
An exact proof term for the current goal is (apply_fun_union_right A B Y f g x Hdisj Hdomf Hdomg Htotf Htotg Hfunf Hfung HxB).
We prove the intermediate claim Hgx: apply_fun g x ∈ V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HfxV.
We prove the intermediate claim HxPre: x ∈ preimage_of B g V.
An exact proof term for the current goal is (SepI B (λx0 : set ⇒ apply_fun g x0 ∈ V) x HxB Hgx).
An exact proof term for the current goal is (binunionI2 (preimage_of A f V) (preimage_of B g V) x HxPre).
Let x be given.
Assume Hx: x ∈ (preimage_of A f V) ∪ (preimage_of B g V).
We will prove x ∈ preimage_of (A ∪ B) (f ∪ g) V.
Apply (binunionE (preimage_of A f V) (preimage_of B g V) x Hx) to the current goal.
Assume HxPreA: x ∈ preimage_of A f V.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (SepE1 A (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPreA).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 A (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPreA).
We prove the intermediate claim HxAB: x ∈ A ∪ B.
An exact proof term for the current goal is (binunionI1 A B x HxA).
We prove the intermediate claim Happ: apply_fun (f ∪ g) x = apply_fun f x.
An exact proof term for the current goal is (apply_fun_union_left A B Y f g x Hdisj Hdomf Hdomg Htotf Htotg Hfunf Hfung HxA).
We prove the intermediate claim HfgV: apply_fun (f ∪ g) x ∈ V.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HfxV.
An exact proof term for the current goal is (SepI (A ∪ B) (λx0 : set ⇒ apply_fun (f ∪ g) x0 ∈ V) x HxAB HfgV).
Assume HxPreB: x ∈ preimage_of B g V.
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (SepE1 B (λx0 : set ⇒ apply_fun g x0 ∈ V) x HxPreB).
We prove the intermediate claim HgxV: apply_fun g x ∈ V.
An exact proof term for the current goal is (SepE2 B (λx0 : set ⇒ apply_fun g x0 ∈ V) x HxPreB).
We prove the intermediate claim HxAB: x ∈ A ∪ B.
An exact proof term for the current goal is (binunionI2 A B x HxB).
We prove the intermediate claim Happ: apply_fun (f ∪ g) x = apply_fun g x.
An exact proof term for the current goal is (apply_fun_union_right A B Y f g x Hdisj Hdomf Hdomg Htotf Htotg Hfunf Hfung HxB).
We prove the intermediate claim HfgV: apply_fun (f ∪ g) x ∈ V.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HgxV.
An exact proof term for the current goal is (SepI (A ∪ B) (λx0 : set ⇒ apply_fun (f ∪ g) x0 ∈ V) x HxAB HfgV).
∎