Let g be given.
Assume HgR: ∀i : set, g i ∈ R.
Set Xi to be the term const_space_family 3 R R_standard_topology.
Set U to be the term space_family_union 3 Xi.
We will prove graph 3 g ∈ {f ∈ đ’Ģ (setprod 3 U)|total_function_on f 3 U ∧ functional_graph f ∧ (∀i : set, i ∈ 3 → apply_fun f i ∈ space_family_set Xi i)}.
We prove the intermediate claim Hsub: graph 3 g ⊆ setprod 3 U.
Let p be given.
Assume Hp: p ∈ graph 3 g.
We will prove p ∈ setprod 3 U.
Apply (ReplE_impred 3 (Îģi : set ⇒ (i,g i)) p Hp (p ∈ setprod 3 U)) to the current goal.
Let i be given.
Assume Hi3: i ∈ 3.
Assume HpEq: p = (i,g i).
rewrite the current goal using HpEq (from left to right).
We prove the intermediate claim HgiU: g i ∈ U.
An exact proof term for the current goal is (real_in_space_family_union_R3 (g i) (HgR i)).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 3 U i (g i) Hi3 HgiU).
We prove the intermediate claim Hpow: graph 3 g ∈ đ’Ģ (setprod 3 U).
An exact proof term for the current goal is (PowerI (setprod 3 U) (graph 3 g) Hsub).
We prove the intermediate claim Hfun: function_on (graph 3 g) 3 U.
Let i be given.
Assume Hi3: i ∈ 3.
We will prove apply_fun (graph 3 g) i ∈ U.
We prove the intermediate claim Happ: apply_fun (graph 3 g) i = g i.
An exact proof term for the current goal is (apply_fun_graph 3 g i Hi3).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (real_in_space_family_union_R3 (g i) (HgR i)).
We prove the intermediate claim Hcoords: ∀i : set, i ∈ 3 → apply_fun (graph 3 g) i ∈ space_family_set Xi i.
Let i be given.
Assume Hi3: i ∈ 3.
We will prove apply_fun (graph 3 g) i ∈ space_family_set Xi i.
We prove the intermediate claim Happ: apply_fun (graph 3 g) i = g i.
An exact proof term for the current goal is (apply_fun_graph 3 g i Hi3).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim HSf: space_family_set Xi i = R.
An exact proof term for the current goal is (space_family_set_const_R3 i Hi3).
rewrite the current goal using HSf (from left to right).
An exact proof term for the current goal is (HgR i).
We prove the intermediate claim Htot: total_function_on (graph 3 g) 3 U.
We prove the intermediate claim Htot': ∀i : set, i ∈ 3 → ∃y : set, y ∈ U ∧ (i,y) ∈ graph 3 g.
Let i be given.
Assume Hi3: i ∈ 3.
We use (g i) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (real_in_space_family_union_R3 (g i) (HgR i)).
An exact proof term for the current goal is (ReplI 3 (Îģi0 : set ⇒ (i0,g i0)) i Hi3).
An exact proof term for the current goal is (andI (function_on (graph 3 g) 3 U) (∀x : set, x ∈ 3 → ∃y : set, y ∈ U ∧ (x,y) ∈ graph 3 g) Hfun Htot').
We prove the intermediate claim Hgraph: functional_graph (graph 3 g).
An exact proof term for the current goal is (functional_graph_graph 3 g).
We prove the intermediate claim Hprop: total_function_on (graph 3 g) 3 U ∧ functional_graph (graph 3 g) ∧ (∀i : set, i ∈ 3 → apply_fun (graph 3 g) i ∈ space_family_set Xi i).
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.
An exact proof term for the current goal is Hcoords.
An exact proof term for the current goal is (SepI (đ’Ģ (setprod 3 U)) (Îģf0 : set ⇒ total_function_on f0 3 U ∧ functional_graph f0 ∧ (∀i : set, i ∈ 3 → apply_fun f0 i ∈ space_family_set Xi i)) (graph 3 g) Hpow Hprop).
∎