Let I, Xi, x1 and x2 be given.
Assume Hx1: x1 ∈ product_space I Xi.
Assume Hx2: x2 ∈ product_space I Xi.
Assume Hneq: x1 ≠ x2.
Apply (xm (∃i : set, i ∈ I ∧ apply_fun x1 i ≠ apply_fun x2 i)) to the current goal.
Assume Hex.
An exact proof term for the current goal is Hex.
Assume Hno: ¬ (∃i : set, i ∈ I ∧ apply_fun x1 i ≠ apply_fun x2 i).
Apply FalseE to the current goal.
Set Y to be the term space_family_union I Xi.
We prove the intermediate claim Hx1Pow: x1 ∈ 𝒫 (setprod I Y).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod I Y)) (λf : set ⇒ total_function_on f I Y ∧ functional_graph f ∧ ∀i : set, i ∈ I → apply_fun f i ∈ space_family_set Xi i) x1 Hx1).
We prove the intermediate claim Hx2Pow: x2 ∈ 𝒫 (setprod I Y).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod I Y)) (λf : set ⇒ total_function_on f I Y ∧ functional_graph f ∧ ∀i : set, i ∈ I → apply_fun f i ∈ space_family_set Xi i) x2 Hx2).
We prove the intermediate claim Hx1sub: x1 ⊆ setprod I Y.
An exact proof term for the current goal is (PowerE (setprod I Y) x1 Hx1Pow).
We prove the intermediate claim Hx2sub: x2 ⊆ setprod I Y.
An exact proof term for the current goal is (PowerE (setprod I Y) x2 Hx2Pow).
We prove the intermediate claim Hx1prop: total_function_on x1 I Y ∧ functional_graph x1 ∧ ∀i : set, i ∈ I → apply_fun x1 i ∈ space_family_set Xi i.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod I Y)) (λf : set ⇒ total_function_on f I Y ∧ functional_graph f ∧ ∀i : set, i ∈ I → apply_fun f i ∈ space_family_set Xi i) x1 Hx1).
We prove the intermediate claim Hx2prop: total_function_on x2 I Y ∧ functional_graph x2 ∧ ∀i : set, i ∈ I → apply_fun x2 i ∈ space_family_set Xi i.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod I Y)) (λf : set ⇒ total_function_on f I Y ∧ functional_graph f ∧ ∀i : set, i ∈ I → apply_fun f i ∈ space_family_set Xi i) x2 Hx2).
We prove the intermediate claim Hx1pair: total_function_on x1 I Y ∧ functional_graph x1.
An exact proof term for the current goal is (andEL (total_function_on x1 I Y ∧ functional_graph x1) (∀i : set, i ∈ I → apply_fun x1 i ∈ space_family_set Xi i) Hx1prop).
We prove the intermediate claim Hx2pair: total_function_on x2 I Y ∧ functional_graph x2.
An exact proof term for the current goal is (andEL (total_function_on x2 I Y ∧ functional_graph x2) (∀i : set, i ∈ I → apply_fun x2 i ∈ space_family_set Xi i) Hx2prop).
We prove the intermediate claim Htot1: total_function_on x1 I Y.
An exact proof term for the current goal is (andEL (total_function_on x1 I Y) (functional_graph x1) Hx1pair).
We prove the intermediate claim Htot2: total_function_on x2 I Y.
An exact proof term for the current goal is (andEL (total_function_on x2 I Y) (functional_graph x2) Hx2pair).
We prove the intermediate claim Hfun1: functional_graph x1.
An exact proof term for the current goal is (andER (total_function_on x1 I Y) (functional_graph x1) Hx1pair).
We prove the intermediate claim Hfun2: functional_graph x2.
An exact proof term for the current goal is (andER (total_function_on x2 I Y) (functional_graph x2) Hx2pair).
We prove the intermediate claim Hall: ∀i : set, i ∈ I → apply_fun x1 i = apply_fun x2 i.
Let i be given.
Assume HiI: i ∈ I.
Apply (xm (apply_fun x1 i = apply_fun x2 i)) to the current goal.
Assume Heq.
An exact proof term for the current goal is Heq.
Assume Hdiff: apply_fun x1 i ≠ apply_fun x2 i.
Apply FalseE to the current goal.
Apply Hno to the current goal.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HiI.
An exact proof term for the current goal is Hdiff.
We prove the intermediate claim Hsub12: x1 ⊆ x2.
Let p be given.
Assume HpIn1: p ∈ x1.
We will prove p ∈ x2.
We prove the intermediate claim HpX: p ∈ setprod I Y.
An exact proof term for the current goal is (Hx1sub p HpIn1).
Apply (setprod_elem_decompose I Y p HpX) to the current goal.
Let i be given.
Assume Hiconj.
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (andEL (i ∈ I) (∃y ∈ Y, p ∈ setprod {i} {y}) Hiconj).
Apply (andER (i ∈ I) (∃y ∈ Y, p ∈ setprod {i} {y}) Hiconj) to the current goal.
Let y be given.
Assume Hyconj.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (andEL (y ∈ Y) (p ∈ setprod {i} {y}) Hyconj).
We prove the intermediate claim Hpiy: p ∈ setprod {i} {y}.
An exact proof term for the current goal is (andER (y ∈ Y) (p ∈ setprod {i} {y}) Hyconj).
We prove the intermediate claim Hp0: p 0 ∈ {i}.
An exact proof term for the current goal is (ap0_Sigma {i} (λ_ : set ⇒ {y}) p Hpiy).
We prove the intermediate claim Hp1sing: p 1 ∈ {y}.
An exact proof term for the current goal is (ap1_Sigma {i} (λ_ : set ⇒ {y}) p Hpiy).
We prove the intermediate claim Hp0eq: p 0 = i.
An exact proof term for the current goal is (singleton_elem (p 0) i Hp0).
We prove the intermediate claim Hp1eq: p 1 = y.
An exact proof term for the current goal is (singleton_elem (p 1) y Hp1sing).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta {i} {y} p Hpiy).
We prove the intermediate claim HpEq: p = (i,y).
rewrite the current goal using Heta (from left to right).
rewrite the current goal using Hp0eq (from left to right).
rewrite the current goal using Hp1eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hpair1: (i,y) ∈ x1.
We will prove (i,y) ∈ x1.
rewrite the current goal using HpEq (from right to left) at position 1.
An exact proof term for the current goal is HpIn1.
We prove the intermediate claim Happ1: apply_fun x1 i = y.
An exact proof term for the current goal is (functional_graph_apply_fun_eq x1 i y Hfun1 Hpair1).
We prove the intermediate claim Happ2: apply_fun x2 i = y.
rewrite the current goal using (Hall i HiI) (from right to left).
An exact proof term for the current goal is Happ1.
We prove the intermediate claim Hpair2: (i,apply_fun x2 i) ∈ x2.
An exact proof term for the current goal is (total_function_on_apply_fun_in_graph x2 I Y i Htot2 HiI).
We prove the intermediate claim Hiy2: (i,y) ∈ x2.
We will prove (i,y) ∈ x2.
rewrite the current goal using Happ2 (from right to left) at position 1.
An exact proof term for the current goal is Hpair2.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is Hiy2.
We prove the intermediate claim Hsub21: x2 ⊆ x1.
Let p be given.
Assume HpIn2: p ∈ x2.
We will prove p ∈ x1.
We prove the intermediate claim HpX: p ∈ setprod I Y.
An exact proof term for the current goal is (Hx2sub p HpIn2).
Apply (setprod_elem_decompose I Y p HpX) to the current goal.
Let i be given.
Assume Hiconj.
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (andEL (i ∈ I) (∃y ∈ Y, p ∈ setprod {i} {y}) Hiconj).
Apply (andER (i ∈ I) (∃y ∈ Y, p ∈ setprod {i} {y}) Hiconj) to the current goal.
Let y be given.
Assume Hyconj.
We prove the intermediate claim Hpiy: p ∈ setprod {i} {y}.
An exact proof term for the current goal is (andER (y ∈ Y) (p ∈ setprod {i} {y}) Hyconj).
We prove the intermediate claim Hp0: p 0 ∈ {i}.
An exact proof term for the current goal is (ap0_Sigma {i} (λ_ : set ⇒ {y}) p Hpiy).
We prove the intermediate claim Hp1sing: p 1 ∈ {y}.
An exact proof term for the current goal is (ap1_Sigma {i} (λ_ : set ⇒ {y}) p Hpiy).
We prove the intermediate claim Hp0eq: p 0 = i.
An exact proof term for the current goal is (singleton_elem (p 0) i Hp0).
We prove the intermediate claim Hp1eq: p 1 = y.
An exact proof term for the current goal is (singleton_elem (p 1) y Hp1sing).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta {i} {y} p Hpiy).
We prove the intermediate claim HpEq: p = (i,y).
rewrite the current goal using Heta (from left to right).
rewrite the current goal using Hp0eq (from left to right).
rewrite the current goal using Hp1eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hpair2: (i,y) ∈ x2.
We will prove (i,y) ∈ x2.
rewrite the current goal using HpEq (from right to left) at position 1.
An exact proof term for the current goal is HpIn2.
We prove the intermediate claim Happ2: apply_fun x2 i = y.
An exact proof term for the current goal is (functional_graph_apply_fun_eq x2 i y Hfun2 Hpair2).
We prove the intermediate claim Happ1: apply_fun x1 i = y.
rewrite the current goal using (Hall i HiI) (from left to right) at position 1.
An exact proof term for the current goal is Happ2.
We prove the intermediate claim Hpair1: (i,apply_fun x1 i) ∈ x1.
An exact proof term for the current goal is (total_function_on_apply_fun_in_graph x1 I Y i Htot1 HiI).
We prove the intermediate claim Hiy1: (i,y) ∈ x1.
We will prove (i,y) ∈ x1.
rewrite the current goal using Happ1 (from right to left) at position 1.
An exact proof term for the current goal is Hpair1.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is Hiy1.
We prove the intermediate claim Heq: x1 = x2.
Apply set_ext to the current goal.
An exact proof term for the current goal is Hsub12.
An exact proof term for the current goal is Hsub21.
An exact proof term for the current goal is (Hneq Heq).
∎