Let I, Xi and g be given.
Assume HgXi: ∀i : set, i ∈ I → g i ∈ space_family_set Xi i.
We will prove graph I g ∈ product_space I Xi.
Set Y to be the term space_family_union I Xi.
We prove the intermediate claim HYdef: Y = space_family_union I Xi.
Use reflexivity.
We prove the intermediate claim HgY: ∀i : set, i ∈ I → g i ∈ Y.
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim HgiXi: g i ∈ space_family_set Xi i.
An exact proof term for the current goal is (HgXi i HiI).
We prove the intermediate claim HXiinU: space_family_set Xi i ∈ {space_family_set Xi j|j ∈ I}.
An exact proof term for the current goal is (ReplI I (λj : set ⇒ space_family_set Xi j) i HiI).
We prove the intermediate claim HgiU: g i ∈ ⋃ {space_family_set Xi j|j ∈ I}.
An exact proof term for the current goal is (UnionI {space_family_set Xi j|j ∈ I} (g i) (space_family_set Xi i) HgiXi HXiinU).
We prove the intermediate claim HunionDef: space_family_union I Xi = ⋃ {space_family_set Xi j|j ∈ I}.
Use reflexivity.
rewrite the current goal using HunionDef (from left to right).
An exact proof term for the current goal is HgiU.
We prove the intermediate claim Hsub: graph I g ⊆ setprod I Y.
Let p be given.
Assume Hp: p ∈ graph I g.
We will prove p ∈ setprod I Y.
Apply (ReplE_impred I (λi0 : set ⇒ (i0,g i0)) p Hp (p ∈ setprod I Y)) to the current goal.
Let i be given.
Assume HiI: i ∈ I.
Assume Heq: p = (i,g i).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma I Y i (g i) HiI (HgY i HiI)).
We prove the intermediate claim Hpow: graph I g ∈ 𝒫 (setprod I Y).
An exact proof term for the current goal is (PowerI (setprod I Y) (graph I g) Hsub).
We prove the intermediate claim Htot: total_function_on (graph I g) I Y.
We will prove function_on (graph I g) I Y ∧ ∀i : set, i ∈ I → ∃y : set, y ∈ Y ∧ (i,y) ∈ (graph I g).
Apply andI to the current goal.
We will prove function_on (graph I g) I Y.
Let i be given.
Assume HiI: i ∈ I.
rewrite the current goal using (apply_fun_graph I g i HiI) (from left to right).
An exact proof term for the current goal is (HgY i HiI).
Let i be given.
Assume HiI: i ∈ I.
We use (g i) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HgY i HiI).
An exact proof term for the current goal is (ReplI I (λi0 : set ⇒ (i0,g i0)) i HiI).
We prove the intermediate claim Hgraph: functional_graph (graph I g).
An exact proof term for the current goal is (functional_graph_graph I g).
We prove the intermediate claim HpsDef: product_space I Xi = {f ∈ 𝒫 (setprod I Y)|total_function_on f I Y ∧ functional_graph f ∧ ∀i0 : set, i0 ∈ I → apply_fun f i0 ∈ space_family_set Xi i0}.
rewrite the current goal using HYdef (from left to right).
Use reflexivity.
rewrite the current goal using HpsDef (from left to right).
Apply (SepI (𝒫 (setprod I Y)) (λf0 : set ⇒ total_function_on f0 I Y ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ I → apply_fun f0 i0 ∈ space_family_set Xi i0) (graph I g) Hpow) 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 Htot.
An exact proof term for the current goal is Hgraph.
Let i be given.
Assume HiI: i ∈ I.
rewrite the current goal using (apply_fun_graph I g i HiI) (from left to right).
An exact proof term for the current goal is (HgXi i HiI).
∎