Let X and d be given.
Assume Hm: metric_on X d.
We will prove first_countable_space X (metric_topology X d).
We will prove topology_on X (metric_topology X d) ∧ ∀x : set, x ∈ X → countable_basis_at X (metric_topology X d) x.
Apply andI to the current goal.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
Let x be given.
Assume Hx: x ∈ X.
We will prove countable_basis_at X (metric_topology X d) x.
We will prove topology_on X (metric_topology X d) ∧ x ∈ X ∧ ∃B : set, B ⊆ metric_topology X d ∧ countable_set B ∧ (∀b : set, b ∈ B → x ∈ b) ∧ (∀U : set, U ∈ metric_topology X d → x ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U).
Apply and3I to the current goal.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
An exact proof term for the current goal is Hx.
Set B to be the term {open_ball X d x (inv_nat (ordsucc n))|n ∈ ω}.
We use B to witness the existential quantifier.
Apply and4I to the current goal.
Let b be given.
Assume Hb: b ∈ B.
We will prove b ∈ metric_topology X d.
Apply (ReplE_impred ω (λn : set ⇒ open_ball X d x (inv_nat (ordsucc n))) b Hb) to the current goal.
Let n be given.
Assume HnOmega: n ∈ ω.
Assume HbEq: b = open_ball X d x (inv_nat (ordsucc n)).
rewrite the current goal using HbEq (from left to right).
We prove the intermediate claim HsuccOmega: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnOmega).
We prove the intermediate claim HsuccNonzero: ordsucc n ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HsuccOmega.
Assume Hmem0: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) Hmem0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim HinvR: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HsuccOmega).
We prove the intermediate claim HinvPos: Rlt 0 (inv_nat (ordsucc n)).
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) HsuccNonzero).
An exact proof term for the current goal is (open_ball_in_metric_topology X d x (inv_nat (ordsucc n)) Hm Hx HinvPos).
We prove the intermediate claim HomegaCount: countable_set ω.
We will prove countable_set ω.
We will prove countable ω.
An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).
An exact proof term for the current goal is (countable_image ω HomegaCount (λn : set ⇒ open_ball X d x (inv_nat (ordsucc n)))).
Let b be given.
Assume Hb: b ∈ B.
We will prove x ∈ b.
Apply (ReplE_impred ω (λn : set ⇒ open_ball X d x (inv_nat (ordsucc n))) b Hb) to the current goal.
Let n be given.
Assume HnOmega: n ∈ ω.
Assume HbEq: b = open_ball X d x (inv_nat (ordsucc n)).
rewrite the current goal using HbEq (from left to right).
We prove the intermediate claim HsuccOmega: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnOmega).
We prove the intermediate claim HsuccNonzero: ordsucc n ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HsuccOmega.
Assume Hmem0: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) Hmem0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim HinvR: inv_nat (ordsucc n) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc n) HsuccOmega).
We prove the intermediate claim HinvPos: Rlt 0 (inv_nat (ordsucc n)).
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) HsuccNonzero).
An exact proof term for the current goal is (center_in_open_ball X d x (inv_nat (ordsucc n)) Hm Hx HinvPos).
Let U be given.
Assume HU: U ∈ metric_topology X d.
Assume HxU: x ∈ U.
We will prove ∃b : set, b ∈ B ∧ b ⊆ U.
We prove the intermediate claim Hex: ∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U.
Set B0 to be the term famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim Hdef: metric_topology X d = generated_topology X B0.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X B0.
We will prove U ∈ generated_topology X B0.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUcond: ∀y ∈ U, ∃b0 ∈ B0, y ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y : set, y ∈ U0 → ∃b0 ∈ B0, y ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb0: ∃b0 ∈ B0, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUcond x HxU).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B0: b0 ∈ B0.
An exact proof term for the current goal is (andEL (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hxinb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) (andER (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair)).
We prove the intermediate claim Hb0sub: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) (andER (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair)).
Apply (famunionE_impred X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}) b0 Hb0B0 (∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume Hb0In: b0 ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c r0) b0 Hb0In (∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hb0eq: b0 = open_ball X d c r0.
We prove the intermediate claim HxinBall: x ∈ open_ball X d c r0.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxinb0.
We prove the intermediate claim HballsubU: open_ball X d c r0 ⊆ U.
We will prove open_ball X d c r0 ⊆ U.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hb0sub.
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (open_ball_refine_center X d c x r0 Hm HcX Hx Hr0R Hr0pos HxinBall).
Apply Hexs to the current goal.
Let s be given.
Assume Hs.
We prove the intermediate claim HsRpos: s ∈ R ∧ Rlt 0 s.
An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hs).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (andEL (s ∈ R) (Rlt 0 s) HsRpos).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) HsRpos).
We prove the intermediate claim HsubBall: open_ball X d x s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hs).
We prove the intermediate claim HsubU: open_ball X d x s ⊆ U.
An exact proof term for the current goal is (Subq_tra (open_ball X d x s) (open_ball X d c r0) U HsubBall HballsubU).
We use s to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HsR.
Apply andI to the current goal.
An exact proof term for the current goal is Hspos.
An exact proof term for the current goal is HsubU.
Apply Hex to the current goal.
Let r be given.
Assume Hrp: r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ U).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ U) Hrp).
We prove the intermediate claim Hrprop: Rlt 0 r ∧ open_ball X d x r ⊆ U.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ U) Hrp).
We prove the intermediate claim H0lt: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (open_ball X d x r ⊆ U) Hrprop).
We prove the intermediate claim Hballsub: open_ball X d x r ⊆ U.
An exact proof term for the current goal is (andER (Rlt 0 r) (open_ball X d x r ⊆ U) Hrprop).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) r.
An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt r HrR H0lt).
Apply HexN to the current goal.
Let N be given.
Assume HNpair: N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) r.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (Rlt (inv_nat (ordsucc N)) r) HNpair).
We prove the intermediate claim HinvLt: Rlt (inv_nat (ordsucc N)) r.
An exact proof term for the current goal is (andER (N ∈ ω) (Rlt (inv_nat (ordsucc N)) r) HNpair).
We use (open_ball X d x (inv_nat (ordsucc N))) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI ω (λn : set ⇒ open_ball X d x (inv_nat (ordsucc n))) N HNomega).
We prove the intermediate claim HsSubS: open_ball X d x (inv_nat (ordsucc N)) ⊆ open_ball X d x r.
An exact proof term for the current goal is (open_ball_radius_mono X d x (inv_nat (ordsucc N)) r HinvLt).
An exact proof term for the current goal is (Subq_tra (open_ball X d x (inv_nat (ordsucc N))) (open_ball X d x r) U HsSubS Hballsub).
∎