Let I and Xi be given.
Assume HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Set X to be the term product_space I Xi.
Set B to be the term box_basis I Xi.
We will prove basis_on X B.
We will prove (B ⊆ đ’Ģ X ∧ (∀x ∈ X, ∃b ∈ B, x ∈ b)) ∧ (∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∊ b2).
Apply andI to the current goal.
Apply andI to the current goal.
Let b be given.
Assume Hb: b ∈ B.
We will prove b ∈ đ’Ģ X.
An exact proof term for the current goal is (SepE1 (đ’Ģ X) (Îģb0 : set ⇒ ∃U : set, total_function_on U I (topology_family_union I Xi) ∧ functional_graph U ∧ (∀i : set, i ∈ I → apply_fun U i ∈ space_family_topology Xi i) ∧ b0 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U i}) b Hb).
Let x be given.
Assume Hx: x ∈ X.
We will prove ∃b ∈ B, x ∈ b.
We use X to witness the existential quantifier.
Apply andI to the current goal.
We will prove X ∈ {b0 ∈ đ’Ģ X|∃U : set, total_function_on U I (topology_family_union I Xi) ∧ functional_graph U ∧ (∀i : set, i ∈ I → apply_fun U i ∈ space_family_topology Xi i) ∧ b0 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U i}}.
Apply SepI to the current goal.
An exact proof term for the current goal is (Self_In_Power X).
We prove the intermediate claim HexU: ∃U : set, total_function_on U I (topology_family_union I Xi) ∧ functional_graph U ∧ (∀i : set, i ∈ I → apply_fun U i ∈ space_family_topology Xi i) ∧ X = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U i}.
Set U0 to be the term graph I (Îģi : set ⇒ space_family_set Xi i).
We use U0 to witness the existential quantifier.
We will prove total_function_on U0 I (topology_family_union I Xi) ∧ functional_graph U0 ∧ (∀i : set, i ∈ I → apply_fun U0 i ∈ space_family_topology Xi i) ∧ X = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U0 i}.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply (total_function_on_graph I (topology_family_union I Xi) (Îģi : set ⇒ space_family_set Xi i)) to the current goal.
Let i be given.
Assume Hi: i ∈ I.
We will prove space_family_set Xi i ∈ topology_family_union I Xi.
Set S to be the term {space_family_topology Xi j|j ∈ I}.
We prove the intermediate claim HdefU: topology_family_union I Xi = ⋃ S.
Use reflexivity.
rewrite the current goal using HdefU (from left to right).
We prove the intermediate claim HiS: space_family_topology Xi i ∈ S.
An exact proof term for the current goal is (ReplI I (Îģj : set ⇒ space_family_topology Xi j) i Hi).
We prove the intermediate claim Hwhole: space_family_set Xi i ∈ space_family_topology Xi i.
We prove the intermediate claim HTi: topology_on (space_family_set Xi i) (space_family_topology Xi i).
An exact proof term for the current goal is (HcompTop i Hi).
An exact proof term for the current goal is (topology_has_X (space_family_set Xi i) (space_family_topology Xi i) HTi).
An exact proof term for the current goal is (UnionI S (space_family_set Xi i) (space_family_topology Xi i) Hwhole HiS).
An exact proof term for the current goal is (functional_graph_graph I (Îģi : set ⇒ space_family_set Xi i)).
Let i be given.
Assume Hi: i ∈ I.
We will prove apply_fun U0 i ∈ space_family_topology Xi i.
We prove the intermediate claim HUi: apply_fun U0 i = space_family_set Xi i.
An exact proof term for the current goal is (apply_fun_graph I (Îģj : set ⇒ space_family_set Xi j) i Hi).
rewrite the current goal using HUi (from left to right).
We prove the intermediate claim HTi: topology_on (space_family_set Xi i) (space_family_topology Xi i).
An exact proof term for the current goal is (HcompTop i Hi).
An exact proof term for the current goal is (topology_has_X (space_family_set Xi i) (space_family_topology Xi i) HTi).
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ X.
We will prove f ∈ {f0 ∈ X|∀i : set, i ∈ I → apply_fun f0 i ∈ apply_fun U0 i}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hf.
Let i be given.
Assume Hi: i ∈ I.
We will prove apply_fun f i ∈ apply_fun U0 i.
We prove the intermediate claim HUi: apply_fun U0 i = space_family_set Xi i.
An exact proof term for the current goal is (apply_fun_graph I (Îģj : set ⇒ space_family_set Xi j) i Hi).
rewrite the current goal using HUi (from left to right).
We prove the intermediate claim Hfprop: (total_function_on f I (space_family_union I Xi) ∧ functional_graph f) ∧ ∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j.
An exact proof term for the current goal is (SepE2 (đ’Ģ (setprod I (space_family_union I Xi))) (Îģf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀j : set, j ∈ I → apply_fun f0 j ∈ space_family_set Xi j) f Hf).
We prove the intermediate claim Hcoords: ∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j.
An exact proof term for the current goal is (andER (total_function_on f I (space_family_union I Xi) ∧ functional_graph f) (∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j) Hfprop).
An exact proof term for the current goal is (Hcoords i Hi).
Let f be given.
Assume Hf: f ∈ {f0 ∈ X|∀i : set, i ∈ I → apply_fun f0 i ∈ apply_fun U0 i}.
We will prove f ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģf0 : set ⇒ ∀i : set, i ∈ I → apply_fun f0 i ∈ apply_fun U0 i) f Hf).
An exact proof term for the current goal is HexU.
An exact proof term for the current goal is Hx.
Let b1 be given.
Assume Hb1: b1 ∈ B.
Let b2 be given.
Assume Hb2: b2 ∈ B.
Let x be given.
Assume Hxb1: x ∈ b1.
Assume Hxb2: x ∈ b2.
We will prove ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
We prove the intermediate claim Hex1: ∃U1 : set, total_function_on U1 I (topology_family_union I Xi) ∧ functional_graph U1 ∧ (∀i : set, i ∈ I → apply_fun U1 i ∈ space_family_topology Xi i) ∧ b1 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U1 i}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (Îģb0 : set ⇒ ∃U : set, total_function_on U I (topology_family_union I Xi) ∧ functional_graph U ∧ (∀i : set, i ∈ I → apply_fun U i ∈ space_family_topology Xi i) ∧ b0 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U i}) b1 Hb1).
We prove the intermediate claim Hex2: ∃U2 : set, total_function_on U2 I (topology_family_union I Xi) ∧ functional_graph U2 ∧ (∀i : set, i ∈ I → apply_fun U2 i ∈ space_family_topology Xi i) ∧ b2 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U2 i}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (Îģb0 : set ⇒ ∃U : set, total_function_on U I (topology_family_union I Xi) ∧ functional_graph U ∧ (∀i : set, i ∈ I → apply_fun U i ∈ space_family_topology Xi i) ∧ b0 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U i}) b2 Hb2).
Apply Hex1 to the current goal.
Let U1 be given.
Assume HU1core.
Apply Hex2 to the current goal.
Let U2 be given.
Assume HU2core.
We prove the intermediate claim HU1top: ∀i : set, i ∈ I → apply_fun U1 i ∈ space_family_topology Xi i.
We prove the intermediate claim HU1left: (total_function_on U1 I (topology_family_union I Xi) ∧ functional_graph U1) ∧ (∀i : set, i ∈ I → apply_fun U1 i ∈ space_family_topology Xi i).
An exact proof term for the current goal is (andEL (((total_function_on U1 I (topology_family_union I Xi) ∧ functional_graph U1) ∧ (∀i : set, i ∈ I → apply_fun U1 i ∈ space_family_topology Xi i))) (b1 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U1 i}) HU1core).
An exact proof term for the current goal is (andER (total_function_on U1 I (topology_family_union I Xi) ∧ functional_graph U1) (∀i : set, i ∈ I → apply_fun U1 i ∈ space_family_topology Xi i) HU1left).
We prove the intermediate claim Hb1eq: b1 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U1 i}.
An exact proof term for the current goal is (andER (((total_function_on U1 I (topology_family_union I Xi) ∧ functional_graph U1) ∧ (∀i : set, i ∈ I → apply_fun U1 i ∈ space_family_topology Xi i))) (b1 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U1 i}) HU1core).
We prove the intermediate claim HU2top: ∀i : set, i ∈ I → apply_fun U2 i ∈ space_family_topology Xi i.
We prove the intermediate claim HU2left: (total_function_on U2 I (topology_family_union I Xi) ∧ functional_graph U2) ∧ (∀i : set, i ∈ I → apply_fun U2 i ∈ space_family_topology Xi i).
An exact proof term for the current goal is (andEL (((total_function_on U2 I (topology_family_union I Xi) ∧ functional_graph U2) ∧ (∀i : set, i ∈ I → apply_fun U2 i ∈ space_family_topology Xi i))) (b2 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U2 i}) HU2core).
An exact proof term for the current goal is (andER (total_function_on U2 I (topology_family_union I Xi) ∧ functional_graph U2) (∀i : set, i ∈ I → apply_fun U2 i ∈ space_family_topology Xi i) HU2left).
We prove the intermediate claim Hb2eq: b2 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U2 i}.
An exact proof term for the current goal is (andER (((total_function_on U2 I (topology_family_union I Xi) ∧ functional_graph U2) ∧ (∀i : set, i ∈ I → apply_fun U2 i ∈ space_family_topology Xi i))) (b2 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U2 i}) HU2core).
Set U3 to be the term graph I (Îģi : set ⇒ (apply_fun U1 i) ∊ (apply_fun U2 i)).
Set b3 to be the term {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U3 i}.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HBdef: B = {B0 ∈ đ’Ģ X|∃U : set, total_function_on U I (topology_family_union I Xi) ∧ functional_graph U ∧ (∀i : set, i ∈ I → apply_fun U i ∈ space_family_topology Xi i) ∧ B0 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U i}}.
Use reflexivity.
rewrite the current goal using HBdef (from left to right).
Apply SepI to the current goal.
Apply PowerI to the current goal.
Let f be given.
Assume Hf: f ∈ b3.
We will prove f ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģf0 : set ⇒ ∀i : set, i ∈ I → apply_fun f0 i ∈ apply_fun U3 i) f Hf).
We prove the intermediate claim HexU3: ∃U : set, total_function_on U I (topology_family_union I Xi) ∧ functional_graph U ∧ (∀i : set, i ∈ I → apply_fun U i ∈ space_family_topology Xi i) ∧ b3 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U i}.
We use U3 to witness the existential quantifier.
We will prove total_function_on U3 I (topology_family_union I Xi) ∧ functional_graph U3 ∧ (∀i : set, i ∈ I → apply_fun U3 i ∈ space_family_topology Xi i) ∧ b3 = {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U3 i}.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply (total_function_on_graph I (topology_family_union I Xi) (Îģi : set ⇒ (apply_fun U1 i) ∊ (apply_fun U2 i))) to the current goal.
Let i be given.
Assume Hi: i ∈ I.
We will prove (apply_fun U1 i ∊ apply_fun U2 i) ∈ topology_family_union I Xi.
Set S to be the term {space_family_topology Xi j|j ∈ I}.
We prove the intermediate claim HdefU: topology_family_union I Xi = ⋃ S.
Use reflexivity.
rewrite the current goal using HdefU (from left to right).
We prove the intermediate claim HiS: space_family_topology Xi i ∈ S.
An exact proof term for the current goal is (ReplI I (Îģj : set ⇒ space_family_topology Xi j) i Hi).
We prove the intermediate claim HTi: topology_on (space_family_set Xi i) (space_family_topology Xi i).
An exact proof term for the current goal is (HcompTop i Hi).
We prove the intermediate claim HU1i: apply_fun U1 i ∈ space_family_topology Xi i.
An exact proof term for the current goal is (HU1top i Hi).
We prove the intermediate claim HU2i: apply_fun U2 i ∈ space_family_topology Xi i.
An exact proof term for the current goal is (HU2top i Hi).
We prove the intermediate claim Hinter: (apply_fun U1 i ∊ apply_fun U2 i) ∈ space_family_topology Xi i.
An exact proof term for the current goal is (topology_binintersect_closed (space_family_set Xi i) (space_family_topology Xi i) (apply_fun U1 i) (apply_fun U2 i) HTi HU1i HU2i).
An exact proof term for the current goal is (UnionI S (apply_fun U1 i ∊ apply_fun U2 i) (space_family_topology Xi i) Hinter HiS).
An exact proof term for the current goal is (functional_graph_graph I (Îģi : set ⇒ (apply_fun U1 i) ∊ (apply_fun U2 i))).
Let i be given.
Assume Hi: i ∈ I.
We will prove apply_fun U3 i ∈ space_family_topology Xi i.
We prove the intermediate claim HTi: topology_on (space_family_set Xi i) (space_family_topology Xi i).
An exact proof term for the current goal is (HcompTop i Hi).
We prove the intermediate claim HU1i: apply_fun U1 i ∈ space_family_topology Xi i.
An exact proof term for the current goal is (HU1top i Hi).
We prove the intermediate claim HU2i: apply_fun U2 i ∈ space_family_topology Xi i.
An exact proof term for the current goal is (HU2top i Hi).
We prove the intermediate claim HUi: apply_fun U3 i = (apply_fun U1 i ∊ apply_fun U2 i).
An exact proof term for the current goal is (apply_fun_graph I (Îģj : set ⇒ (apply_fun U1 j) ∊ (apply_fun U2 j)) i Hi).
rewrite the current goal using HUi (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed (space_family_set Xi i) (space_family_topology Xi i) (apply_fun U1 i) (apply_fun U2 i) HTi HU1i HU2i).
Use reflexivity.
An exact proof term for the current goal is HexU3.
Apply andI to the current goal.
We will prove x ∈ {f ∈ X|∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U3 i}.
Apply SepI to the current goal.
We prove the intermediate claim HxInB1: x ∈ {f ∈ X|∀j : set, j ∈ I → apply_fun f j ∈ apply_fun U1 j}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hxb1.
An exact proof term for the current goal is (SepE1 X (Îģf0 : set ⇒ ∀j : set, j ∈ I → apply_fun f0 j ∈ apply_fun U1 j) x HxInB1).
Let i be given.
Assume Hi: i ∈ I.
We will prove apply_fun x i ∈ apply_fun U3 i.
We prove the intermediate claim HxU1: ∀j : set, j ∈ I → apply_fun x j ∈ apply_fun U1 j.
We prove the intermediate claim HxInB1: x ∈ {f ∈ X|∀j : set, j ∈ I → apply_fun f j ∈ apply_fun U1 j}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hxb1.
An exact proof term for the current goal is (SepE2 X (Îģf0 : set ⇒ ∀j : set, j ∈ I → apply_fun f0 j ∈ apply_fun U1 j) x HxInB1).
We prove the intermediate claim HxU2: ∀j : set, j ∈ I → apply_fun x j ∈ apply_fun U2 j.
We prove the intermediate claim HxInB2: x ∈ {f ∈ X|∀j : set, j ∈ I → apply_fun f j ∈ apply_fun U2 j}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hxb2.
An exact proof term for the current goal is (SepE2 X (Îģf0 : set ⇒ ∀j : set, j ∈ I → apply_fun f0 j ∈ apply_fun U2 j) x HxInB2).
We prove the intermediate claim HUi: apply_fun U3 i = (apply_fun U1 i ∊ apply_fun U2 i).
An exact proof term for the current goal is (apply_fun_graph I (Îģj : set ⇒ (apply_fun U1 j) ∊ (apply_fun U2 j)) i Hi).
rewrite the current goal using HUi (from left to right).
An exact proof term for the current goal is (binintersectI (apply_fun U1 i) (apply_fun U2 i) (apply_fun x i) (HxU1 i Hi) (HxU2 i Hi)).
Let f be given.
Assume Hf: f ∈ b3.
We will prove f ∈ b1 ∊ b2.
We prove the intermediate claim HfX: f ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģf0 : set ⇒ ∀i : set, i ∈ I → apply_fun f0 i ∈ apply_fun U3 i) f Hf).
We prove the intermediate claim HfU3: ∀i : set, i ∈ I → apply_fun f i ∈ apply_fun U3 i.
An exact proof term for the current goal is (SepE2 X (Îģf0 : set ⇒ ∀i : set, i ∈ I → apply_fun f0 i ∈ apply_fun U3 i) f Hf).
We prove the intermediate claim HfB1: f ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HfX.
Let i be given.
Assume Hi: i ∈ I.
We will prove apply_fun f i ∈ apply_fun U1 i.
We prove the intermediate claim HUi: apply_fun U3 i = (apply_fun U1 i ∊ apply_fun U2 i).
An exact proof term for the current goal is (apply_fun_graph I (Îģj : set ⇒ (apply_fun U1 j) ∊ (apply_fun U2 j)) i Hi).
We prove the intermediate claim Hfin: apply_fun f i ∈ apply_fun U1 i ∊ apply_fun U2 i.
rewrite the current goal using HUi (from right to left).
An exact proof term for the current goal is (HfU3 i Hi).
An exact proof term for the current goal is (binintersectE1 (apply_fun U1 i) (apply_fun U2 i) (apply_fun f i) Hfin).
We prove the intermediate claim HfB2: f ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HfX.
Let i be given.
Assume Hi: i ∈ I.
We will prove apply_fun f i ∈ apply_fun U2 i.
We prove the intermediate claim HUi: apply_fun U3 i = (apply_fun U1 i ∊ apply_fun U2 i).
An exact proof term for the current goal is (apply_fun_graph I (Îģj : set ⇒ (apply_fun U1 j) ∊ (apply_fun U2 j)) i Hi).
We prove the intermediate claim Hfin: apply_fun f i ∈ apply_fun U1 i ∊ apply_fun U2 i.
rewrite the current goal using HUi (from right to left).
An exact proof term for the current goal is (HfU3 i Hi).
An exact proof term for the current goal is (binintersectE2 (apply_fun U1 i) (apply_fun U2 i) (apply_fun f i) Hfin).
An exact proof term for the current goal is (binintersectI b1 b2 f HfB1 HfB2).
∎