Let Fam and Y be given.
We will prove restrict_family_to_subspace Fam Y ⊆ 𝒫 Y.
Let W be given.
Assume HW: W ∈ restrict_family_to_subspace Fam Y.
Apply (ReplE_impred Fam (λU : set ⇒ U ∩ Y) W HW (W ∈ 𝒫 Y)) to the current goal.
Let U be given.
Assume HUfam: U ∈ Fam.
Assume HWeq: W = U ∩ Y.
We prove the intermediate claim Hsub: U ∩ Y ⊆ Y.
An exact proof term for the current goal is (binintersect_Subq_2 U Y).
We prove the intermediate claim HWpow: U ∩ Y ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y (U ∩ Y) Hsub).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HWpow.
∎