We will prove ¬ normal_space (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology).
Set X to be the term setprod S_Omega Sbar_Omega.
Set Tx to be the term product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology.
Assume Hnorm: normal_space X Tx.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim Hsep: ∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hnorm).
Set Top to be the term setprod S_Omega {S_Omega}.
Set Delta to be the term {p ∈ X|∃a : set, a ∈ S_Omega ∧ p = (a,a)}.
We prove the intermediate claim HclDelta: closed_in X Tx Delta.
Set BigX to be the term setprod Sbar_Omega Sbar_Omega.
Set Tbig to be the term product_topology Sbar_Omega SbarOmega_topology Sbar_Omega SbarOmega_topology.
Set D to be the term {(t,t)|t ∈ Sbar_Omega}.
We prove the intermediate claim HTy: topology_on Sbar_Omega SbarOmega_topology.
We prove the intermediate claim Hdef: SbarOmega_topology = order_topology Sbar_Omega.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (order_topology_is_topology Sbar_Omega simply_ordered_set_Sbar_Omega).
We prove the intermediate claim HTbig: topology_on BigX Tbig.
An exact proof term for the current goal is (product_topology_is_topology Sbar_Omega SbarOmega_topology Sbar_Omega SbarOmega_topology HTy HTy).
We prove the intermediate claim HHaus: Hausdorff_space Sbar_Omega SbarOmega_topology.
We prove the intermediate claim Hdef: SbarOmega_topology = order_topology Sbar_Omega.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (ex17_10_order_topology_Hausdorff Sbar_Omega simply_ordered_set_Sbar_Omega).
We prove the intermediate claim HDclosed: closed_in BigX Tbig D.
We prove the intermediate claim HDclosed0: closed_in (setprod Sbar_Omega Sbar_Omega) (product_topology Sbar_Omega SbarOmega_topology Sbar_Omega SbarOmega_topology) {(x,x)|x ∈ Sbar_Omega}.
An exact proof term for the current goal is (iffEL (Hausdorff_space Sbar_Omega SbarOmega_topology) (closed_in (setprod Sbar_Omega Sbar_Omega) (product_topology Sbar_Omega SbarOmega_topology Sbar_Omega SbarOmega_topology) {(x,x)|x ∈ Sbar_Omega}) (ex17_13_diagonal_closed_iff_Hausdorff Sbar_Omega SbarOmega_topology HTy) HHaus).
We prove the intermediate claim HdefBig: BigX = setprod Sbar_Omega Sbar_Omega.
Use reflexivity.
We prove the intermediate claim HdefT: Tbig = product_topology Sbar_Omega SbarOmega_topology Sbar_Omega SbarOmega_topology.
Use reflexivity.
We prove the intermediate claim HdefD: D = {(x,x)|x ∈ Sbar_Omega}.
Use reflexivity.
rewrite the current goal using HdefBig (from left to right).
rewrite the current goal using HdefT (from left to right).
rewrite the current goal using HdefD (from left to right).
An exact proof term for the current goal is HDclosed0.
We prove the intermediate claim HXsub: X ⊆ BigX.
An exact proof term for the current goal is (setprod_Subq S_Omega Sbar_Omega Sbar_Omega Sbar_Omega S_Omega_Subq_Sbar_Omega (Subq_ref Sbar_Omega)).
We prove the intermediate claim HTxSub: Tx = subspace_topology BigX Tbig X.
We prove the intermediate claim HTyWhole: subspace_topology Sbar_Omega SbarOmega_topology Sbar_Omega = SbarOmega_topology.
An exact proof term for the current goal is (subspace_topology_whole Sbar_Omega SbarOmega_topology HTy).
We prove the intermediate claim HTx1: Tx = product_topology S_Omega (subspace_topology Sbar_Omega SbarOmega_topology S_Omega) Sbar_Omega SbarOmega_topology.
We prove the intermediate claim HdefTx: Tx = product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology.
Use reflexivity.
rewrite the current goal using HdefTx (from left to right).
rewrite the current goal using (SOmega_topology_eq_subspace_SbarOmega) (from left to right).
Use reflexivity.
rewrite the current goal using HTx1 (from left to right).
We prove the intermediate claim HTx2: product_topology S_Omega (subspace_topology Sbar_Omega SbarOmega_topology S_Omega) Sbar_Omega SbarOmega_topology = subspace_topology (setprod Sbar_Omega Sbar_Omega) (product_topology Sbar_Omega SbarOmega_topology Sbar_Omega SbarOmega_topology) (setprod S_Omega Sbar_Omega).
We prove the intermediate claim HTx2sub: product_topology S_Omega (subspace_topology Sbar_Omega SbarOmega_topology S_Omega) Sbar_Omega (subspace_topology Sbar_Omega SbarOmega_topology Sbar_Omega) = subspace_topology (setprod Sbar_Omega Sbar_Omega) (product_topology Sbar_Omega SbarOmega_topology Sbar_Omega SbarOmega_topology) (setprod S_Omega Sbar_Omega).
An exact proof term for the current goal is (product_subspace_topology Sbar_Omega SbarOmega_topology Sbar_Omega SbarOmega_topology S_Omega Sbar_Omega HTy HTy S_Omega_Subq_Sbar_Omega (Subq_ref Sbar_Omega)).
We prove the intermediate claim Htmp: product_topology S_Omega (subspace_topology Sbar_Omega SbarOmega_topology S_Omega) Sbar_Omega (subspace_topology Sbar_Omega SbarOmega_topology Sbar_Omega) = product_topology S_Omega (subspace_topology Sbar_Omega SbarOmega_topology S_Omega) Sbar_Omega SbarOmega_topology.
rewrite the current goal using HTyWhole (from left to right).
Use reflexivity.
rewrite the current goal using Htmp (from right to left).
An exact proof term for the current goal is HTx2sub.
rewrite the current goal using HTx2 (from left to right).
We prove the intermediate claim HdefBig: BigX = setprod Sbar_Omega Sbar_Omega.
Use reflexivity.
We prove the intermediate claim HdefX: X = setprod S_Omega Sbar_Omega.
Use reflexivity.
rewrite the current goal using HdefBig (from left to right).
rewrite the current goal using HdefX (from left to right).
Use reflexivity.
rewrite the current goal using HTxSub (from left to right).
Apply (iffER (closed_in X (subspace_topology BigX Tbig X) Delta) (∃C : set, closed_in BigX Tbig C ∧ Delta = C ∩ X) (closed_in_subspace_iff_intersection BigX Tbig X Delta HTbig HXsub)) to the current goal.
We use D to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HDclosed.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ Delta.
We will prove p ∈ D ∩ X.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (SepE1 X (λp0 : set ⇒ ∃a : set, a ∈ S_Omega ∧ p0 = (a,a)) p Hp).
We prove the intermediate claim HpPred: ∃a : set, a ∈ S_Omega ∧ p = (a,a).
An exact proof term for the current goal is (SepE2 X (λp0 : set ⇒ ∃a : set, a ∈ S_Omega ∧ p0 = (a,a)) p Hp).
Apply HpPred to the current goal.
Let a be given.
Assume HaConj.
We prove the intermediate claim HaS: a ∈ S_Omega.
An exact proof term for the current goal is (andEL (a ∈ S_Omega) (p = (a,a)) HaConj).
We prove the intermediate claim HpEq: p = (a,a).
An exact proof term for the current goal is (andER (a ∈ S_Omega) (p = (a,a)) HaConj).
We prove the intermediate claim HaSb: a ∈ Sbar_Omega.
An exact proof term for the current goal is (S_Omega_Subq_Sbar_Omega a HaS).
We prove the intermediate claim HpD: p ∈ D.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (ReplI Sbar_Omega (λt : set ⇒ (t,t)) a HaSb).
An exact proof term for the current goal is (binintersectI D X p HpD HpX).
Let p be given.
Assume Hp: p ∈ D ∩ X.
We will prove p ∈ Delta.
We prove the intermediate claim HpD: p ∈ D.
An exact proof term for the current goal is (binintersectE1 D X p Hp).
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (binintersectE2 D X p Hp).
We prove the intermediate claim Hex: ∃t ∈ Sbar_Omega, p = (t,t).
An exact proof term for the current goal is (ReplE Sbar_Omega (λt : set ⇒ (t,t)) p HpD).
Apply Hex to the current goal.
Let t be given.
Assume HtPair.
Apply HtPair to the current goal.
Assume HtSb: t ∈ Sbar_Omega.
Assume HpEq: p = (t,t).
We prove the intermediate claim Hp0S: p 0 ∈ S_Omega.
An exact proof term for the current goal is (ap0_Sigma S_Omega (λ_ : set ⇒ Sbar_Omega) p HpX).
We prove the intermediate claim Hp0t: p 0 = t.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq t t).
We prove the intermediate claim HtS: t ∈ S_Omega.
rewrite the current goal using Hp0t (from right to left).
An exact proof term for the current goal is Hp0S.
Apply (SepI X (λp0 : set ⇒ ∃a : set, a ∈ S_Omega ∧ p0 = (a,a)) p HpX) to the current goal.
We use t to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HtS.
An exact proof term for the current goal is HpEq.
We prove the intermediate claim HclTop: closed_in X Tx Top.
We prove the intermediate claim HnormFac: normal_space S_Omega SOmega_topology ∧ normal_space Sbar_Omega SbarOmega_topology.
An exact proof term for the current goal is SOmega_SbarOmega_factors_normal.
We prove the intermediate claim HnormS: normal_space S_Omega SOmega_topology.
An exact proof term for the current goal is (andEL (normal_space S_Omega SOmega_topology) (normal_space Sbar_Omega SbarOmega_topology) HnormFac).
We prove the intermediate claim HnormSb: normal_space Sbar_Omega SbarOmega_topology.
An exact proof term for the current goal is (andER (normal_space S_Omega SOmega_topology) (normal_space Sbar_Omega SbarOmega_topology) HnormFac).
We prove the intermediate claim HTx1: topology_on S_Omega SOmega_topology.
An exact proof term for the current goal is (normal_space_topology_on S_Omega SOmega_topology HnormS).
We prove the intermediate claim HTy1: topology_on Sbar_Omega SbarOmega_topology.
An exact proof term for the current goal is (normal_space_topology_on Sbar_Omega SbarOmega_topology HnormSb).
We prove the intermediate claim HprojPack: continuous_map (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) S_Omega SOmega_topology (projection_map1 S_Omega Sbar_Omega) ∧ continuous_map (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) Sbar_Omega SbarOmega_topology (projection_map2 S_Omega Sbar_Omega).
An exact proof term for the current goal is (projection_maps_continuous S_Omega SOmega_topology Sbar_Omega SbarOmega_topology HTx1 HTy1).
We prove the intermediate claim Hproj2: continuous_map X Tx Sbar_Omega SbarOmega_topology (projection_map2 S_Omega Sbar_Omega).
An exact proof term for the current goal is (andER (continuous_map (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) S_Omega SOmega_topology (projection_map1 S_Omega Sbar_Omega)) (continuous_map (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) Sbar_Omega SbarOmega_topology (projection_map2 S_Omega Sbar_Omega)) HprojPack).
We prove the intermediate claim HoneSb: one_point_sets_closed Sbar_Omega SbarOmega_topology.
An exact proof term for the current goal is (andEL (one_point_sets_closed Sbar_Omega SbarOmega_topology) (∀A B : set, closed_in Sbar_Omega SbarOmega_topology A → closed_in Sbar_Omega SbarOmega_topology B → A ∩ B = Empty → ∃U V : set, U ∈ SbarOmega_topology ∧ V ∈ SbarOmega_topology ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) HnormSb).
We prove the intermediate claim HSmem: S_Omega ∈ Sbar_Omega.
An exact proof term for the current goal is S_Omega_in_Sbar_Omega.
We prove the intermediate claim HallSing: ∀x : set, x ∈ Sbar_Omega → closed_in Sbar_Omega SbarOmega_topology {x}.
An exact proof term for the current goal is (andER (topology_on Sbar_Omega SbarOmega_topology) (∀x : set, x ∈ Sbar_Omega → closed_in Sbar_Omega SbarOmega_topology {x}) HoneSb).
We prove the intermediate claim HsingClosed: closed_in Sbar_Omega SbarOmega_topology {S_Omega}.
An exact proof term for the current goal is (HallSing S_Omega HSmem).
We prove the intermediate claim HpreClosed: closed_in X Tx (preimage_of X (projection_map2 S_Omega Sbar_Omega) {S_Omega}).
An exact proof term for the current goal is (continuous_preserves_closed X Tx Sbar_Omega SbarOmega_topology (projection_map2 S_Omega Sbar_Omega) Hproj2 {S_Omega} HsingClosed).
We prove the intermediate claim HVsub: {S_Omega} ⊆ Sbar_Omega.
Let y be given.
Assume Hy: y ∈ {S_Omega}.
rewrite the current goal using (SingE S_Omega y Hy) (from left to right).
An exact proof term for the current goal is HSmem.
We prove the intermediate claim HpreEq: preimage_of (setprod S_Omega Sbar_Omega) (projection_map2 S_Omega Sbar_Omega) {S_Omega} = rectangle_set S_Omega {S_Omega}.
An exact proof term for the current goal is (preimage_projection2_rectangle S_Omega Sbar_Omega {S_Omega} HVsub).
We will prove closed_in X Tx Top.
rewrite the current goal using HpreEq (from right to left).
An exact proof term for the current goal is HpreClosed.
We prove the intermediate claim Hdisj: Delta ∩ Top = Empty.
Apply Empty_Subq_eq to the current goal.
We will prove Delta ∩ Top ⊆ Empty.
Let p be given.
Assume Hp: p ∈ Delta ∩ Top.
We will prove p ∈ Empty.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HpD: p ∈ Delta.
An exact proof term for the current goal is (binintersectE1 Delta Top p Hp).
We prove the intermediate claim HpT: p ∈ Top.
An exact proof term for the current goal is (binintersectE2 Delta Top p Hp).
We prove the intermediate claim HpPred: ∃a : set, a ∈ S_Omega ∧ p = (a,a).
An exact proof term for the current goal is (SepE2 X (λp0 : set ⇒ ∃a : set, a ∈ S_Omega ∧ p0 = (a,a)) p HpD).
Apply HpPred to the current goal.
Let a be given.
Assume HaConj.
We prove the intermediate claim HaS: a ∈ S_Omega.
An exact proof term for the current goal is (andEL (a ∈ S_Omega) (p = (a,a)) HaConj).
We prove the intermediate claim HpEqD: p = (a,a).
An exact proof term for the current goal is (andER (a ∈ S_Omega) (p = (a,a)) HaConj).
Apply (Sigma_E S_Omega (λ_ : set ⇒ {S_Omega}) p HpT) to the current goal.
Let x be given.
Assume Hxpair.
Apply Hxpair to the current goal.
Assume HxS Hexy.
Apply Hexy to the current goal.
Let y be given.
Assume Hypair.
Apply Hypair to the current goal.
Assume HySing HpEqT.
We prove the intermediate claim HyEq: y = S_Omega.
An exact proof term for the current goal is (SingE S_Omega y HySing).
We prove the intermediate claim Hp1y: p 1 = y.
rewrite the current goal using HpEqT (from left to right).
rewrite the current goal using (tuple_pair x y) (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq x y).
We prove the intermediate claim Hp1a: p 1 = a.
rewrite the current goal using HpEqD (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq a a).
We prove the intermediate claim Heqya: y = a.
rewrite the current goal using Hp1y (from right to left).
An exact proof term for the current goal is Hp1a.
We prove the intermediate claim HaEq: a = S_Omega.
rewrite the current goal using Heqya (from right to left).
An exact proof term for the current goal is HyEq.
We prove the intermediate claim Hmem: S_Omega ∈ S_Omega.
rewrite the current goal using HaEq (from right to left) at position 1.
An exact proof term for the current goal is HaS.
An exact proof term for the current goal is ((In_irref S_Omega) Hmem).
We prove the intermediate claim HUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ Delta ⊆ U ∧ Top ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hsep Delta Top HclDelta HclTop Hdisj).
Apply HUV to the current goal.
Let U be given.
Assume HUV2.
Apply HUV2 to the current goal.
Let V be given.
Assume HUVpack: U ∈ Tx ∧ V ∈ Tx ∧ Delta ⊆ U ∧ Top ⊆ V ∧ U ∩ V = Empty.
Apply (and5E (U ∈ Tx) (V ∈ Tx) (Delta ⊆ U) (Top ⊆ V) (U ∩ V = Empty) HUVpack) to the current goal.
Assume HUinTx HVinTx HDeltaSub HTopSub HUVempty.
We prove the intermediate claim HSunc: uncountable_set S_Omega.
An exact proof term for the current goal is (andER (well_ordered_set S_Omega) (uncountable_set S_Omega) S_Omega_well_ordered_uncountable).
We prove the intermediate claim HSne: S_Omega ≠ Empty.
An exact proof term for the current goal is (uncountable_set_ne_Empty S_Omega HSunc).
We prove the intermediate claim Hexx1: ∃x1 : set, x1 ∈ S_Omega.
An exact proof term for the current goal is (nonempty_has_element S_Omega HSne).
Apply Hexx1 to the current goal.
Let x1 be given.
Assume Hx1: x1 ∈ S_Omega.
Set beta to be the term (λx : set ⇒ Eps_i (λb : set ⇒ b ∈ S_Omega ∧ order_rel Sbar_Omega x b ∧ (x,b) ∉ U)).
We prove the intermediate claim Hbeta_ex: ∀x : set, x ∈ S_Omega → ∃b : set, b ∈ S_Omega ∧ order_rel Sbar_Omega x b ∧ (x,b) ∉ U ∧ beta x = b.
Let x be given.
Assume HxS: x ∈ S_Omega.
We prove the intermediate claim Hex: ∃b : set, b ∈ S_Omega ∧ order_rel Sbar_Omega x b ∧ (x,b) ∉ U.
Set p0 to be the term (x,S_Omega).
We prove the intermediate claim Hp0Top: p0 ∈ Top.
We prove the intermediate claim HTopDef: Top = setprod S_Omega {S_Omega}.
Use reflexivity.
rewrite the current goal using HTopDef (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma S_Omega {S_Omega} x S_Omega HxS (SingI S_Omega)).
We prove the intermediate claim Hp0V: p0 ∈ V.
An exact proof term for the current goal is (HTopSub p0 Hp0Top).
We prove the intermediate claim HTxDef: Tx = generated_topology X (product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology).
Use reflexivity.
We prove the intermediate claim HVgen: V ∈ generated_topology X (product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology).
rewrite the current goal using HTxDef (from right to left).
An exact proof term for the current goal is HVinTx.
We prove the intermediate claim Hexb0: ∃b0 ∈ product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology, p0 ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (generated_topology_local_refine X (product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) V p0 HVgen Hp0V).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pack.
We prove the intermediate claim Hb0B: b0 ∈ product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology.
An exact proof term for the current goal is (andEL (b0 ∈ product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) (p0 ∈ b0 ∧ b0 ⊆ V) Hb0pack).
We prove the intermediate claim Hb0rest: p0 ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (andER (b0 ∈ product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) (p0 ∈ b0 ∧ b0 ⊆ V) Hb0pack).
We prove the intermediate claim Hp0b0: p0 ∈ b0.
An exact proof term for the current goal is (andEL (p0 ∈ b0) (b0 ⊆ V) Hb0rest).
We prove the intermediate claim Hb0subV: b0 ⊆ V.
An exact proof term for the current goal is (andER (p0 ∈ b0) (b0 ⊆ V) Hb0rest).
We prove the intermediate claim HexU1: ∃U1 ∈ SOmega_topology, b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}.
An exact proof term for the current goal is (famunionE SOmega_topology (λU1 : set ⇒ {rectangle_set U1 W|W ∈ SbarOmega_topology}) b0 Hb0B).
Apply HexU1 to the current goal.
Let U1 be given.
Assume HU1pack: U1 ∈ SOmega_topology ∧ b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}.
We prove the intermediate claim HU1open: U1 ∈ SOmega_topology.
An exact proof term for the current goal is (andEL (U1 ∈ SOmega_topology) (b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}) HU1pack).
We prove the intermediate claim Hb0fam: b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}.
An exact proof term for the current goal is (andER (U1 ∈ SOmega_topology) (b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}) HU1pack).
We prove the intermediate claim HexV1: ∃V1 ∈ SbarOmega_topology, b0 = rectangle_set U1 V1.
An exact proof term for the current goal is (ReplE SbarOmega_topology (λV1 : set ⇒ rectangle_set U1 V1) b0 Hb0fam).
Apply HexV1 to the current goal.
Let V1 be given.
Assume HV1pack: V1 ∈ SbarOmega_topology ∧ b0 = rectangle_set U1 V1.
We prove the intermediate claim HV1open: V1 ∈ SbarOmega_topology.
An exact proof term for the current goal is (andEL (V1 ∈ SbarOmega_topology) (b0 = rectangle_set U1 V1) HV1pack).
We prove the intermediate claim Hb0eq: b0 = rectangle_set U1 V1.
An exact proof term for the current goal is (andER (V1 ∈ SbarOmega_topology) (b0 = rectangle_set U1 V1) HV1pack).
We prove the intermediate claim Hp0rect: p0 ∈ rectangle_set U1 V1.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hp0b0.
We prove the intermediate claim Hp0prod: p0 ∈ setprod U1 V1.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is Hp0rect.
We prove the intermediate claim Hp0U1: p0 0 ∈ U1.
An exact proof term for the current goal is (ap0_Sigma U1 (λ_ : set ⇒ V1) p0 Hp0prod).
We prove the intermediate claim Hp0V1: p0 1 ∈ V1.
An exact proof term for the current goal is (ap1_Sigma U1 (λ_ : set ⇒ V1) p0 Hp0prod).
We prove the intermediate claim HxU1: x ∈ U1.
rewrite the current goal using (tuple_2_0_eq x S_Omega) (from right to left).
An exact proof term for the current goal is Hp0U1.
We prove the intermediate claim HOmegaV1: S_Omega ∈ V1.
rewrite the current goal using (tuple_2_1_eq x S_Omega) (from right to left).
An exact proof term for the current goal is Hp0V1.
We prove the intermediate claim HdefSbarTop: SbarOmega_topology = order_topology Sbar_Omega.
Use reflexivity.
We prove the intermediate claim HV1ordTop: V1 ∈ order_topology Sbar_Omega.
rewrite the current goal using HdefSbarTop (from right to left).
An exact proof term for the current goal is HV1open.
We prove the intermediate claim HdefOrdTop: order_topology Sbar_Omega = generated_topology Sbar_Omega (order_topology_basis Sbar_Omega).
Use reflexivity.
We prove the intermediate claim HV1gen: V1 ∈ generated_topology Sbar_Omega (order_topology_basis Sbar_Omega).
rewrite the current goal using HdefOrdTop (from right to left).
An exact proof term for the current goal is HV1ordTop.
We prove the intermediate claim HexI: ∃I ∈ order_topology_basis Sbar_Omega, S_Omega ∈ I ∧ I ⊆ V1.
An exact proof term for the current goal is (generated_topology_local_refine Sbar_Omega (order_topology_basis Sbar_Omega) V1 S_Omega HV1gen HOmegaV1).
Apply HexI to the current goal.
Let I be given.
Assume HIpack.
We prove the intermediate claim HIbas: I ∈ order_topology_basis Sbar_Omega.
An exact proof term for the current goal is (andEL (I ∈ order_topology_basis Sbar_Omega) (S_Omega ∈ I ∧ I ⊆ V1) HIpack).
We prove the intermediate claim HIrest: S_Omega ∈ I ∧ I ⊆ V1.
An exact proof term for the current goal is (andER (I ∈ order_topology_basis Sbar_Omega) (S_Omega ∈ I ∧ I ⊆ V1) HIpack).
We prove the intermediate claim HOmegaI: S_Omega ∈ I.
An exact proof term for the current goal is (andEL (S_Omega ∈ I) (I ⊆ V1) HIrest).
We prove the intermediate claim HISubV1: I ⊆ V1.
An exact proof term for the current goal is (andER (S_Omega ∈ I) (I ⊆ V1) HIrest).
We prove the intermediate claim HIcases: (∃a0 ∈ Sbar_Omega, ∃b0x ∈ Sbar_Omega, I = {y ∈ Sbar_Omega|order_rel Sbar_Omega a0 y ∧ order_rel Sbar_Omega y b0x}) ∨ (∃b0x ∈ Sbar_Omega, I = {y ∈ Sbar_Omega|order_rel Sbar_Omega y b0x}) ∨ (∃a0 ∈ Sbar_Omega, I = {y ∈ Sbar_Omega|order_rel Sbar_Omega a0 y}) ∨ I = Sbar_Omega.
An exact proof term for the current goal is (order_topology_basis_cases Sbar_Omega I HIbas).
Apply HIcases to the current goal.
Assume Habc: (∃a0 ∈ Sbar_Omega, ∃b0x ∈ Sbar_Omega, I = {y ∈ Sbar_Omega|order_rel Sbar_Omega a0 y ∧ order_rel Sbar_Omega y b0x}) ∨ (∃b0x ∈ Sbar_Omega, I = {y ∈ Sbar_Omega|order_rel Sbar_Omega y b0x}) ∨ (∃a0 ∈ Sbar_Omega, I = {y ∈ Sbar_Omega|order_rel Sbar_Omega a0 y}).
Apply Habc to the current goal.
Assume Hab: (∃a0 ∈ Sbar_Omega, ∃b0x ∈ Sbar_Omega, I = {y ∈ Sbar_Omega|order_rel Sbar_Omega a0 y ∧ order_rel Sbar_Omega y b0x}) ∨ (∃b0x ∈ Sbar_Omega, I = {y ∈ Sbar_Omega|order_rel Sbar_Omega y b0x}).
Apply Hab to the current goal.
Assume Hint.
Apply FalseE to the current goal.
Apply Hint to the current goal.
Let a0 be given.
Assume Ha0pack.
Apply Ha0pack to the current goal.
Assume Ha0inSbar Hexb0x.
Apply Hexb0x to the current goal.
Let b0x be given.
Assume Hb0xpack.
Apply Hb0xpack to the current goal.
Assume Hb0xinSbar HIeq.
We prove the intermediate claim HOmegaInSep: S_Omega ∈ {y ∈ Sbar_Omega|order_rel Sbar_Omega a0 y ∧ order_rel Sbar_Omega y b0x}.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HOmegaI.
We prove the intermediate claim Hrel: order_rel Sbar_Omega a0 S_Omega ∧ order_rel Sbar_Omega S_Omega b0x.
An exact proof term for the current goal is (SepE2 Sbar_Omega (λy : set ⇒ order_rel Sbar_Omega a0 y ∧ order_rel Sbar_Omega y b0x) S_Omega HOmegaInSep).
We prove the intermediate claim HOmegaLt: order_rel Sbar_Omega S_Omega b0x.
An exact proof term for the current goal is (andER (order_rel Sbar_Omega a0 S_Omega) (order_rel Sbar_Omega S_Omega b0x) Hrel).
We prove the intermediate claim HOmegaMem: S_Omega ∈ b0x.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem Sbar_Omega S_Omega b0x Sbar_Omega_well_ordered_set HOmegaLt).
We prove the intermediate claim Hb0xSub: b0x ⊆ S_Omega.
We prove the intermediate claim Hb0xInSucc: b0x ∈ ordsucc S_Omega.
rewrite the current goal using Sbar_Omega_eq_ordsucc (from right to left).
An exact proof term for the current goal is Hb0xinSbar.
Apply (ordsuccE S_Omega b0x Hb0xInSucc) to the current goal.
Assume Hb0xInSO: b0x ∈ S_Omega.
An exact proof term for the current goal is (S_Omega_TransSet b0x Hb0xInSO).
Assume Hb0xEq: b0x = S_Omega.
rewrite the current goal using Hb0xEq (from left to right).
An exact proof term for the current goal is (Subq_ref S_Omega).
We prove the intermediate claim HOmegaInOmega: S_Omega ∈ S_Omega.
An exact proof term for the current goal is (Hb0xSub S_Omega HOmegaMem).
An exact proof term for the current goal is ((In_irref S_Omega) HOmegaInOmega).
Assume Hlow.
Apply FalseE to the current goal.
Apply Hlow to the current goal.
Let b0x be given.
Assume Hb0xpack.
Apply Hb0xpack to the current goal.
Assume Hb0xinSbar HIeq.
We prove the intermediate claim HOmegaInSep: S_Omega ∈ {y ∈ Sbar_Omega|order_rel Sbar_Omega y b0x}.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HOmegaI.
We prove the intermediate claim HOmegaLt: order_rel Sbar_Omega S_Omega b0x.
An exact proof term for the current goal is (SepE2 Sbar_Omega (λy : set ⇒ order_rel Sbar_Omega y b0x) S_Omega HOmegaInSep).
We prove the intermediate claim HOmegaMem: S_Omega ∈ b0x.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem Sbar_Omega S_Omega b0x Sbar_Omega_well_ordered_set HOmegaLt).
We prove the intermediate claim Hb0xSub: b0x ⊆ S_Omega.
We prove the intermediate claim Hb0xInSucc: b0x ∈ ordsucc S_Omega.
rewrite the current goal using Sbar_Omega_eq_ordsucc (from right to left).
An exact proof term for the current goal is Hb0xinSbar.
Apply (ordsuccE S_Omega b0x Hb0xInSucc) to the current goal.
Assume Hb0xInSO: b0x ∈ S_Omega.
An exact proof term for the current goal is (S_Omega_TransSet b0x Hb0xInSO).
Assume Hb0xEq: b0x = S_Omega.
rewrite the current goal using Hb0xEq (from left to right).
An exact proof term for the current goal is (Subq_ref S_Omega).
We prove the intermediate claim HOmegaInOmega: S_Omega ∈ S_Omega.
An exact proof term for the current goal is (Hb0xSub S_Omega HOmegaMem).
An exact proof term for the current goal is ((In_irref S_Omega) HOmegaInOmega).
Assume Hup.
Apply Hup to the current goal.
Let a0 be given.
Assume Ha0pack.
Apply Ha0pack to the current goal.
Assume Ha0inSbar HIeq.
We prove the intermediate claim HOmegaInSep: S_Omega ∈ {y ∈ Sbar_Omega|order_rel Sbar_Omega a0 y}.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HOmegaI.
We prove the intermediate claim Ha0LtOmega: order_rel Sbar_Omega a0 S_Omega.
An exact proof term for the current goal is (SepE2 Sbar_Omega (λy : set ⇒ order_rel Sbar_Omega a0 y) S_Omega HOmegaInSep).
We prove the intermediate claim Ha0InSO: a0 ∈ S_Omega.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem Sbar_Omega a0 S_Omega Sbar_Omega_well_ordered_set Ha0LtOmega).
Set A to be the term UPair a0 x.
We prove the intermediate claim HAsub: A ⊆ S_Omega.
Let y be given.
Assume HyA: y ∈ A.
Apply (UPairE y a0 x HyA (y ∈ S_Omega)) to the current goal.
Assume HyEq: y = a0.
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is Ha0InSO.
Assume HyEq: y = x.
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is HxS.
We prove the intermediate claim HAcount: countable_set A.
We prove the intermediate claim HdefA: A = UPair a0 x.
Use reflexivity.
We prove the intermediate claim HAfin: finite A.
rewrite the current goal using HdefA (from left to right).
An exact proof term for the current goal is (finite_UPair a0 x).
An exact proof term for the current goal is (finite_countable A HAfin).
We prove the intermediate claim Hexb: ∃b : set, b ∈ S_Omega ∧ ∀a : set, a ∈ A → a ∈ b.
An exact proof term for the current goal is (S_Omega_countable_subsets_bounded A HAsub HAcount).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack.
We prove the intermediate claim HbS: b ∈ S_Omega.
An exact proof term for the current goal is (andEL (b ∈ S_Omega) (∀a : set, a ∈ A → a ∈ b) Hbpack).
We prove the intermediate claim HbBd: ∀a : set, a ∈ A → a ∈ b.
An exact proof term for the current goal is (andER (b ∈ S_Omega) (∀a : set, a ∈ A → a ∈ b) Hbpack).
We prove the intermediate claim Ha0Inb: a0 ∈ b.
An exact proof term for the current goal is (HbBd a0 (UPairI1 a0 x)).
We prove the intermediate claim HxInb: x ∈ b.
An exact proof term for the current goal is (HbBd x (UPairI2 a0 x)).
We prove the intermediate claim HbInSbar: b ∈ Sbar_Omega.
An exact proof term for the current goal is (S_Omega_Subq_Sbar_Omega b HbS).
We prove the intermediate claim HbInI: b ∈ I.
rewrite the current goal using HIeq (from left to right).
Apply (SepI Sbar_Omega (λy : set ⇒ order_rel Sbar_Omega a0 y) b HbInSbar) to the current goal.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered Sbar_Omega a0 b Sbar_Omega_well_ordered_set Ha0Inb).
We prove the intermediate claim HbV1: b ∈ V1.
An exact proof term for the current goal is (HISubV1 b HbInI).
We prove the intermediate claim HxbV: (x,b) ∈ V.
We prove the intermediate claim HxbinRect: (x,b) ∈ rectangle_set U1 V1.
An exact proof term for the current goal is (tuple_2_rectangle_set U1 V1 x b HxU1 HbV1).
We prove the intermediate claim Hxbinb0: (x,b) ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HxbinRect.
An exact proof term for the current goal is (Hb0subV (x,b) Hxbinb0).
We prove the intermediate claim HxbNotU: (x,b) ∉ U.
Assume HxbU: (x,b) ∈ U.
Apply FalseE to the current goal.
We prove the intermediate claim HxbInt: (x,b) ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V (x,b) HxbU HxbV).
We prove the intermediate claim HxbEmpty: (x,b) ∈ Empty.
An exact proof term for the current goal is (mem_eqR (x,b) (U ∩ V) Empty HUVempty HxbInt).
An exact proof term for the current goal is (EmptyE (x,b) HxbEmpty).
We use b to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HbS.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered Sbar_Omega x b Sbar_Omega_well_ordered_set HxInb).
An exact proof term for the current goal is HxbNotU.
Assume HIwhole: I = Sbar_Omega.
We prove the intermediate claim HV1all: ∀y : set, y ∈ Sbar_Omega → y ∈ V1.
Let y be given.
Assume HySbar: y ∈ Sbar_Omega.
Apply HISubV1 to the current goal.
rewrite the current goal using HIwhole (from left to right).
An exact proof term for the current goal is HySbar.
Set A to be the term {x}.
We prove the intermediate claim HAsub: A ⊆ S_Omega.
Let y be given.
Assume HyA: y ∈ A.
rewrite the current goal using (SingE x y HyA) (from left to right).
An exact proof term for the current goal is HxS.
We prove the intermediate claim HAcount: countable_set A.
An exact proof term for the current goal is (finite_countable A (Sing_finite x)).
We prove the intermediate claim Hexb: ∃b : set, b ∈ S_Omega ∧ ∀a : set, a ∈ A → a ∈ b.
An exact proof term for the current goal is (S_Omega_countable_subsets_bounded A HAsub HAcount).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack.
We prove the intermediate claim HbS: b ∈ S_Omega.
An exact proof term for the current goal is (andEL (b ∈ S_Omega) (∀a : set, a ∈ A → a ∈ b) Hbpack).
We prove the intermediate claim HbBd: ∀a : set, a ∈ A → a ∈ b.
An exact proof term for the current goal is (andER (b ∈ S_Omega) (∀a : set, a ∈ A → a ∈ b) Hbpack).
We prove the intermediate claim HxInb: x ∈ b.
An exact proof term for the current goal is (HbBd x (SingI x)).
We prove the intermediate claim HbInSbar: b ∈ Sbar_Omega.
An exact proof term for the current goal is (S_Omega_Subq_Sbar_Omega b HbS).
We prove the intermediate claim HbV1: b ∈ V1.
An exact proof term for the current goal is (HV1all b HbInSbar).
We prove the intermediate claim HxbV: (x,b) ∈ V.
We prove the intermediate claim HxbinRect: (x,b) ∈ rectangle_set U1 V1.
An exact proof term for the current goal is (tuple_2_rectangle_set U1 V1 x b HxU1 HbV1).
We prove the intermediate claim Hxbinb0: (x,b) ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HxbinRect.
An exact proof term for the current goal is (Hb0subV (x,b) Hxbinb0).
We prove the intermediate claim HxbNotU: (x,b) ∉ U.
Assume HxbU: (x,b) ∈ U.
Apply FalseE to the current goal.
We prove the intermediate claim HxbInt: (x,b) ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V (x,b) HxbU HxbV).
We prove the intermediate claim HxbEmpty: (x,b) ∈ Empty.
An exact proof term for the current goal is (mem_eqR (x,b) (U ∩ V) Empty HUVempty HxbInt).
An exact proof term for the current goal is (EmptyE (x,b) HxbEmpty).
We use b to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HbS.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered Sbar_Omega x b Sbar_Omega_well_ordered_set HxInb).
An exact proof term for the current goal is HxbNotU.
We prove the intermediate claim HP: (beta x) ∈ S_Omega ∧ order_rel Sbar_Omega x (beta x) ∧ (x,beta x) ∉ U.
An exact proof term for the current goal is (Eps_i_ex (λb : set ⇒ b ∈ S_Omega ∧ order_rel Sbar_Omega x b ∧ (x,b) ∉ U) Hex).
We use (beta x) to witness the existential quantifier.
Apply (and3E ((beta x) ∈ S_Omega) (order_rel Sbar_Omega x (beta x)) ((x,beta x) ∉ U) HP) to the current goal.
Assume HbS HbRel HbNotU.
Apply and4I to the current goal.
An exact proof term for the current goal is HbS.
An exact proof term for the current goal is HbRel.
An exact proof term for the current goal is HbNotU.
Use reflexivity.
Set step to be the term (λi xi : set ⇒ beta xi).
Set seqx to be the term graph ω (λn : set ⇒ nat_primrec x1 step n).
We prove the intermediate claim Hexb: ∃b : set, b ∈ S_Omega ∧ converges_to S_Omega SOmega_topology seqx b.
We will prove ∃b : set, b ∈ S_Omega ∧ converges_to S_Omega SOmega_topology seqx b.
Set g to be the term (λn : set ⇒ nat_primrec x1 step n).
We prove the intermediate claim HseqxDef: seqx = graph ω g.
Use reflexivity.
We prove the intermediate claim Hgnat: ∀n : set, nat_p n → g n ∈ S_Omega.
Let n be given.
Assume HnNat: nat_p n.
Set P to be the term (λk : set ⇒ g k ∈ S_Omega).
We prove the intermediate claim HP0: P 0.
We will prove g 0 ∈ S_Omega.
rewrite the current goal using (nat_primrec_0 x1 step) (from left to right).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HPS: ∀k : set, nat_p k → P k → P (ordsucc k).
Let k be given.
Assume HkNat: nat_p k.
Assume HPk: P k.
We will prove g (ordsucc k) ∈ S_Omega.
We prove the intermediate claim HgSdef: g (ordsucc k) = nat_primrec x1 step (ordsucc k).
Use reflexivity.
rewrite the current goal using HgSdef (from left to right).
We prove the intermediate claim HprimS: nat_primrec x1 step (ordsucc k) = step k (nat_primrec x1 step k).
An exact proof term for the current goal is (nat_primrec_S x1 step k HkNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HstepDef: step k (nat_primrec x1 step k) = beta (nat_primrec x1 step k).
Use reflexivity.
rewrite the current goal using HstepDef (from left to right).
We prove the intermediate claim HxkS: (nat_primrec x1 step k) ∈ S_Omega.
An exact proof term for the current goal is HPk.
We prove the intermediate claim HbetaPack: ∃bb : set, bb ∈ S_Omega ∧ order_rel Sbar_Omega (nat_primrec x1 step k) bb ∧ ((nat_primrec x1 step k),bb) ∉ U ∧ beta (nat_primrec x1 step k) = bb.
An exact proof term for the current goal is (Hbeta_ex (nat_primrec x1 step k) HxkS).
Apply HbetaPack to the current goal.
Let bb be given.
Assume Hbbpack.
Apply (and4E (bb ∈ S_Omega) (order_rel Sbar_Omega (nat_primrec x1 step k) bb) (((nat_primrec x1 step k),bb) ∉ U) (beta (nat_primrec x1 step k) = bb) Hbbpack) to the current goal.
Assume HbbS HbbRel HbbNotU HbbEq.
We prove the intermediate claim HbbEq2: bb = beta (nat_primrec x1 step k).
Use symmetry.
An exact proof term for the current goal is HbbEq.
rewrite the current goal using HbbEq2 (from right to left).
An exact proof term for the current goal is HbbS.
An exact proof term for the current goal is (nat_ind P HP0 (λk HkNat HPk ⇒ HPS k HkNat HPk) n HnNat).
We prove the intermediate claim HgS: ∀n : set, n ∈ ω → g n ∈ S_Omega.
Let n be given.
Assume HnO: n ∈ ω.
An exact proof term for the current goal is (Hgnat n (omega_nat_p n HnO)).
We prove the intermediate claim Happlyg: ∀n : set, n ∈ ω → apply_fun seqx n = g n.
Let n be given.
Assume HnO: n ∈ ω.
rewrite the current goal using HseqxDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω g n HnO).
We prove the intermediate claim HseqxFun: function_on seqx ω S_Omega.
rewrite the current goal using HseqxDef (from left to right).
We prove the intermediate claim Htot: total_function_on (graph ω g) ω S_Omega.
An exact proof term for the current goal is (total_function_on_graph ω S_Omega g (λn HnO ⇒ HgS n HnO)).
An exact proof term for the current goal is (total_function_on_function_on (graph ω g) ω S_Omega Htot).
Set A to be the term {g n|n ∈ ω}.
Set bsup to be the term ⋃ A.
We prove the intermediate claim HAord: ∀a : set, a ∈ A → ordinal a.
Let a be given.
Assume HaA: a ∈ A.
Apply (ReplE_impred ω g a HaA (ordinal a)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HaDef: a = g n.
rewrite the current goal using HaDef (from left to right).
We prove the intermediate claim HSnOrd: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
An exact proof term for the current goal is (ordinal_Hered S_Omega HSnOrd (g n) (HgS n HnO)).
We prove the intermediate claim HReplId: {(λx : set ⇒ x) a0|a0 ∈ A} = A.
Apply set_ext to the current goal.
We will prove {(λx : set ⇒ x) a0|a0 ∈ A} ⊆ A.
Let y be given.
Assume Hy: y ∈ {(λx : set ⇒ x) a0|a0 ∈ A}.
Apply (ReplE_impred A (λx : set ⇒ x) y Hy (y ∈ A)) to the current goal.
Let a0 be given.
Assume Ha0A: a0 ∈ A.
Assume HyDef: y = (λx : set ⇒ x) a0.
rewrite the current goal using HyDef (from left to right).
An exact proof term for the current goal is Ha0A.
We will prove A ⊆ {(λx : set ⇒ x) a0|a0 ∈ A}.
Let y be given.
Assume HyA: y ∈ A.
An exact proof term for the current goal is (ReplI A (λx : set ⇒ x) y HyA).
We prove the intermediate claim HbsupOrd: ordinal bsup.
We prove the intermediate claim HfamEq: (⋃a0 ∈ A(λx : set ⇒ x) a0) = ⋃ A.
Apply set_ext to the current goal.
We will prove (⋃a0 ∈ A(λx : set ⇒ x) a0) ⊆ ⋃ A.
Let y be given.
Assume Hy: y ∈ (⋃a0 ∈ A(λx : set ⇒ x) a0).
Apply (famunionE_impred A (λx : set ⇒ (λx0 : set ⇒ x0) x) y Hy (y ∈ ⋃ A)) to the current goal.
Let a0 be given.
Assume Ha0A: a0 ∈ A.
Assume HyIn: y ∈ (λx0 : set ⇒ x0) a0.
We prove the intermediate claim HyInA0: y ∈ a0.
An exact proof term for the current goal is HyIn.
An exact proof term for the current goal is (UnionI A y a0 HyInA0 Ha0A).
We will prove ⋃ A ⊆ (⋃a0 ∈ A(λx : set ⇒ x) a0).
Let y be given.
Assume Hy: y ∈ ⋃ A.
Apply (UnionE_impred A y Hy (y ∈ (⋃a0 ∈ A(λx : set ⇒ x) a0))) to the current goal.
Let a0 be given.
Assume HyInA0: y ∈ a0.
Assume Ha0A: a0 ∈ A.
An exact proof term for the current goal is (famunionI A (λx : set ⇒ (λx0 : set ⇒ x0) x) a0 y Ha0A HyInA0).
rewrite the current goal using HfamEq (from right to left).
An exact proof term for the current goal is (ordinal_famunion A (λx : set ⇒ x) (λa0 Ha0A ⇒ HAord a0 Ha0A)).
We prove the intermediate claim HbsupSubSO: bsup ⊆ S_Omega.
Let y be given.
Assume Hy: y ∈ bsup.
Apply (UnionE_impred A y Hy (y ∈ S_Omega)) to the current goal.
Let Y be given.
Assume HyY: y ∈ Y.
Assume HYinA: Y ∈ A.
Apply (ReplE_impred ω g Y HYinA (y ∈ S_Omega)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HYdef: Y = g n.
We prove the intermediate claim HyInGn: y ∈ g n.
An exact proof term for the current goal is (mem_eqR y Y (g n) HYdef HyY).
An exact proof term for the current goal is (S_Omega_TransSet (g n) (HgS n HnO) y HyInGn).
We prove the intermediate claim Hexb0: ∃b0 : set, b0 ∈ S_Omega ∧ ∀n : set, n ∈ ω → apply_fun seqx n ∈ b0.
An exact proof term for the current goal is (S_Omega_omega_family_has_upper_bound seqx HseqxFun).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pack.
We prove the intermediate claim Hb0S: b0 ∈ S_Omega.
An exact proof term for the current goal is (andEL (b0 ∈ S_Omega) (∀n : set, n ∈ ω → apply_fun seqx n ∈ b0) Hb0pack).
We prove the intermediate claim Hb0Bd: ∀n : set, n ∈ ω → apply_fun seqx n ∈ b0.
An exact proof term for the current goal is (andER (b0 ∈ S_Omega) (∀n : set, n ∈ ω → apply_fun seqx n ∈ b0) Hb0pack).
We prove the intermediate claim HbsupSubb0: bsup ⊆ b0.
Let y be given.
Assume Hy: y ∈ bsup.
Apply (UnionE_impred A y Hy (y ∈ b0)) to the current goal.
Let Y be given.
Assume HyY: y ∈ Y.
Assume HYinA: Y ∈ A.
Apply (ReplE_impred ω g Y HYinA (y ∈ b0)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HYdef: Y = g n.
We prove the intermediate claim HYnEq: Y = apply_fun seqx n.
rewrite the current goal using HYdef (from left to right).
rewrite the current goal using (Happlyg n HnO) (from right to left).
Use reflexivity.
We prove the intermediate claim HyInSeq: y ∈ apply_fun seqx n.
An exact proof term for the current goal is (mem_eqR y Y (apply_fun seqx n) HYnEq HyY).
We prove the intermediate claim HynInb0: apply_fun seqx n ∈ b0.
An exact proof term for the current goal is (Hb0Bd n HnO).
We prove the intermediate claim Hb0Ord: ordinal b0.
We prove the intermediate claim HSnOrd: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
An exact proof term for the current goal is (ordinal_Hered S_Omega HSnOrd b0 Hb0S).
An exact proof term for the current goal is (ordinal_TransSet b0 Hb0Ord (apply_fun seqx n) HynInb0 y HyInSeq).
We prove the intermediate claim HbsupInSO: bsup ∈ S_Omega.
We prove the intermediate claim HSnOrd: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
Apply (ordinal_In_Or_Subq bsup S_Omega HbsupOrd HSnOrd (bsup ∈ S_Omega)) to the current goal.
Assume HbIn: bsup ∈ S_Omega.
An exact proof term for the current goal is HbIn.
Assume HSsub: S_Omega ⊆ bsup.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HSsubb0: S_Omega ⊆ b0.
Let y be given.
Assume HySO: y ∈ S_Omega.
Apply HbsupSubb0 to the current goal.
Apply HSsub to the current goal.
An exact proof term for the current goal is HySO.
We prove the intermediate claim Hb0Inb0: b0 ∈ b0.
Apply HSsubb0 to the current goal.
An exact proof term for the current goal is Hb0S.
An exact proof term for the current goal is ((In_irref b0) Hb0Inb0).
We use bsup to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbsupInSO.
We will prove converges_to S_Omega SOmega_topology seqx bsup.
We will prove topology_on S_Omega SOmega_topology ∧ sequence_on seqx S_Omega ∧ bsup ∈ S_Omega ∧ ∀U0 : set, U0 ∈ SOmega_topology → bsup ∈ U0 → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqx n ∈ U0.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HdefSO0: SOmega_topology = order_topology S_Omega.
Use reflexivity.
rewrite the current goal using HdefSO0 (from left to right).
An exact proof term for the current goal is (order_topology_is_topology S_Omega simply_ordered_set_S_Omega).
We will prove sequence_on seqx S_Omega.
An exact proof term for the current goal is HseqxFun.
An exact proof term for the current goal is HbsupInSO.
Let U0 be given.
Assume HU0: U0 ∈ SOmega_topology.
Assume HbsupU0: bsup ∈ U0.
We prove the intermediate claim HdefSO: SOmega_topology = order_topology S_Omega.
Use reflexivity.
We prove the intermediate claim HU0ord: U0 ∈ order_topology S_Omega.
rewrite the current goal using HdefSO (from right to left).
An exact proof term for the current goal is HU0.
We prove the intermediate claim HdefOrd: order_topology S_Omega = generated_topology S_Omega (order_topology_basis S_Omega).
Use reflexivity.
We prove the intermediate claim HU0gen: U0 ∈ generated_topology S_Omega (order_topology_basis S_Omega).
rewrite the current goal using HdefOrd (from right to left).
An exact proof term for the current goal is HU0ord.
We prove the intermediate claim HexI: ∃I ∈ order_topology_basis S_Omega, bsup ∈ I ∧ I ⊆ U0.
An exact proof term for the current goal is (generated_topology_local_refine S_Omega (order_topology_basis S_Omega) U0 bsup HU0gen HbsupU0).
Apply HexI to the current goal.
Let I be given.
Assume HIpack.
We prove the intermediate claim HIbas: I ∈ order_topology_basis S_Omega.
An exact proof term for the current goal is (andEL (I ∈ order_topology_basis S_Omega) (bsup ∈ I ∧ I ⊆ U0) HIpack).
We prove the intermediate claim HIrest: bsup ∈ I ∧ I ⊆ U0.
An exact proof term for the current goal is (andER (I ∈ order_topology_basis S_Omega) (bsup ∈ I ∧ I ⊆ U0) HIpack).
We prove the intermediate claim HbsupI: bsup ∈ I.
An exact proof term for the current goal is (andEL (bsup ∈ I) (I ⊆ U0) HIrest).
We prove the intermediate claim HISubU0: I ⊆ U0.
An exact proof term for the current goal is (andER (bsup ∈ I) (I ⊆ U0) HIrest).
Set xn to be the term (λn : set ⇒ apply_fun seqx n).
We prove the intermediate claim HxSubSucc: ∀n : set, n ∈ ω → xn n ⊆ xn (ordsucc n).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HnSO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HxDef: xn n = nat_primrec x1 step n.
rewrite the current goal using (Happlyg n HnO) (from left to right).
Use reflexivity.
We prove the intermediate claim HxSDef: xn (ordsucc n) = nat_primrec x1 step (ordsucc n).
rewrite the current goal using (Happlyg (ordsucc n) HnSO) (from left to right).
Use reflexivity.
rewrite the current goal using HxDef (from left to right).
rewrite the current goal using HxSDef (from left to right).
We prove the intermediate claim HprimS: nat_primrec x1 step (ordsucc n) = step n (nat_primrec x1 step n).
An exact proof term for the current goal is (nat_primrec_S x1 step n HnNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HstepDef: step n (nat_primrec x1 step n) = beta (nat_primrec x1 step n).
Use reflexivity.
rewrite the current goal using HstepDef (from left to right).
We prove the intermediate claim HxS: (nat_primrec x1 step n) ∈ S_Omega.
An exact proof term for the current goal is (HgS n HnO).
We prove the intermediate claim HbetaPack: ∃bb : set, bb ∈ S_Omega ∧ order_rel Sbar_Omega (nat_primrec x1 step n) bb ∧ ((nat_primrec x1 step n),bb) ∉ U ∧ beta (nat_primrec x1 step n) = bb.
An exact proof term for the current goal is (Hbeta_ex (nat_primrec x1 step n) HxS).
Apply HbetaPack to the current goal.
Let bb be given.
Assume Hbbpack.
Apply (and4E (bb ∈ S_Omega) (order_rel Sbar_Omega (nat_primrec x1 step n) bb) (((nat_primrec x1 step n),bb) ∉ U) (beta (nat_primrec x1 step n) = bb) Hbbpack) to the current goal.
Assume HbbS HbbRel HbbNotU HbbEq.
We prove the intermediate claim HbbEq2: bb = beta (nat_primrec x1 step n).
Use symmetry.
An exact proof term for the current goal is HbbEq.
rewrite the current goal using HbbEq2 (from right to left).
We prove the intermediate claim Hxmem: (nat_primrec x1 step n) ∈ bb.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem Sbar_Omega (nat_primrec x1 step n) bb Sbar_Omega_well_ordered_set HbbRel).
We prove the intermediate claim HbbOrd: ordinal bb.
We prove the intermediate claim HSnOrd: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
An exact proof term for the current goal is (ordinal_Hered S_Omega HSnOrd bb HbbS).
Let y be given.
Assume Hy: y ∈ (nat_primrec x1 step n).
An exact proof term for the current goal is (ordinal_TransSet bb HbbOrd (nat_primrec x1 step n) Hxmem y Hy).
We prove the intermediate claim Hmono: ∀m : set, nat_p m → ∀n : set, n ∈ ω → n ⊆ m → xn n ⊆ xn m.
Let m be given.
Assume HmNat: nat_p m.
Set Pm to be the term (λk : set ⇒ ∀n : set, n ∈ ω → n ⊆ k → xn n ⊆ xn k).
We prove the intermediate claim HPm0: Pm 0.
Let n be given.
Assume HnO: n ∈ ω.
Assume HnSub0: n ⊆ 0.
We prove the intermediate claim H0def: 0 = Empty.
Use reflexivity.
We prove the intermediate claim HnEmpty: n ⊆ Empty.
rewrite the current goal using H0def (from right to left).
An exact proof term for the current goal is HnSub0.
We prove the intermediate claim HnEq0: n = 0.
We prove the intermediate claim HnEqE: n = Empty.
An exact proof term for the current goal is (Empty_Subq_eq n HnEmpty).
rewrite the current goal using H0def (from right to left).
An exact proof term for the current goal is HnEqE.
rewrite the current goal using HnEq0 (from left to right).
An exact proof term for the current goal is (Subq_ref (xn 0)).
We prove the intermediate claim HPmS: ∀k : set, nat_p k → Pm k → Pm (ordsucc k).
Let k be given.
Assume HkNat: nat_p k.
Assume HPk: Pm k.
Let n be given.
Assume HnO: n ∈ ω.
Assume HnSub: n ⊆ ordsucc k.
We prove the intermediate claim HnOrd: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n HnO).
We prove the intermediate claim HkO: k ∈ ω.
An exact proof term for the current goal is (nat_p_omega k HkNat).
We prove the intermediate claim HokOrd: ordinal (ordsucc k).
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (ordsucc k) (omega_ordsucc k HkO)).
Apply (ordinal_trichotomy_or_impred n (ordsucc k) HnOrd HokOrd (xn n ⊆ xn (ordsucc k))) to the current goal.
Assume HnIn: n ∈ ordsucc k.
We prove the intermediate claim Hnk: n ∈ k ∨ n = k.
An exact proof term for the current goal is (ordsuccE k n HnIn).
Apply (Hnk (xn n ⊆ xn (ordsucc k))) to the current goal.
Assume HnInk: n ∈ k.
We prove the intermediate claim HnSubk: n ⊆ k.
An exact proof term for the current goal is (nat_trans k HkNat n HnInk).
We prove the intermediate claim Hsub1: xn n ⊆ xn k.
An exact proof term for the current goal is (HPk n HnO HnSubk).
We prove the intermediate claim Hsub2: xn k ⊆ xn (ordsucc k).
An exact proof term for the current goal is (HxSubSucc k HkO).
Let y be given.
Assume Hy: y ∈ xn n.
Apply Hsub2 to the current goal.
An exact proof term for the current goal is (Hsub1 y Hy).
Assume HnEqk: n = k.
rewrite the current goal using HnEqk (from left to right).
An exact proof term for the current goal is (HxSubSucc k HkO).
Assume HnEq: n = ordsucc k.
rewrite the current goal using HnEq (from left to right).
An exact proof term for the current goal is (Subq_ref (xn (ordsucc k))).
Assume HokIn: ordsucc k ∈ n.
We prove the intermediate claim HokSub: ordsucc k ⊆ n.
An exact proof term for the current goal is (ordinal_TransSet n HnOrd (ordsucc k) HokIn).
We prove the intermediate claim HnEq: n = ordsucc k.
Apply set_ext to the current goal.
An exact proof term for the current goal is HnSub.
An exact proof term for the current goal is HokSub.
rewrite the current goal using HnEq (from left to right).
An exact proof term for the current goal is (Subq_ref (xn (ordsucc k))).
An exact proof term for the current goal is (nat_ind Pm HPm0 (λk HkNat HPk ⇒ HPmS k HkNat HPk) m HmNat).
We prove the intermediate claim HIcases: (∃a ∈ S_Omega, ∃c ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}) ∨ (∃c ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega x c}) ∨ (∃a ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x}) ∨ I = S_Omega.
An exact proof term for the current goal is (order_topology_basis_cases S_Omega I HIbas).
Apply HIcases to the current goal.
Assume Habc: (∃a ∈ S_Omega, ∃c ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}) ∨ (∃c ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega x c}) ∨ (∃a ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x}).
Apply Habc to the current goal.
Assume Hab: (∃a ∈ S_Omega, ∃c ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}) ∨ (∃c ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega x c}).
Apply Hab to the current goal.
Assume Hex: ∃a ∈ S_Omega, ∃c ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}.
Apply Hex to the current goal.
Let a be given.
Assume HaPack.
We prove the intermediate claim HaS: a ∈ S_Omega.
An exact proof term for the current goal is (andEL (a ∈ S_Omega) (∃c : set, c ∈ S_Omega ∧ I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}) HaPack).
We prove the intermediate claim Hrest: ∃c : set, c ∈ S_Omega ∧ I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}.
An exact proof term for the current goal is (andER (a ∈ S_Omega) (∃c : set, c ∈ S_Omega ∧ I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}) HaPack).
Apply Hrest to the current goal.
Let c be given.
Assume HcPack.
We prove the intermediate claim HcS: c ∈ S_Omega.
An exact proof term for the current goal is (andEL (c ∈ S_Omega) (I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}) HcPack).
We prove the intermediate claim HIeq: I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}.
An exact proof term for the current goal is (andER (c ∈ S_Omega) (I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}) HcPack).
We prove the intermediate claim HbsupCore: order_rel S_Omega a bsup ∧ order_rel S_Omega bsup c.
We prove the intermediate claim HbsupI': bsup ∈ {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}.
An exact proof term for the current goal is (mem_eqR bsup I {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c} HIeq HbsupI).
An exact proof term for the current goal is (SepE2 S_Omega (λx : set ⇒ order_rel S_Omega a x ∧ order_rel S_Omega x c) bsup HbsupI').
We prove the intermediate claim Habup: order_rel S_Omega a bsup.
An exact proof term for the current goal is (andEL (order_rel S_Omega a bsup) (order_rel S_Omega bsup c) HbsupCore).
We prove the intermediate claim Hbsupc: order_rel S_Omega bsup c.
An exact proof term for the current goal is (andER (order_rel S_Omega a bsup) (order_rel S_Omega bsup c) HbsupCore).
We prove the intermediate claim HaInbsup: a ∈ bsup.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem S_Omega a bsup S_Omega_well_ordered_set Habup).
We prove the intermediate claim HbsupInc: bsup ∈ c.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem S_Omega bsup c S_Omega_well_ordered_set Hbsupc).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ a ∈ xn N.
Apply (UnionE_impred A a HaInbsup (∃N : set, N ∈ ω ∧ a ∈ xn N)) to the current goal.
Let Y be given.
Assume HaY: a ∈ Y.
Assume HYinA: Y ∈ A.
Apply (ReplE_impred ω g Y HYinA (∃N : set, N ∈ ω ∧ a ∈ xn N)) to the current goal.
Let N be given.
Assume HNO: N ∈ ω.
Assume HYdef: Y = g N.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNO.
We prove the intermediate claim HaInGN: a ∈ g N.
An exact proof term for the current goal is (mem_eqR a Y (g N) HYdef HaY).
An exact proof term for the current goal is (mem_eqL a (apply_fun seqx N) (g N) (Happlyg N HNO) HaInGN).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (a ∈ xn N) HNpack).
We prove the intermediate claim HaInxN: a ∈ xn N.
An exact proof term for the current goal is (andER (N ∈ ω) (a ∈ xn N) HNpack).
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 HNsub: N ⊆ n.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HsubNN: xn N ⊆ xn n.
An exact proof term for the current goal is (Hmono n HnNat N HNO HNsub).
We prove the intermediate claim HaInxn: a ∈ xn n.
An exact proof term for the current goal is (HsubNN a HaInxN).
We prove the intermediate claim HxnS: xn n ∈ S_Omega.
rewrite the current goal using (Happlyg n HnO) (from left to right).
An exact proof term for the current goal is (HgS n HnO).
We prove the intermediate claim Habxn: order_rel S_Omega a (xn n).
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered S_Omega a (xn n) S_Omega_well_ordered_set HaInxn).
We prove the intermediate claim Hxnc: order_rel S_Omega (xn n) c.
We prove the intermediate claim HcOrd: ordinal c.
We prove the intermediate claim HSnOrd: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
An exact proof term for the current goal is (ordinal_Hered S_Omega HSnOrd c HcS).
We prove the intermediate claim HxnSubbsup: xn n ⊆ bsup.
Let y be given.
Assume Hy: y ∈ xn n.
We prove the intermediate claim HyAp: y ∈ apply_fun seqx n.
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyGn: y ∈ g n.
An exact proof term for the current goal is (mem_eqR y (apply_fun seqx n) (g n) (Happlyg n HnO) HyAp).
An exact proof term for the current goal is (UnionI A y (g n) HyGn (ReplI ω g n HnO)).
We prove the intermediate claim HbsupSubc: bsup ⊆ c.
An exact proof term for the current goal is (ordinal_TransSet c HcOrd bsup HbsupInc).
We prove the intermediate claim HxnSubc: xn n ⊆ c.
Let y be given.
Assume Hy: y ∈ xn n.
Apply HbsupSubc to the current goal.
An exact proof term for the current goal is (HxnSubbsup y Hy).
We prove the intermediate claim HxnOrd: ordinal (xn n).
We prove the intermediate claim HSnOrd: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
An exact proof term for the current goal is (ordinal_Hered S_Omega HSnOrd (xn n) HxnS).
We prove the intermediate claim HxnInOr: (xn n) ∈ c ∨ c ⊆ (xn n).
An exact proof term for the current goal is (ordinal_In_Or_Subq (xn n) c HxnOrd HcOrd).
Apply (HxnInOr (order_rel S_Omega (xn n) c)) to the current goal.
Assume HxnInc: (xn n) ∈ c.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered S_Omega (xn n) c S_Omega_well_ordered_set HxnInc).
Assume HcSub: c ⊆ (xn n).
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HxnEqc: xn n = c.
Apply set_ext to the current goal.
An exact proof term for the current goal is HxnSubc.
An exact proof term for the current goal is HcSub.
We prove the intermediate claim HbsupEqc: bsup = c.
Apply set_ext to the current goal.
An exact proof term for the current goal is HbsupSubc.
Let y be given.
Assume Hyc: y ∈ c.
We prove the intermediate claim Hyxn: y ∈ xn n.
An exact proof term for the current goal is (HcSub y Hyc).
An exact proof term for the current goal is (HxnSubbsup y Hyxn).
We prove the intermediate claim Heq: c = bsup.
Use symmetry.
An exact proof term for the current goal is HbsupEqc.
We prove the intermediate claim HbsupInbsup: bsup ∈ bsup.
An exact proof term for the current goal is (mem_eqR bsup c bsup Heq HbsupInc).
An exact proof term for the current goal is ((In_irref bsup) HbsupInbsup).
We prove the intermediate claim HxnI: xn n ∈ I.
We prove the intermediate claim HxnI': xn n ∈ {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c}.
Apply (SepI S_Omega (λx : set ⇒ order_rel S_Omega a x ∧ order_rel S_Omega x c) (xn n) HxnS) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Habxn.
An exact proof term for the current goal is Hxnc.
An exact proof term for the current goal is (mem_eqL (xn n) I {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x c} HIeq HxnI').
Apply HISubU0 to the current goal.
An exact proof term for the current goal is HxnI.
Assume Hex: ∃c ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega x c}.
Apply Hex to the current goal.
Let c be given.
Assume HcPack.
We prove the intermediate claim HcS: c ∈ S_Omega.
An exact proof term for the current goal is (andEL (c ∈ S_Omega) (I = {x ∈ S_Omega|order_rel S_Omega x c}) HcPack).
We prove the intermediate claim HIeq: I = {x ∈ S_Omega|order_rel S_Omega x c}.
An exact proof term for the current goal is (andER (c ∈ S_Omega) (I = {x ∈ S_Omega|order_rel S_Omega x c}) HcPack).
We prove the intermediate claim HbsupRel: order_rel S_Omega bsup c.
We prove the intermediate claim HbsupI': bsup ∈ {x ∈ S_Omega|order_rel S_Omega x c}.
An exact proof term for the current goal is (mem_eqR bsup I {x ∈ S_Omega|order_rel S_Omega x c} HIeq HbsupI).
An exact proof term for the current goal is (SepE2 S_Omega (λx : set ⇒ order_rel S_Omega x c) bsup HbsupI').
We prove the intermediate claim HbsupInc: bsup ∈ c.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem S_Omega bsup c S_Omega_well_ordered_set HbsupRel).
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 H0sub: 0 ⊆ n.
We prove the intermediate claim HxnS: xn n ∈ S_Omega.
rewrite the current goal using (Happlyg n HnO) (from left to right).
An exact proof term for the current goal is (HgS n HnO).
We prove the intermediate claim HcOrd: ordinal c.
We prove the intermediate claim HSnOrd: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
An exact proof term for the current goal is (ordinal_Hered S_Omega HSnOrd c HcS).
We prove the intermediate claim HxnSubbsup: xn n ⊆ bsup.
Let y be given.
Assume Hy: y ∈ xn n.
We prove the intermediate claim HyAp: y ∈ apply_fun seqx n.
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyGn: y ∈ g n.
An exact proof term for the current goal is (mem_eqR y (apply_fun seqx n) (g n) (Happlyg n HnO) HyAp).
An exact proof term for the current goal is (UnionI A y (g n) HyGn (ReplI ω g n HnO)).
We prove the intermediate claim HbsupSubc: bsup ⊆ c.
An exact proof term for the current goal is (ordinal_TransSet c HcOrd bsup HbsupInc).
We prove the intermediate claim HxnSubc: xn n ⊆ c.
Let y be given.
Assume Hy: y ∈ xn n.
Apply HbsupSubc to the current goal.
An exact proof term for the current goal is (HxnSubbsup y Hy).
We prove the intermediate claim HxnOrd: ordinal (xn n).
We prove the intermediate claim HSnOrd: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
An exact proof term for the current goal is (ordinal_Hered S_Omega HSnOrd (xn n) HxnS).
We prove the intermediate claim HxnInOr: (xn n) ∈ c ∨ c ⊆ (xn n).
An exact proof term for the current goal is (ordinal_In_Or_Subq (xn n) c HxnOrd HcOrd).
Apply (HxnInOr (apply_fun seqx n ∈ U0)) to the current goal.
Assume HxnInc: (xn n) ∈ c.
We prove the intermediate claim HxnRel: order_rel S_Omega (xn n) c.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered S_Omega (xn n) c S_Omega_well_ordered_set HxnInc).
We prove the intermediate claim HxnI: xn n ∈ I.
We prove the intermediate claim HxnI': xn n ∈ {x ∈ S_Omega|order_rel S_Omega x c}.
An exact proof term for the current goal is (SepI S_Omega (λx : set ⇒ order_rel S_Omega x c) (xn n) HxnS HxnRel).
An exact proof term for the current goal is (mem_eqL (xn n) I {x ∈ S_Omega|order_rel S_Omega x c} HIeq HxnI').
Apply HISubU0 to the current goal.
An exact proof term for the current goal is HxnI.
Assume HcSub: c ⊆ (xn n).
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HxnEqc: xn n = c.
Apply set_ext to the current goal.
An exact proof term for the current goal is HxnSubc.
An exact proof term for the current goal is HcSub.
We prove the intermediate claim HbsupEqc: bsup = c.
Apply set_ext to the current goal.
An exact proof term for the current goal is HbsupSubc.
Let y be given.
Assume Hyc: y ∈ c.
We prove the intermediate claim Hyxn: y ∈ xn n.
An exact proof term for the current goal is (mem_eqL y (xn n) c HxnEqc Hyc).
An exact proof term for the current goal is (HxnSubbsup y Hyxn).
We prove the intermediate claim Heq: c = bsup.
Use symmetry.
An exact proof term for the current goal is HbsupEqc.
We prove the intermediate claim HbsupInbsup: bsup ∈ bsup.
An exact proof term for the current goal is (mem_eqR bsup c bsup Heq HbsupInc).
An exact proof term for the current goal is ((In_irref bsup) HbsupInbsup).
Assume Hex: ∃a ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x}.
Apply Hex to the current goal.
Let a be given.
Assume HaPack.
We prove the intermediate claim HaS: a ∈ S_Omega.
An exact proof term for the current goal is (andEL (a ∈ S_Omega) (I = {x ∈ S_Omega|order_rel S_Omega a x}) HaPack).
We prove the intermediate claim HIeq: I = {x ∈ S_Omega|order_rel S_Omega a x}.
An exact proof term for the current goal is (andER (a ∈ S_Omega) (I = {x ∈ S_Omega|order_rel S_Omega a x}) HaPack).
We prove the intermediate claim HbsupRel: order_rel S_Omega a bsup.
We prove the intermediate claim HbsupI': bsup ∈ {x ∈ S_Omega|order_rel S_Omega a x}.
An exact proof term for the current goal is (mem_eqR bsup I {x ∈ S_Omega|order_rel S_Omega a x} HIeq HbsupI).
An exact proof term for the current goal is (SepE2 S_Omega (λx : set ⇒ order_rel S_Omega a x) bsup HbsupI').
We prove the intermediate claim HaInbsup: a ∈ bsup.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem S_Omega a bsup S_Omega_well_ordered_set HbsupRel).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ a ∈ xn N.
Apply (UnionE_impred A a HaInbsup (∃N : set, N ∈ ω ∧ a ∈ xn N)) to the current goal.
Let Y be given.
Assume HaY: a ∈ Y.
Assume HYinA: Y ∈ A.
Apply (ReplE_impred ω g Y HYinA (∃N : set, N ∈ ω ∧ a ∈ xn N)) to the current goal.
Let N be given.
Assume HNO: N ∈ ω.
Assume HYdef: Y = g N.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNO.
We prove the intermediate claim HaInGN: a ∈ g N.
An exact proof term for the current goal is (mem_eqR a Y (g N) HYdef HaY).
An exact proof term for the current goal is (mem_eqL a (apply_fun seqx N) (g N) (Happlyg N HNO) HaInGN).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (a ∈ xn N) HNpack).
We prove the intermediate claim HaInxN: a ∈ xn N.
An exact proof term for the current goal is (andER (N ∈ ω) (a ∈ xn N) HNpack).
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 HNsub: N ⊆ n.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HsubNN: xn N ⊆ xn n.
An exact proof term for the current goal is (Hmono n HnNat N HNO HNsub).
We prove the intermediate claim HaInxn: a ∈ xn n.
An exact proof term for the current goal is (HsubNN a HaInxN).
We prove the intermediate claim HxnS: xn n ∈ S_Omega.
rewrite the current goal using (Happlyg n HnO) (from left to right).
An exact proof term for the current goal is (HgS n HnO).
We prove the intermediate claim Harxn: order_rel S_Omega a (xn n).
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered S_Omega a (xn n) S_Omega_well_ordered_set HaInxn).
We prove the intermediate claim HxnI: xn n ∈ I.
We prove the intermediate claim HxnI': xn n ∈ {x ∈ S_Omega|order_rel S_Omega a x}.
An exact proof term for the current goal is (SepI S_Omega (λx : set ⇒ order_rel S_Omega a x) (xn n) HxnS Harxn).
An exact proof term for the current goal is (mem_eqL (xn n) I {x ∈ S_Omega|order_rel S_Omega a x} HIeq HxnI').
Apply HISubU0 to the current goal.
An exact proof term for the current goal is HxnI.
Assume HIwhole: I = S_Omega.
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 H0sub: 0 ⊆ n.
Apply HISubU0 to the current goal.
rewrite the current goal using HIwhole (from left to right).
rewrite the current goal using (Happlyg n HnO) (from left to right).
An exact proof term for the current goal is (HgS n HnO).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack.
We prove the intermediate claim HbS: b ∈ S_Omega.
An exact proof term for the current goal is (andEL (b ∈ S_Omega) (converges_to S_Omega SOmega_topology seqx b) Hbpack).
We prove the intermediate claim Hconvx: converges_to S_Omega SOmega_topology seqx b.
An exact proof term for the current goal is (andER (b ∈ S_Omega) (converges_to S_Omega SOmega_topology seqx b) Hbpack).
Set seqp to be the term graph ω (λn : set ⇒ (apply_fun seqx n,beta (apply_fun seqx n))).
We prove the intermediate claim Hconvp: converges_to X Tx seqp (b,b).
We will prove converges_to X Tx seqp (b,b).
We will prove topology_on X Tx ∧ sequence_on seqp X ∧ (b,b) ∈ X ∧ ∀U0 : set, U0 ∈ Tx → (b,b) ∈ U0 → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqp n ∈ U0.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We will prove sequence_on seqp X.
We will prove function_on seqp ω X.
Set g to be the term (λn : set ⇒ (apply_fun seqx n,beta (apply_fun seqx n))).
We prove the intermediate claim Hg_in: ∀n : set, n ∈ ω → g n ∈ X.
Let n be given.
Assume HnO: n ∈ ω.
Set xn to be the term apply_fun seqx n.
We prove the intermediate claim HseqxOn: sequence_on seqx S_Omega.
An exact proof term for the current goal is (converges_to_sequence_on S_Omega SOmega_topology seqx b Hconvx).
We prove the intermediate claim HxnS: xn ∈ S_Omega.
An exact proof term for the current goal is (HseqxOn n HnO).
We prove the intermediate claim Hexb: ∃bb : set, bb ∈ S_Omega ∧ order_rel Sbar_Omega xn bb ∧ (xn,bb) ∉ U ∧ beta xn = bb.
An exact proof term for the current goal is (Hbeta_ex xn HxnS).
Apply Hexb to the current goal.
Let bb be given.
Assume Hbbpack.
Apply (and4E (bb ∈ S_Omega) (order_rel Sbar_Omega xn bb) ((xn,bb) ∉ U) (beta xn = bb) Hbbpack) to the current goal.
Assume HbbS HbbRel HbbNotU HbetaEq.
We prove the intermediate claim HexPn: ∃t : set, t ∈ S_Omega ∧ order_rel Sbar_Omega xn t ∧ (xn,t) ∉ U.
We use bb to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HbbS.
An exact proof term for the current goal is HbbRel.
An exact proof term for the current goal is HbbNotU.
We prove the intermediate claim HPn: (beta xn) ∈ S_Omega ∧ order_rel Sbar_Omega xn (beta xn) ∧ (xn,beta xn) ∉ U.
An exact proof term for the current goal is (Eps_i_ex (λt : set ⇒ t ∈ S_Omega ∧ order_rel Sbar_Omega xn t ∧ (xn,t) ∉ U) HexPn).
We prove the intermediate claim HbetaCore: (beta xn) ∈ S_Omega ∧ order_rel Sbar_Omega xn (beta xn).
An exact proof term for the current goal is (andEL ((beta xn) ∈ S_Omega ∧ order_rel Sbar_Omega xn (beta xn)) ((xn,beta xn) ∉ U) HPn).
We prove the intermediate claim HbetaS: beta xn ∈ S_Omega.
An exact proof term for the current goal is (andEL ((beta xn) ∈ S_Omega) (order_rel Sbar_Omega xn (beta xn)) HbetaCore).
We prove the intermediate claim HySbar: beta xn ∈ Sbar_Omega.
An exact proof term for the current goal is (S_Omega_Subq_Sbar_Omega (beta xn) HbetaS).
We prove the intermediate claim HgDef: g n = (xn,beta xn).
Use reflexivity.
rewrite the current goal using HgDef (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma S_Omega Sbar_Omega xn (beta xn) HxnS HySbar).
We prove the intermediate claim HseqpDef: seqp = graph ω g.
Use reflexivity.
rewrite the current goal using HseqpDef (from left to right).
We prove the intermediate claim Htot: total_function_on (graph ω g) ω X.
An exact proof term for the current goal is (total_function_on_graph ω X g Hg_in).
An exact proof term for the current goal is (total_function_on_function_on (graph ω g) ω X Htot).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma S_Omega Sbar_Omega b b HbS (S_Omega_Subq_Sbar_Omega b HbS)).
Let U0 be given.
Assume HU0: U0 ∈ Tx.
Assume HbbU0: (b,b) ∈ U0.
We prove the intermediate claim HTxDef: Tx = generated_topology X (product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology).
Use reflexivity.
We prove the intermediate claim HU0gen: U0 ∈ generated_topology X (product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology).
rewrite the current goal using HTxDef (from right to left).
An exact proof term for the current goal is HU0.
We prove the intermediate claim Hexb0: ∃b0 ∈ product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology, (b,b) ∈ b0 ∧ b0 ⊆ U0.
An exact proof term for the current goal is (generated_topology_local_refine X (product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) U0 (b,b) HU0gen HbbU0).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pack.
We prove the intermediate claim Hb0B: b0 ∈ product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology.
An exact proof term for the current goal is (andEL (b0 ∈ product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) ((b,b) ∈ b0 ∧ b0 ⊆ U0) Hb0pack).
We prove the intermediate claim Hb0rest: (b,b) ∈ b0 ∧ b0 ⊆ U0.
An exact proof term for the current goal is (andER (b0 ∈ product_subbasis S_Omega SOmega_topology Sbar_Omega SbarOmega_topology) ((b,b) ∈ b0 ∧ b0 ⊆ U0) Hb0pack).
We prove the intermediate claim Hbb_b0: (b,b) ∈ b0.
An exact proof term for the current goal is (andEL ((b,b) ∈ b0) (b0 ⊆ U0) Hb0rest).
We prove the intermediate claim Hb0subU0: b0 ⊆ U0.
An exact proof term for the current goal is (andER ((b,b) ∈ b0) (b0 ⊆ U0) Hb0rest).
We prove the intermediate claim HexU1: ∃U1 ∈ SOmega_topology, b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}.
An exact proof term for the current goal is (famunionE SOmega_topology (λU1 : set ⇒ {rectangle_set U1 W|W ∈ SbarOmega_topology}) b0 Hb0B).
Apply HexU1 to the current goal.
Let U1 be given.
Assume HU1pack: U1 ∈ SOmega_topology ∧ b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}.
We prove the intermediate claim HU1open: U1 ∈ SOmega_topology.
An exact proof term for the current goal is (andEL (U1 ∈ SOmega_topology) (b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}) HU1pack).
We prove the intermediate claim Hb0fam: b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}.
An exact proof term for the current goal is (andER (U1 ∈ SOmega_topology) (b0 ∈ {rectangle_set U1 W|W ∈ SbarOmega_topology}) HU1pack).
We prove the intermediate claim HexV1: ∃V1 ∈ SbarOmega_topology, b0 = rectangle_set U1 V1.
An exact proof term for the current goal is (ReplE SbarOmega_topology (λV1 : set ⇒ rectangle_set U1 V1) b0 Hb0fam).
Apply HexV1 to the current goal.
Let V1 be given.
Assume HV1pack: V1 ∈ SbarOmega_topology ∧ b0 = rectangle_set U1 V1.
We prove the intermediate claim HV1open: V1 ∈ SbarOmega_topology.
An exact proof term for the current goal is (andEL (V1 ∈ SbarOmega_topology) (b0 = rectangle_set U1 V1) HV1pack).
We prove the intermediate claim Hb0eq: b0 = rectangle_set U1 V1.
An exact proof term for the current goal is (andER (V1 ∈ SbarOmega_topology) (b0 = rectangle_set U1 V1) HV1pack).
We prove the intermediate claim HbbRect: (b,b) ∈ rectangle_set U1 V1.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hbb_b0.
We prove the intermediate claim HbbProd: (b,b) ∈ setprod U1 V1.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is HbbRect.
We prove the intermediate claim HbU1: b ∈ U1.
We prove the intermediate claim Hb0coord: (b,b) 0 ∈ U1.
An exact proof term for the current goal is (ap0_Sigma U1 (λ_ : set ⇒ V1) (b,b) HbbProd).
rewrite the current goal using (tuple_2_0_eq b b) (from right to left).
An exact proof term for the current goal is Hb0coord.
We prove the intermediate claim HbV1: b ∈ V1.
We prove the intermediate claim Hb1coord: (b,b) 1 ∈ V1.
An exact proof term for the current goal is (ap1_Sigma U1 (λ_ : set ⇒ V1) (b,b) HbbProd).
rewrite the current goal using (tuple_2_1_eq b b) (from right to left).
An exact proof term for the current goal is Hb1coord.
We prove the intermediate claim HN1pack: ∃N1 : set, N1 ∈ ω ∧ ∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seqx n ∈ U1.
An exact proof term for the current goal is (converges_to_neighborhoods S_Omega SOmega_topology seqx b Hconvx U1 HU1open HbU1).
Apply HN1pack to the current goal.
Let N1 be given.
Assume HN1conj.
We prove the intermediate claim HN1O: N1 ∈ ω.
An exact proof term for the current goal is (andEL (N1 ∈ ω) (∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seqx n ∈ U1) HN1conj).
We prove the intermediate claim HN1prop: ∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seqx n ∈ U1.
An exact proof term for the current goal is (andER (N1 ∈ ω) (∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seqx n ∈ U1) HN1conj).
Set V1sub to be the term V1 ∩ S_Omega.
We prove the intermediate claim HV1subOpen: V1sub ∈ SOmega_topology.
We prove the intermediate claim Hsub: V1sub ∈ subspace_topology Sbar_Omega SbarOmega_topology S_Omega.
An exact proof term for the current goal is (subspace_topologyI Sbar_Omega SbarOmega_topology S_Omega V1 HV1open).
rewrite the current goal using (SOmega_topology_eq_subspace_SbarOmega) (from left to right).
An exact proof term for the current goal is Hsub.
We prove the intermediate claim HbbV1sub: b ∈ V1sub.
An exact proof term for the current goal is (binintersectI V1 S_Omega b HbV1 HbS).
We prove the intermediate claim HN2pack: ∃N2 : set, N2 ∈ ω ∧ ∀n : set, n ∈ ω → N2 ⊆ n → apply_fun seqx n ∈ V1sub.
An exact proof term for the current goal is (converges_to_neighborhoods S_Omega SOmega_topology seqx b Hconvx V1sub HV1subOpen HbbV1sub).
Apply HN2pack to the current goal.
Let N2 be given.
Assume HN2conj.
We prove the intermediate claim HN2O: N2 ∈ ω.
An exact proof term for the current goal is (andEL (N2 ∈ ω) (∀n : set, n ∈ ω → N2 ⊆ n → apply_fun seqx n ∈ V1sub) HN2conj).
We prove the intermediate claim HN2prop: ∀n : set, n ∈ ω → N2 ⊆ n → apply_fun seqx n ∈ V1sub.
An exact proof term for the current goal is (andER (N2 ∈ ω) (∀n : set, n ∈ ω → N2 ⊆ n → apply_fun seqx n ∈ V1sub) HN2conj).
We prove the intermediate claim HordN1: ordinal N1.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal N1 HN1O).
We prove the intermediate claim HordN2: ordinal N2.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal N2 HN2O).
We prove the intermediate claim Hlin: N1 ⊆ N2 ∨ N2 ⊆ N1.
An exact proof term for the current goal is (ordinal_linear N1 N2 HordN1 HordN2).
Apply Hlin to the current goal.
Assume H12: N1 ⊆ N2.
We use N2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN2O.
Let n be given.
Assume HnO: n ∈ ω.
Assume HN2subn: N2 ⊆ n.
We will prove apply_fun seqp n ∈ U0.
We prove the intermediate claim HN1subn: N1 ⊆ n.
An exact proof term for the current goal is (Subq_tra N1 N2 n H12 HN2subn).
We prove the intermediate claim HxU1: apply_fun seqx n ∈ U1.
An exact proof term for the current goal is (HN1prop n HnO HN1subn).
We prove the intermediate claim HseqxDef: seqx = graph ω (λk : set ⇒ nat_primrec x1 step k).
Use reflexivity.
We prove the intermediate claim HxDef: apply_fun seqx n = nat_primrec x1 step n.
rewrite the current goal using HseqxDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λk : set ⇒ nat_primrec x1 step k) n HnO).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HnSO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HxSDef: apply_fun seqx (ordsucc n) = nat_primrec x1 step (ordsucc n).
rewrite the current goal using HseqxDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λk : set ⇒ nat_primrec x1 step k) (ordsucc n) HnSO).
We prove the intermediate claim HprimS: nat_primrec x1 step (ordsucc n) = step n (nat_primrec x1 step n).
An exact proof term for the current goal is (nat_primrec_S x1 step n HnNat).
We prove the intermediate claim HbetaEq: beta (apply_fun seqx n) = apply_fun seqx (ordsucc n).
rewrite the current goal using HxSDef (from left to right).
rewrite the current goal using HprimS (from left to right).
rewrite the current goal using HxDef (from right to left).
Use reflexivity.
We prove the intermediate claim HN2subSucc: N2 ⊆ ordsucc n.
An exact proof term for the current goal is (Subq_tra N2 n (ordsucc n) HN2subn (ordsuccI1 n)).
We prove the intermediate claim HxSuccInV1sub: apply_fun seqx (ordsucc n) ∈ V1sub.
An exact proof term for the current goal is (HN2prop (ordsucc n) HnSO HN2subSucc).
We prove the intermediate claim HyInV1: beta (apply_fun seqx n) ∈ V1.
rewrite the current goal using HbetaEq (from left to right).
An exact proof term for the current goal is (binintersectE1 V1 S_Omega (apply_fun seqx (ordsucc n)) HxSuccInV1sub).
We prove the intermediate claim HseqpDef: seqp = graph ω (λk : set ⇒ (apply_fun seqx k,beta (apply_fun seqx k))).
Use reflexivity.
We prove the intermediate claim HseqpN: apply_fun seqp n = (apply_fun seqx n,beta (apply_fun seqx n)).
rewrite the current goal using HseqpDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λk : set ⇒ (apply_fun seqx k,beta (apply_fun seqx k))) n HnO).
We prove the intermediate claim HpairInRect: (apply_fun seqx n,beta (apply_fun seqx n)) ∈ rectangle_set U1 V1.
An exact proof term for the current goal is (tuple_2_rectangle_set U1 V1 (apply_fun seqx n) (beta (apply_fun seqx n)) HxU1 HyInV1).
We prove the intermediate claim HpairInb0: (apply_fun seqx n,beta (apply_fun seqx n)) ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HpairInRect.
We prove the intermediate claim HseqpInb0: apply_fun seqp n ∈ b0.
rewrite the current goal using HseqpN (from left to right).
An exact proof term for the current goal is HpairInb0.
An exact proof term for the current goal is (Hb0subU0 (apply_fun seqp n) HseqpInb0).
Assume H21: N2 ⊆ N1.
We use N1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1O.
Let n be given.
Assume HnO: n ∈ ω.
Assume HN1subn: N1 ⊆ n.
We will prove apply_fun seqp n ∈ U0.
We prove the intermediate claim HN2subn: N2 ⊆ n.
An exact proof term for the current goal is (Subq_tra N2 N1 n H21 HN1subn).
We prove the intermediate claim HxU1: apply_fun seqx n ∈ U1.
An exact proof term for the current goal is (HN1prop n HnO HN1subn).
We prove the intermediate claim HseqxDef: seqx = graph ω (λk : set ⇒ nat_primrec x1 step k).
Use reflexivity.
We prove the intermediate claim HxDef: apply_fun seqx n = nat_primrec x1 step n.
rewrite the current goal using HseqxDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λk : set ⇒ nat_primrec x1 step k) n HnO).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HnSO: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HxSDef: apply_fun seqx (ordsucc n) = nat_primrec x1 step (ordsucc n).
rewrite the current goal using HseqxDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λk : set ⇒ nat_primrec x1 step k) (ordsucc n) HnSO).
We prove the intermediate claim HprimS: nat_primrec x1 step (ordsucc n) = step n (nat_primrec x1 step n).
An exact proof term for the current goal is (nat_primrec_S x1 step n HnNat).
We prove the intermediate claim HbetaEq: beta (apply_fun seqx n) = apply_fun seqx (ordsucc n).
rewrite the current goal using HxSDef (from left to right).
rewrite the current goal using HprimS (from left to right).
rewrite the current goal using HxDef (from right to left).
Use reflexivity.
We prove the intermediate claim HN2subSucc: N2 ⊆ ordsucc n.
An exact proof term for the current goal is (Subq_tra N2 n (ordsucc n) HN2subn (ordsuccI1 n)).
We prove the intermediate claim HxSuccInV1sub: apply_fun seqx (ordsucc n) ∈ V1sub.
An exact proof term for the current goal is (HN2prop (ordsucc n) HnSO HN2subSucc).
We prove the intermediate claim HyInV1: beta (apply_fun seqx n) ∈ V1.
rewrite the current goal using HbetaEq (from left to right).
An exact proof term for the current goal is (binintersectE1 V1 S_Omega (apply_fun seqx (ordsucc n)) HxSuccInV1sub).
We prove the intermediate claim HseqpDef: seqp = graph ω (λk : set ⇒ (apply_fun seqx k,beta (apply_fun seqx k))).
Use reflexivity.
We prove the intermediate claim HseqpN: apply_fun seqp n = (apply_fun seqx n,beta (apply_fun seqx n)).
rewrite the current goal using HseqpDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λk : set ⇒ (apply_fun seqx k,beta (apply_fun seqx k))) n HnO).
We prove the intermediate claim HpairInRect: (apply_fun seqx n,beta (apply_fun seqx n)) ∈ rectangle_set U1 V1.
An exact proof term for the current goal is (tuple_2_rectangle_set U1 V1 (apply_fun seqx n) (beta (apply_fun seqx n)) HxU1 HyInV1).
We prove the intermediate claim HpairInb0: (apply_fun seqx n,beta (apply_fun seqx n)) ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HpairInRect.
We prove the intermediate claim HseqpInb0: apply_fun seqp n ∈ b0.
rewrite the current goal using HseqpN (from left to right).
An exact proof term for the current goal is HpairInb0.
An exact proof term for the current goal is (Hb0subU0 (apply_fun seqp n) HseqpInb0).
We prove the intermediate claim HbbInDelta: (b,b) ∈ Delta.
We prove the intermediate claim HbbX: (b,b) ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma S_Omega Sbar_Omega b b HbS (S_Omega_Subq_Sbar_Omega b HbS)).
Apply (SepI X (λp0 : set ⇒ ∃a : set, a ∈ S_Omega ∧ p0 = (a,a)) (b,b) HbbX) to the current goal.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbS.
Use reflexivity.
We prove the intermediate claim HbbU: (b,b) ∈ U.
An exact proof term for the current goal is (HDeltaSub (b,b) HbbInDelta).
We prove the intermediate claim HNpack: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqp n ∈ U.
An exact proof term for the current goal is (converges_to_neighborhoods X Tx seqp (b,b) Hconvp U HUinTx HbbU).
Apply HNpack to the current goal.
Let N be given.
Assume HNconj.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seqp n ∈ U) HNconj).
We prove the intermediate claim HNprop: ∀n : set, n ∈ ω → N ⊆ n → apply_fun seqp n ∈ U.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seqp n ∈ U) HNconj).
We prove the intermediate claim HseqpN: apply_fun seqp N ∈ U.
An exact proof term for the current goal is (HNprop N HNO (Subq_ref N)).
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HseqxOn: sequence_on seqx S_Omega.
An exact proof term for the current goal is (converges_to_sequence_on S_Omega SOmega_topology seqx b Hconvx).
We prove the intermediate claim HxN: apply_fun seqx N ∈ S_Omega.
An exact proof term for the current goal is (HseqxOn N HNO).
We prove the intermediate claim HexbN: ∃bb : set, bb ∈ S_Omega ∧ order_rel Sbar_Omega (apply_fun seqx N) bb ∧ (apply_fun seqx N,bb) ∉ U ∧ beta (apply_fun seqx N) = bb.
An exact proof term for the current goal is (Hbeta_ex (apply_fun seqx N) HxN).
Apply HexbN to the current goal.
Let bb be given.
Assume Hbbpack.
Apply (and4E (bb ∈ S_Omega) (order_rel Sbar_Omega (apply_fun seqx N) bb) ((apply_fun seqx N,bb) ∉ U) (beta (apply_fun seqx N) = bb) Hbbpack) to the current goal.
Assume HbbS HbbRel HnotU HbetaEq.
We prove the intermediate claim HseqpDef: seqp = graph ω (λn : set ⇒ (apply_fun seqx n,beta (apply_fun seqx n))).
Use reflexivity.
We prove the intermediate claim HseqpNpair: apply_fun seqp N = (apply_fun seqx N,beta (apply_fun seqx N)).
rewrite the current goal using HseqpDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λn : set ⇒ (apply_fun seqx n,beta (apply_fun seqx n))) N HNO).
We prove the intermediate claim HseqpNpair2: apply_fun seqp N = (apply_fun seqx N,bb).
rewrite the current goal using HseqpNpair (from left to right).
We prove the intermediate claim HxEq: apply_fun seqx N = apply_fun seqx N.
Use reflexivity.
An exact proof term for the current goal is (tuple_coords_eq (apply_fun seqx N) (beta (apply_fun seqx N)) (apply_fun seqx N) bb HxEq HbetaEq).
We prove the intermediate claim HxNbbinU: (apply_fun seqx N,bb) ∈ U.
rewrite the current goal using HseqpNpair2 (from right to left).
An exact proof term for the current goal is HseqpN.
An exact proof term for the current goal is (HnotU HxNbbinU).
∎