Let J, f and g be given.
Assume Hf: f ∈ power_real J.
Assume Hg: g ∈ power_real J.
Assume Hagree: ∀j : set, j ∈ J → apply_fun f j = apply_fun g j.
Set Xi to be the term const_space_family J R R_standard_topology.
Set Y to be the term space_family_union J Xi.
We prove the intermediate claim HfPow: f ∈ 𝒫 (setprod J Y).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod J Y)) (λf0 : set ⇒ total_function_on f0 J Y ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ J → apply_fun f0 i0 ∈ space_family_set Xi i0) f Hf).
We prove the intermediate claim HgPow: g ∈ 𝒫 (setprod J Y).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod J Y)) (λg0 : set ⇒ total_function_on g0 J Y ∧ functional_graph g0 ∧ ∀i0 : set, i0 ∈ J → apply_fun g0 i0 ∈ space_family_set Xi i0) g Hg).
We prove the intermediate claim HfSub: f ⊆ setprod J Y.
An exact proof term for the current goal is (PowerE (setprod J Y) f HfPow).
We prove the intermediate claim HgSub: g ⊆ setprod J Y.
An exact proof term for the current goal is (PowerE (setprod J Y) g HgPow).
We prove the intermediate claim Hfpred: total_function_on f J Y ∧ functional_graph f ∧ ∀i0 : set, i0 ∈ J → apply_fun f i0 ∈ space_family_set Xi i0.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod J Y)) (λf0 : set ⇒ total_function_on f0 J Y ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ J → apply_fun f0 i0 ∈ space_family_set Xi i0) f Hf).
We prove the intermediate claim Hgpred: total_function_on g J Y ∧ functional_graph g ∧ ∀i0 : set, i0 ∈ J → apply_fun g i0 ∈ space_family_set Xi i0.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod J Y)) (λg0 : set ⇒ total_function_on g0 J Y ∧ functional_graph g0 ∧ ∀i0 : set, i0 ∈ J → apply_fun g0 i0 ∈ space_family_set Xi i0) g Hg).
We prove the intermediate claim Hf12: total_function_on f J Y ∧ functional_graph f.
An exact proof term for the current goal is (andEL (total_function_on f J Y ∧ functional_graph f) (∀i0 : set, i0 ∈ J → apply_fun f i0 ∈ space_family_set Xi i0) Hfpred).
We prove the intermediate claim Hg12: total_function_on g J Y ∧ functional_graph g.
An exact proof term for the current goal is (andEL (total_function_on g J Y ∧ functional_graph g) (∀i0 : set, i0 ∈ J → apply_fun g i0 ∈ space_family_set Xi i0) Hgpred).
We prove the intermediate claim Hftot: total_function_on f J Y.
An exact proof term for the current goal is (andEL (total_function_on f J Y) (functional_graph f) Hf12).
We prove the intermediate claim Hgtot: total_function_on g J Y.
An exact proof term for the current goal is (andEL (total_function_on g J Y) (functional_graph g) Hg12).
We prove the intermediate claim Hffun: functional_graph f.
An exact proof term for the current goal is (andER (total_function_on f J Y) (functional_graph f) Hf12).
We prove the intermediate claim Hgfun: functional_graph g.
An exact proof term for the current goal is (andER (total_function_on g J Y) (functional_graph g) Hg12).
We prove the intermediate claim Hgtot2: ∀j : set, j ∈ J → ∃y : set, y ∈ Y ∧ (j,y) ∈ g.
An exact proof term for the current goal is (andER (function_on g J Y) (∀x : set, x ∈ J → ∃y : set, y ∈ Y ∧ (x,y) ∈ g) Hgtot).
We prove the intermediate claim Hftot2: ∀j : set, j ∈ J → ∃y : set, y ∈ Y ∧ (j,y) ∈ f.
An exact proof term for the current goal is (andER (function_on f J Y) (∀x : set, x ∈ J → ∃y : set, y ∈ Y ∧ (x,y) ∈ f) Hftot).
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ f.
We will prove p ∈ g.
We prove the intermediate claim HpXY: p ∈ setprod J Y.
An exact proof term for the current goal is (HfSub p Hp).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta J Y p HpXY).
We prove the intermediate claim Hp0: p 0 ∈ J.
An exact proof term for the current goal is (ap0_Sigma J (λ_ : set ⇒ Y) p HpXY).
We prove the intermediate claim Hp1: p 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma J (λ_ : set ⇒ Y) p HpXY).
We prove the intermediate claim Hpair: (p 0,p 1) ∈ f.
rewrite the current goal using Heta (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Happf: apply_fun f (p 0) = (p 1).
An exact proof term for the current goal is (functional_graph_apply_fun_eq f (p 0) (p 1) Hffun Hpair).
We prove the intermediate claim Hfg: apply_fun f (p 0) = apply_fun g (p 0).
An exact proof term for the current goal is (Hagree (p 0) Hp0).
We prove the intermediate claim Hgf: apply_fun g (p 0) = apply_fun f (p 0).
Use symmetry.
An exact proof term for the current goal is Hfg.
We prove the intermediate claim Happg: apply_fun g (p 0) = (p 1).
rewrite the current goal using Hgf (from left to right).
An exact proof term for the current goal is Happf.
We prove the intermediate claim Hexg: ∃y : set, (p 0,y) ∈ g.
Apply (Hgtot2 (p 0) Hp0) to the current goal.
Let y be given.
Assume Hy: y ∈ Y ∧ (p 0,y) ∈ g.
We use y to witness the existential quantifier.
An exact proof term for the current goal is (andER (y ∈ Y) ((p 0,y) ∈ g) Hy).
We prove the intermediate claim Hgpair: (p 0,apply_fun g (p 0)) ∈ g.
An exact proof term for the current goal is (apply_fun_in_graph_of_ex g (p 0) Hexg).
We prove the intermediate claim Hpeq: (p 0,apply_fun g (p 0)) = (p 0,p 1).
rewrite the current goal using Happg (from left to right).
Use reflexivity.
rewrite the current goal using Heta (from left to right).
rewrite the current goal using Hpeq (from right to left).
An exact proof term for the current goal is Hgpair.
Let p be given.
Assume Hp: p ∈ g.
We will prove p ∈ f.
We prove the intermediate claim HpXY: p ∈ setprod J Y.
An exact proof term for the current goal is (HgSub p Hp).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta J Y p HpXY).
We prove the intermediate claim Hp0: p 0 ∈ J.
An exact proof term for the current goal is (ap0_Sigma J (λ_ : set ⇒ Y) p HpXY).
We prove the intermediate claim Hp1: p 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma J (λ_ : set ⇒ Y) p HpXY).
We prove the intermediate claim Hpair: (p 0,p 1) ∈ g.
rewrite the current goal using Heta (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Happg: apply_fun g (p 0) = (p 1).
An exact proof term for the current goal is (functional_graph_apply_fun_eq g (p 0) (p 1) Hgfun Hpair).
We prove the intermediate claim Hfg: apply_fun f (p 0) = apply_fun g (p 0).
An exact proof term for the current goal is (Hagree (p 0) Hp0).
We prove the intermediate claim Happf: apply_fun f (p 0) = (p 1).
rewrite the current goal using Hfg (from left to right).
An exact proof term for the current goal is Happg.
We prove the intermediate claim Hexf: ∃y : set, (p 0,y) ∈ f.
Apply (Hftot2 (p 0) Hp0) to the current goal.
Let y be given.
Assume Hy: y ∈ Y ∧ (p 0,y) ∈ f.
We use y to witness the existential quantifier.
An exact proof term for the current goal is (andER (y ∈ Y) ((p 0,y) ∈ f) Hy).
We prove the intermediate claim Hfpair: (p 0,apply_fun f (p 0)) ∈ f.
An exact proof term for the current goal is (apply_fun_in_graph_of_ex f (p 0) Hexf).
We prove the intermediate claim Hpeq: (p 0,apply_fun f (p 0)) = (p 0,p 1).
rewrite the current goal using Happf (from left to right).
Use reflexivity.
rewrite the current goal using Heta (from left to right).
rewrite the current goal using Hpeq (from right to left).
An exact proof term for the current goal is Hfpair.
∎