Assume Hconv: converges_to X (product_topology_full J Xi) seq x.

Let j be given.

Assume Hj: j ∈ J.

Set Xj to be the term product_component Xi j.

Set Tj to be the term product_component_topology Xi j.

Set seqj to be the term product_coordinate_sequence seq j.

We will prove converges_to Xj Tj seqj (apply_fun x j).

We prove the intermediate claim HTj: topology_on Xj Tj.

rewrite the current goal using (product_component_def Xi j) (from left to right).

rewrite the current goal using (product_component_topology_def Xi j) (from left to right).

rewrite the current goal using (const_space_family_apply J R R_standard_topology j Hj) (from left to right).

rewrite the current goal using (tuple_2_0_eq R R_standard_topology) (from left to right).

rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).

An exact proof term for the current goal is R_standard_topology_is_topology.

We prove the intermediate claim Hxprod: x ∈ product_space J Xi.

rewrite the current goal using HX (from right to left).

An exact proof term for the current goal is HxX.

We prove the intermediate claim Hxcoord: apply_fun x j ∈ Xj.

rewrite the current goal using (product_component_def Xi j) (from left to right).

We prove the intermediate claim HxProp: total_function_on x J (space_family_union J Xi) ∧ functional_graph x ∧ ∀i : set, i ∈ J → apply_fun x i ∈ space_family_set Xi i.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod J (space_family_union J Xi))) (λf0 : set ⇒ total_function_on f0 J (space_family_union J Xi) ∧ functional_graph f0 ∧ ∀i : set, i ∈ J → apply_fun f0 i ∈ space_family_set Xi i) x Hxprod).

We prove the intermediate claim HxCoord: ∀i : set, i ∈ J → apply_fun x i ∈ space_family_set Xi i.

An exact proof term for the current goal is (andER (total_function_on x J (space_family_union J Xi) ∧ functional_graph x) (∀i : set, i ∈ J → apply_fun x i ∈ space_family_set Xi i) HxProp).

An exact proof term for the current goal is (HxCoord j Hj).

We prove the intermediate claim Hseqj: sequence_on seqj Xj.

Let n be given.

Assume HnO: n ∈ ω.

We will prove apply_fun seqj n ∈ Xj.

We prove the intermediate claim HseqnX: apply_fun seq n ∈ product_space J Xi.

rewrite the current goal using HX (from right to left).

An exact proof term for the current goal is (Hseq n HnO).

We prove the intermediate claim HseqnProp: total_function_on (apply_fun seq n) J (space_family_union J Xi) ∧ functional_graph (apply_fun seq n) ∧ ∀i : set, i ∈ J → apply_fun (apply_fun seq n) i ∈ space_family_set Xi i.

We prove the intermediate claim HseqnCoord: ∀i : set, i ∈ J → apply_fun (apply_fun seq n) i ∈ space_family_set Xi i.

An exact proof term for the current goal is (andER (total_function_on (apply_fun seq n) J (space_family_union J Xi) ∧ functional_graph (apply_fun seq n)) (∀i : set, i ∈ J → apply_fun (apply_fun seq n) i ∈ space_family_set Xi i) HseqnProp).

rewrite the current goal using (product_component_def Xi j) (from left to right).

We prove the intermediate claim Hseqjdef: seqj = graph ω (λn0 : set ⇒ apply_fun (apply_fun seq n0) j).

Use reflexivity.

rewrite the current goal using Hseqjdef (from left to right).

rewrite the current goal using (apply_fun_graph ω (λn0 : set ⇒ apply_fun (apply_fun seq n0) j) n HnO) (from left to right).

An exact proof term for the current goal is (HseqnCoord j Hj).

We will prove topology_on Xj Tj ∧ sequence_on seqj Xj ∧ apply_fun x j ∈ Xj ∧ ∀U : set, U ∈ Tj → apply_fun x j ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqj n ∈ U.

Apply andI to the current goal.

An exact proof term for the current goal is HTj.

An exact proof term for the current goal is Hseqj.

An exact proof term for the current goal is Hxcoord.

Let U be given.

Assume HU: U ∈ Tj.

Assume HxU: apply_fun x j ∈ U.

We prove the intermediate claim HUfam: U ∈ space_family_topology Xi j.

We prove the intermediate claim HTjEq: Tj = space_family_topology Xi j.

Use reflexivity.

rewrite the current goal using HTjEq (from right to left).

An exact proof term for the current goal is HU.

Set Cyl to be the term product_cylinder J Xi j U.

We prove the intermediate claim HCylDef: Cyl = {f ∈ product_space J Xi|j ∈ J ∧ U ∈ space_family_topology Xi j ∧ apply_fun f j ∈ U}.

Use reflexivity.

We prove the intermediate claim HjNe: J ≠ Empty.

Assume HJeq: J = Empty.

We prove the intermediate claim HjEmpty: j ∈ Empty.

rewrite the current goal using HJeq (from right to left).

An exact proof term for the current goal is Hj.

We will prove False.

An exact proof term for the current goal is (EmptyE j HjEmpty False).

We prove the intermediate claim HcompTop: ∀i : set, i ∈ J → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Let i be given.

Assume Hi: i ∈ J.

We prove the intermediate claim Hseteq: space_family_set Xi i = product_component Xi i.

Use reflexivity.

We prove the intermediate claim Htopeq: space_family_topology Xi i = product_component_topology Xi i.

Use reflexivity.

rewrite the current goal using Hseteq (from left to right).

rewrite the current goal using Htopeq (from left to right).

rewrite the current goal using (product_component_def Xi i) (from left to right).

rewrite the current goal using (product_component_topology_def Xi i) (from left to right).

rewrite the current goal using (const_space_family_apply J R R_standard_topology i Hi) (from left to right).

rewrite the current goal using (tuple_2_0_eq R R_standard_topology) (from left to right).

rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).

An exact proof term for the current goal is R_standard_topology_is_topology.

We prove the intermediate claim HSsub: subbasis_on (product_space J Xi) (product_subbasis_full J Xi).

An exact proof term for the current goal is (product_subbasis_full_subbasis_on J Xi HjNe HcompTop).

We prove the intermediate claim HCylS: Cyl ∈ product_subbasis_full J Xi.

We prove the intermediate claim HCylRepl: Cyl ∈ {product_cylinder J Xi j V|V ∈ space_family_topology Xi j}.

An exact proof term for the current goal is (ReplI (space_family_topology Xi j) (λV : set ⇒ product_cylinder J Xi j V) U HUfam).

An exact proof term for the current goal is (famunionI J (λi0 : set ⇒ {product_cylinder J Xi i0 V|V ∈ space_family_topology Xi i0}) j Cyl Hj HCylRepl).

We prove the intermediate claim HCylOpen: Cyl ∈ product_topology_full J Xi.

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis (product_space J Xi) (product_subbasis_full J Xi) Cyl HSsub HCylS).

We prove the intermediate claim HxCyl: x ∈ Cyl.

rewrite the current goal using HCylDef (from left to right).

Apply (SepI (product_space J Xi) (λf : set ⇒ j ∈ J ∧ U ∈ space_family_topology Xi j ∧ apply_fun f j ∈ U) x Hxprod (andI (j ∈ J ∧ U ∈ space_family_topology Xi j) (apply_fun x j ∈ U) (andI (j ∈ J) (U ∈ space_family_topology Xi j) Hj HUfam) HxU)) to the current goal.

We prove the intermediate claim HN: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ Cyl.

An exact proof term for the current goal is (converges_to_neighborhoods X (product_topology_full J Xi) seq x Hconv Cyl HCylOpen HxCyl).

Apply HN to the current goal.

Let N be given.

Assume HNpair.

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ Cyl) HNpair).

Let n be given.

Assume HnO: n ∈ ω.

Assume HNn: N ⊆ n.

We will prove apply_fun seqj n ∈ U.

We prove the intermediate claim HseqnCyl: apply_fun seq n ∈ Cyl.

An exact proof term for the current goal is (andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → apply_fun seq n0 ∈ Cyl) HNpair n HnO HNn).

We prove the intermediate claim HseqnCylD: apply_fun seq n ∈ {f ∈ product_space J Xi|j ∈ J ∧ U ∈ space_family_topology Xi j ∧ apply_fun f j ∈ U}.

rewrite the current goal using HCylDef (from right to left).

An exact proof term for the current goal is HseqnCyl.

We prove the intermediate claim HcylProp: j ∈ J ∧ U ∈ space_family_topology Xi j ∧ apply_fun (apply_fun seq n) j ∈ U.

An exact proof term for the current goal is (SepE2 (product_space J Xi) (λf : set ⇒ j ∈ J ∧ U ∈ space_family_topology Xi j ∧ apply_fun f j ∈ U) (apply_fun seq n) HseqnCylD).

We prove the intermediate claim HcylLeft: j ∈ J ∧ U ∈ space_family_topology Xi j.

An exact proof term for the current goal is (andEL (j ∈ J ∧ U ∈ space_family_topology Xi j) (apply_fun (apply_fun seq n) j ∈ U) HcylProp).

We prove the intermediate claim HcoordIn: apply_fun (apply_fun seq n) j ∈ U.

An exact proof term for the current goal is (andER (j ∈ J ∧ U ∈ space_family_topology Xi j) (apply_fun (apply_fun seq n) j ∈ U) HcylProp).

We prove the intermediate claim Hseqjdef2: seqj = graph ω (λn0 : set ⇒ apply_fun (apply_fun seq n0) j).

Use reflexivity.

rewrite the current goal using Hseqjdef2 (from left to right).

rewrite the current goal using (apply_fun_graph ω (λn0 : set ⇒ apply_fun (apply_fun seq n0) j) n HnO) (from left to right).

An exact proof term for the current goal is HcoordIn.

Assume Hcoord: ∀j : set, j ∈ J → converges_to (product_component Xi j) (product_component_topology Xi j) (product_coordinate_sequence seq j) (apply_fun x j).

We will prove converges_to X (product_topology_full J Xi) seq x.

We will prove topology_on X (product_topology_full J Xi) ∧ sequence_on seq X ∧ x ∈ X ∧ ∀U : set, U ∈ product_topology_full J Xi → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.

Apply andI to the current goal.

rewrite the current goal using HX (from left to right).

We prove the intermediate claim HHfam: Hausdorff_spaces_family J Xi.

Let i be given.

Assume Hi: i ∈ J.

We will prove Hausdorff_space (product_component Xi i) (product_component_topology Xi i).

rewrite the current goal using (product_component_def Xi i) (from left to right).

rewrite the current goal using (product_component_topology_def Xi i) (from left to right).

rewrite the current goal using (const_space_family_apply J R R_standard_topology i Hi) (from left to right).

rewrite the current goal using (tuple_2_0_eq R R_standard_topology) (from left to right).

rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).

An exact proof term for the current goal is R_standard_topology_Hausdorff.

We prove the intermediate claim HHprod: Hausdorff_space (product_space J Xi) (product_topology_full J Xi).

An exact proof term for the current goal is (product_topology_full_Hausdorff_axiom J Xi HHfam).

An exact proof term for the current goal is (Hausdorff_space_topology (product_space J Xi) (product_topology_full J Xi) HHprod).

An exact proof term for the current goal is Hseq.

An exact proof term for the current goal is HxX.

Let U be given.

Assume HU: U ∈ product_topology_full J Xi.

Assume HxU: x ∈ U.

Set X0 to be the term product_space J Xi.

Set S to be the term product_subbasis_full J Xi.

Set B to be the term basis_of_subbasis X0 S.

We prove the intermediate claim HxX0: x ∈ X0.

rewrite the current goal using HX (from right to left).

An exact proof term for the current goal is HxX.

We prove the intermediate claim HUgen: U ∈ generated_topology X0 B.

We prove the intermediate claim HTdef: product_topology_full J Xi = generated_topology X0 B.

Use reflexivity.

We will prove U ∈ generated_topology X0 B.

rewrite the current goal using HTdef (from right to left).

An exact proof term for the current goal is HU.

We prove the intermediate claim HUbasis: ∀z ∈ U, ∃b0 ∈ B, z ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 X0) (λU0 : set ⇒ ∀z ∈ U0, ∃b0 ∈ B, z ∈ b0 ∧ b0 ⊆ U0) U HUgen).

Apply (HUbasis x HxU) to the current goal.

Let b0 be given.

Assume Hb0pair.

We prove the intermediate claim Hb0B: b0 ∈ B.

An exact proof term for the current goal is (andEL (b0 ∈ B) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).

We prove the intermediate claim Hxb0sub: x ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (andER (b0 ∈ B) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).

We prove the intermediate claim Hxb0: x ∈ b0.

An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) Hxb0sub).

We prove the intermediate claim Hb0subU: b0 ⊆ U.

An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) Hxb0sub).

We prove the intermediate claim HexN0: ∃N0 : set, N0 ∈ ω ∧ ∀n : set, n ∈ ω → N0 ⊆ n → apply_fun seq n ∈ b0.

We prove the intermediate claim Hb0fin: b0 ∈ finite_intersections_of X0 S.

An exact proof term for the current goal is (SepE1 (finite_intersections_of X0 S) (λb : set ⇒ b ≠ Empty) b0 Hb0B).

We prove the intermediate claim HexF: ∃F ∈ finite_subcollections S, b0 = intersection_of_family X0 F.

An exact proof term for the current goal is (ReplE (finite_subcollections S) (λF0 : set ⇒ intersection_of_family X0 F0) b0 Hb0fin).

Apply HexF to the current goal.

Let F be given.

Assume HFpair.

Apply HFpair to the current goal.

Assume HF: F ∈ finite_subcollections S.

Assume Hb0eq: b0 = intersection_of_family X0 F.

We prove the intermediate claim HxIF: x ∈ intersection_of_family X0 F.

rewrite the current goal using Hb0eq (from right to left).

An exact proof term for the current goal is Hxb0.

We prove the intermediate claim HFpow: F ∈ 𝒫 S.

An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) F HF).

We prove the intermediate claim HFsubS: F ⊆ S.

An exact proof term for the current goal is (PowerE S F HFpow).

We prove the intermediate claim HFfin: finite F.

An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) F HF).

We prove the intermediate claim HeventSub: ∀s : set, s ∈ S → x ∈ s → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ s.

Let s be given.

Assume HsS: s ∈ S.

Assume Hxs: x ∈ s.

We will prove ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ s.

Set Fam to be the term (λi : set ⇒ {product_cylinder J Xi i U|U ∈ space_family_topology Xi i}).

We prove the intermediate claim HsFam: s ∈ (⋃_{i ∈ J}Fam i).

An exact proof term for the current goal is HsS.

Apply (famunionE_impred J Fam s HsFam (∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ s)) to the current goal.

Let i be given.

Assume HiJ: i ∈ J.

Assume HsFi: s ∈ Fam i.

We prove the intermediate claim HexU: ∃U ∈ space_family_topology Xi i, s = product_cylinder J Xi i U.

An exact proof term for the current goal is (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder J Xi i U0) s HsFi).

Apply HexU to the current goal.

Let U be given.

Assume HUand.

Apply HUand to the current goal.

Assume HUtop: U ∈ space_family_topology Xi i.

Assume Hseqs: s = product_cylinder J Xi i U.

We prove the intermediate claim HxCyl: x ∈ product_cylinder J Xi i U.

rewrite the current goal using Hseqs (from right to left).

An exact proof term for the current goal is Hxs.

We prove the intermediate claim HxCylProp: i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun x i ∈ U.

An exact proof term for the current goal is (SepE2 (product_space J Xi) (λf : set ⇒ i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U) x HxCyl).

We prove the intermediate claim HxCylLeft: i ∈ J ∧ U ∈ space_family_topology Xi i.

An exact proof term for the current goal is (andEL (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun x i ∈ U) HxCylProp).

We prove the intermediate claim HUtop2: U ∈ space_family_topology Xi i.

An exact proof term for the current goal is (andER (i ∈ J) (U ∈ space_family_topology Xi i) HxCylLeft).

We prove the intermediate claim HxUi: apply_fun x i ∈ U.

An exact proof term for the current goal is (andER (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun x i ∈ U) HxCylProp).

We prove the intermediate claim Hconi: converges_to (product_component Xi i) (product_component_topology Xi i) (product_coordinate_sequence seq i) (apply_fun x i).

An exact proof term for the current goal is (Hcoord i HiJ).

We prove the intermediate claim HUi: U ∈ product_component_topology Xi i.

We prove the intermediate claim Heq: product_component_topology Xi i = space_family_topology Xi i.

Use reflexivity.

rewrite the current goal using Heq (from left to right).

An exact proof term for the current goal is HUtop2.

We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun (product_coordinate_sequence seq i) n ∈ U.

An exact proof term for the current goal is (converges_to_neighborhoods (product_component Xi i) (product_component_topology Xi i) (product_coordinate_sequence seq i) (apply_fun x i) Hconi U HUi HxUi).

Apply HexN to the current goal.

Let N be given.

Assume HNpair.

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun (product_coordinate_sequence seq i) n ∈ U) HNpair).

Let n be given.

Assume HnO: n ∈ ω.

Assume HNn: N ⊆ n.

We will prove apply_fun seq n ∈ s.

We prove the intermediate claim HseqnX0: apply_fun seq n ∈ product_space J Xi.

rewrite the current goal using HX (from right to left).

An exact proof term for the current goal is (Hseq n HnO).

We prove the intermediate claim Hseqidef: product_coordinate_sequence seq i = graph ω (λn0 : set ⇒ apply_fun (apply_fun seq n0) i).

Use reflexivity.

We prove the intermediate claim HcoordIn: apply_fun (apply_fun seq n) i ∈ U.

We prove the intermediate claim Htmp: apply_fun (product_coordinate_sequence seq i) n ∈ U.

An exact proof term for the current goal is (andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → apply_fun (product_coordinate_sequence seq i) n0 ∈ U) HNpair n HnO HNn).

We prove the intermediate claim Happ: apply_fun (product_coordinate_sequence seq i) n = apply_fun (apply_fun seq n) i.

rewrite the current goal using Hseqidef (from left to right).

rewrite the current goal using (apply_fun_graph ω (λn0 : set ⇒ apply_fun (apply_fun seq n0) i) n HnO) (from left to right).

Use reflexivity.

rewrite the current goal using Happ (from right to left).

An exact proof term for the current goal is Htmp.

rewrite the current goal using Hseqs (from left to right).

We prove the intermediate claim HcylDef: product_cylinder J Xi i U = {f ∈ product_space J Xi|i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U}.

Use reflexivity.

rewrite the current goal using HcylDef (from left to right).

An exact proof term for the current goal is (SepI (product_space J Xi) (λf : set ⇒ i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U) (apply_fun seq n) HseqnX0 (andI (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun seq n) i ∈ U) (andI (i ∈ J) (U ∈ space_family_topology Xi i) HiJ HUtop) HcoordIn)).

Set p to be the term (λA : set ⇒ A ⊆ S → x ∈ intersection_of_family X0 A → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ intersection_of_family X0 A).

We prove the intermediate claim HpEmpty: p Empty.

Assume Hsub0: Empty ⊆ S.

Assume HxI0: x ∈ intersection_of_family X0 Empty.

We will prove ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ intersection_of_family X0 Empty.

We use 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (nat_p_omega 0 nat_0).

Let n be given.

Assume HnO: n ∈ ω.

Assume H0n: 0 ⊆ n.

We will prove apply_fun seq n ∈ intersection_of_family X0 Empty.

rewrite the current goal using (intersection_of_family_empty_eq X0) (from left to right).

We prove the intermediate claim HseqnX0: apply_fun seq n ∈ X0.

rewrite the current goal using HX (from right to left).

An exact proof term for the current goal is (Hseq n HnO).

An exact proof term for the current goal is HseqnX0.

We prove the intermediate claim HpStep: ∀A y : set, finite A → y ∉ A → p A → p (A ∪ {y}).

Let A and y be given.

Assume HAfin: finite A.

Assume HynA: y ∉ A.

Assume HpA: p A.

Assume HsubAy: A ∪ {y} ⊆ S.

Assume HxIay: x ∈ intersection_of_family X0 (A ∪ {y}).

We will prove ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ intersection_of_family X0 (A ∪ {y}).

We prove the intermediate claim HsubA: A ⊆ S.

An exact proof term for the current goal is (Subq_tra A (A ∪ {y}) S (binunion_Subq_1 A {y}) HsubAy).

We prove the intermediate claim HyIn: y ∈ A ∪ {y}.

An exact proof term for the current goal is (binunionI2 A {y} y (SingI y)).

We prove the intermediate claim HyS: y ∈ S.

An exact proof term for the current goal is (HsubAy y HyIn).

We prove the intermediate claim HxIay2: x ∈ (intersection_of_family X0 A) ∩ y.

rewrite the current goal using (intersection_of_family_adjoin X0 A y) (from right to left).

An exact proof term for the current goal is HxIay.

We prove the intermediate claim HxIA: x ∈ intersection_of_family X0 A.

An exact proof term for the current goal is (binintersectE1 (intersection_of_family X0 A) y x HxIay2).

We prove the intermediate claim Hxy: x ∈ y.

An exact proof term for the current goal is (binintersectE2 (intersection_of_family X0 A) y x HxIay2).

We prove the intermediate claim HexNA: ∃NA : set, NA ∈ ω ∧ ∀n : set, n ∈ ω → NA ⊆ n → apply_fun seq n ∈ intersection_of_family X0 A.

An exact proof term for the current goal is (HpA HsubA HxIA).

We prove the intermediate claim HexNy: ∃Ny : set, Ny ∈ ω ∧ ∀n : set, n ∈ ω → Ny ⊆ n → apply_fun seq n ∈ y.

An exact proof term for the current goal is (HeventSub y HyS Hxy).

Apply HexNA to the current goal.

Let NA be given.

Assume HNApair.

Apply HexNy to the current goal.

Let Ny be given.

Assume HNypair.

Set N to be the term NA ∪ Ny.

We prove the intermediate claim HNAo: NA ∈ ω.

An exact proof term for the current goal is (andEL (NA ∈ ω) (∀n : set, n ∈ ω → NA ⊆ n → apply_fun seq n ∈ intersection_of_family X0 A) HNApair).

We prove the intermediate claim HNyo: Ny ∈ ω.

An exact proof term for the current goal is (andEL (Ny ∈ ω) (∀n : set, n ∈ ω → Ny ⊆ n → apply_fun seq n ∈ y) HNypair).

We prove the intermediate claim HNo: N ∈ ω.

An exact proof term for the current goal is (omega_binunion NA Ny HNAo HNyo).

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HNo.

Let n be given.

Assume HnO: n ∈ ω.

Assume HNn: N ⊆ n.

We will prove apply_fun seq n ∈ intersection_of_family X0 (A ∪ {y}).

We prove the intermediate claim HNAsub: NA ⊆ N.

An exact proof term for the current goal is (binunion_Subq_1 NA Ny).

We prove the intermediate claim HNysub: Ny ⊆ N.

An exact proof term for the current goal is (binunion_Subq_2 NA Ny).

We prove the intermediate claim HNAn: NA ⊆ n.

An exact proof term for the current goal is (Subq_tra NA N n HNAsub HNn).

We prove the intermediate claim HNyn: Ny ⊆ n.

An exact proof term for the current goal is (Subq_tra Ny N n HNysub HNn).

We prove the intermediate claim HseqnA: apply_fun seq n ∈ intersection_of_family X0 A.

An exact proof term for the current goal is (andER (NA ∈ ω) (∀n0 : set, n0 ∈ ω → NA ⊆ n0 → apply_fun seq n0 ∈ intersection_of_family X0 A) HNApair n HnO HNAn).

We prove the intermediate claim Hseqny: apply_fun seq n ∈ y.

An exact proof term for the current goal is (andER (Ny ∈ ω) (∀n0 : set, n0 ∈ ω → Ny ⊆ n0 → apply_fun seq n0 ∈ y) HNypair n HnO HNyn).

rewrite the current goal using (intersection_of_family_adjoin X0 A y) (from left to right).

An exact proof term for the current goal is (binintersectI (intersection_of_family X0 A) y (apply_fun seq n) HseqnA Hseqny).

We prove the intermediate claim HpF: p F.

An exact proof term for the current goal is (finite_ind p HpEmpty HpStep F HFfin).

We prove the intermediate claim HexNF: ∃N0 : set, N0 ∈ ω ∧ ∀n : set, n ∈ ω → N0 ⊆ n → apply_fun seq n ∈ intersection_of_family X0 F.

An exact proof term for the current goal is (HpF HFsubS HxIF).

Apply HexNF to the current goal.

Let N0 be given.

Assume HN0pair.

We use N0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀n : set, n ∈ ω → N0 ⊆ n → apply_fun seq n ∈ intersection_of_family X0 F) HN0pair).

Let n be given.

Assume HnO: n ∈ ω.

Assume HN0n: N0 ⊆ n.

We will prove apply_fun seq n ∈ b0.

rewrite the current goal using Hb0eq (from left to right).

An exact proof term for the current goal is (andER (N0 ∈ ω) (∀n0 : set, n0 ∈ ω → N0 ⊆ n0 → apply_fun seq n0 ∈ intersection_of_family X0 F) HN0pair n HnO HN0n).

Apply HexN0 to the current goal.

Let N0 be given.

Assume HN0pair.

We use N0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀n : set, n ∈ ω → N0 ⊆ n → apply_fun seq n ∈ b0) HN0pair).

Let n be given.

Assume HnO: n ∈ ω.

Assume HN0n: N0 ⊆ n.

We will prove apply_fun seq n ∈ U.

We prove the intermediate claim Hnb0: apply_fun seq n ∈ b0.

An exact proof term for the current goal is (andER (N0 ∈ ω) (∀n0 : set, n0 ∈ ω → N0 ⊆ n0 → apply_fun seq n0 ∈ b0) HN0pair n HnO HN0n).

An exact proof term for the current goal is (Hb0subU (apply_fun seq n) Hnb0).