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 (setminusE1 U V (apply_fun f x) HfxUV).
We prove the intermediate claim HfxnotV: apply_fun f x ∉ V.
An exact proof term for the current goal is (setminusE2 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 HxnotPreV: x ∉ preimage_of X f V.
Assume HxPreV: x ∈ preimage_of X f V.
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).
An exact proof term for the current goal is (HfxnotV HfxV).
An exact proof term for the current goal is (setminusI (preimage_of X f U) (preimage_of X f V) x HxPreU HxnotPreV).
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 (setminusE1 (preimage_of X f U) (preimage_of X f V) x Hx).
We prove the intermediate claim HxnotPreV: x ∉ preimage_of X f V.
An exact proof term for the current goal is (setminusE2 (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 HfxnotV: apply_fun f x ∉ V.
Assume HfxV: apply_fun f x ∈ V.
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 (HxnotPreV HxPreV).
We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∖ V.
An exact proof term for the current goal is (setminusI U V (apply_fun f x) HfxU HfxnotV).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U ∖ V) x HxX HfxUV).
∎