Let J and g be given.
Assume Hg: ∀j : set, j ∈ J → g j ∈ R.
Set Xi to be the term const_space_family J R R_standard_topology.
We will prove graph J g ∈ product_space J Xi.
We prove the intermediate claim Hdef: product_space J Xi = {f ∈ 𝒫 (setprod J (space_family_union J Xi))|total_function_on f J (space_family_union J Xi) ∧ functional_graph f ∧ ∀i0 : set, i0 ∈ J → apply_fun f i0 ∈ space_family_set Xi i0}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply SepI to the current goal.
Apply (PowerI (setprod J (space_family_union J Xi)) (graph J g)) to the current goal.
Let p be given.
Assume Hp: p ∈ graph J g.
We will prove p ∈ setprod J (space_family_union J Xi).
Apply (ReplE_impred J (λj0 : set ⇒ (j0,g j0)) p Hp (p ∈ setprod J (space_family_union J Xi))) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Hpeq: p = (j,g j).
rewrite the current goal using Hpeq (from left to right).
We prove the intermediate claim HgjR: g j ∈ R.
An exact proof term for the current goal is (Hg j HjJ).
We prove the intermediate claim HgjInUnion: g j ∈ space_family_union J Xi.
Set Sj to be the term space_family_set Xi j.
We prove the intermediate claim HSjFam: Sj ∈ {space_family_set Xi i|i ∈ J}.
An exact proof term for the current goal is (ReplI J (λi0 : set ⇒ space_family_set Xi i0) j HjJ).
We prove the intermediate claim HSjEq: Sj = R.
rewrite the current goal using (space_family_set_const_space_family J R R_standard_topology j HjJ) (from left to right).
Use reflexivity.
We prove the intermediate claim HgjSj: g j ∈ Sj.
rewrite the current goal using HSjEq (from left to right).
An exact proof term for the current goal is HgjR.
An exact proof term for the current goal is (UnionI {space_family_set Xi i|i ∈ J} (g j) Sj HgjSj HSjFam).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J (space_family_union J Xi) j (g j) HjJ HgjInUnion).
We will prove total_function_on (graph J g) J (space_family_union J Xi) ∧ functional_graph (graph J g) ∧ ∀i0 : set, i0 ∈ J → apply_fun (graph J g) i0 ∈ space_family_set Xi i0.
Apply andI to the current goal.
Apply andI to the current goal.
Apply (total_function_on_graph J (space_family_union J Xi) g) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
We prove the intermediate claim HgjR: g j ∈ R.
An exact proof term for the current goal is (Hg j HjJ).
Set Sj to be the term space_family_set Xi j.
We prove the intermediate claim HSjFam: Sj ∈ {space_family_set Xi i|i ∈ J}.
An exact proof term for the current goal is (ReplI J (λi0 : set ⇒ space_family_set Xi i0) j HjJ).
We prove the intermediate claim HSjEq: Sj = R.
rewrite the current goal using (space_family_set_const_space_family J R R_standard_topology j HjJ) (from left to right).
Use reflexivity.
We prove the intermediate claim HgjSj: g j ∈ Sj.
rewrite the current goal using HSjEq (from left to right).
An exact proof term for the current goal is HgjR.
An exact proof term for the current goal is (UnionI {space_family_set Xi i|i ∈ J} (g j) Sj HgjSj HSjFam).
An exact proof term for the current goal is (functional_graph_graph J g).
Let j be given.
Assume HjJ: j ∈ J.
We will prove apply_fun (graph J g) j ∈ space_family_set Xi j.
rewrite the current goal using (apply_fun_graph J g j HjJ) (from left to right).
rewrite the current goal using (space_family_set_const_space_family J R R_standard_topology j HjJ) (from left to right).
An exact proof term for the current goal is (Hg j HjJ).
∎