Let X, f, U and V be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f (U ∩ V).
We will prove x ∈ (preimage_of X f U) ∩ (preimage_of X f V).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ U ∩ V) x Hx).
We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∩ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ U ∩ V) x Hx).
We prove the intermediate claim HfxU: apply_fun f x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V (apply_fun f x) HfxUV).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V (apply_fun f x) HfxUV).
We prove the intermediate claim HxPreU: x ∈ preimage_of X f U.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U) x HxX HfxU).
We prove the intermediate claim HxPreV: x ∈ preimage_of X f V.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxX HfxV).
An exact proof term for the current goal is (binintersectI (preimage_of X f U) (preimage_of X f V) x HxPreU HxPreV).
Let x be given.
Assume Hx: x ∈ (preimage_of X f U) ∩ (preimage_of X f V).
We will prove x ∈ preimage_of X f (U ∩ V).
We prove the intermediate claim HxPreU: x ∈ preimage_of X f U.
An exact proof term for the current goal is (binintersectE1 (preimage_of X f U) (preimage_of X f V) x Hx).
We prove the intermediate claim HxPreV: x ∈ preimage_of X f V.
An exact proof term for the current goal is (binintersectE2 (preimage_of X f U) (preimage_of X f V) x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ U) x HxPreU).
We prove the intermediate claim HfxU: apply_fun f x ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ U) x HxPreU).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPreV).
We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V (apply_fun f x) HfxU HfxV).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U ∩ V) x HxX HfxUV).
∎