Let X, Tx and x be given.
Assume Hfc: first_countable_space X Tx.
Assume HT1: T1_space X Tx.
Assume HxX: x ∈ X.
We will prove Gdelta_in X Tx (Sing x).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x0 : set, x0 ∈ X → countable_basis_at X Tx x0) Hfc).
We prove the intermediate claim Hcountbas: ∀x0 : set, x0 ∈ X → countable_basis_at X Tx x0.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → countable_basis_at X Tx x0) Hfc).
We prove the intermediate claim Hcbx: countable_basis_at X Tx x.
An exact proof term for the current goal is (Hcountbas x HxX).
We prove the intermediate claim HexB: ∃B : set, B ⊆ Tx ∧ countable_set B ∧ (∀b : set, b ∈ B → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U).
An exact proof term for the current goal is (andER (topology_on X Tx ∧ x ∈ X) (∃B : set, B ⊆ Tx ∧ countable_set B ∧ (∀b : set, b ∈ B → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U)) Hcbx).
Set B to be the term Eps_i (λB0 : set ⇒ B0 ⊆ Tx ∧ countable_set B0 ∧ (∀b : set, b ∈ B0 → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B0 ∧ b ⊆ U)).
We prove the intermediate claim HBprop: B ⊆ Tx ∧ countable_set B ∧ (∀b : set, b ∈ B → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U).
An exact proof term for the current goal is (Eps_i_ex (λB0 : set ⇒ B0 ⊆ Tx ∧ countable_set B0 ∧ (∀b : set, b ∈ B0 → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B0 ∧ b ⊆ U)) HexB).
We prove the intermediate claim HB123: ((B ⊆ Tx ∧ countable_set B) ∧ (∀b : set, b ∈ B → x ∈ b)).
An exact proof term for the current goal is (andEL ((B ⊆ Tx ∧ countable_set B) ∧ (∀b : set, b ∈ B → x ∈ b)) (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U) HBprop).
We prove the intermediate claim HBrefine: ∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U.
An exact proof term for the current goal is (andER ((B ⊆ Tx ∧ countable_set B) ∧ (∀b : set, b ∈ B → x ∈ b)) (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U) HBprop).
We prove the intermediate claim HB12: (B ⊆ Tx ∧ countable_set B).
An exact proof term for the current goal is (andEL (B ⊆ Tx ∧ countable_set B) (∀b : set, b ∈ B → x ∈ b) HB123).
We prove the intermediate claim HBx: ∀b : set, b ∈ B → x ∈ b.
An exact proof term for the current goal is (andER (B ⊆ Tx ∧ countable_set B) (∀b : set, b ∈ B → x ∈ b) HB123).
We prove the intermediate claim HBsub: B ⊆ Tx.
An exact proof term for the current goal is (andEL (B ⊆ Tx) (countable_set B) HB12).
We prove the intermediate claim HBcount: countable_set B.
An exact proof term for the current goal is (andER (B ⊆ Tx) (countable_set B) HB12).
We will prove ∃Fam : set, countable_set Fam ∧ (∀U ∈ Fam, open_in X Tx U) ∧ intersection_over_family X Fam = Sing x.
We use B to witness the existential quantifier.
Apply andI to the current goal.
We will prove countable_set B ∧ (∀U ∈ B, open_in X Tx U).
Apply andI to the current goal.
An exact proof term for the current goal is HBcount.
Let U be given.
Assume HU: U ∈ B.
We will prove topology_on X Tx ∧ U ∈ Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Apply HBsub to the current goal.
An exact proof term for the current goal is HU.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ intersection_over_family X B.
We will prove z ∈ Sing x.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∀U : set, U ∈ B → z0 ∈ U) z Hz).
We prove the intermediate claim Hzall: ∀U : set, U ∈ B → z ∈ U.
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ ∀U : set, U ∈ B → z0 ∈ U) z Hz).
Apply xm (z = x) to the current goal.
Assume Hzx: z = x.
rewrite the current goal using Hzx (from left to right).
An exact proof term for the current goal is (SingI x).
Assume Hzneq: z ≠ x.
Apply FalseE to the current goal.
We prove the intermediate claim HsubZ: {z} ⊆ X.
An exact proof term for the current goal is (singleton_subset z X HzX).
We prove the intermediate claim Hzfin: finite {z}.
An exact proof term for the current goal is (Sing_finite z).
We prove the intermediate claim Hzclosed: closed_in X Tx {z}.
An exact proof term for the current goal is (T1_space_finite_closed X Tx {z} HT1 HsubZ Hzfin).
Set Uc to be the term X ∖ {z}.
We prove the intermediate claim HUcopen: open_in X Tx Uc.
An exact proof term for the current goal is (open_of_closed_complement X Tx {z} Hzclosed).
We prove the intermediate claim HUcTx: Uc ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx Uc HUcopen).
We prove the intermediate claim Hxnotz: x ∉ {z}.
Assume Hxz: x ∈ {z}.
We prove the intermediate claim HxzEq: x = z.
An exact proof term for the current goal is (SingE z x Hxz).
We prove the intermediate claim HzxEq: z = x.
rewrite the current goal using HxzEq (from left to right).
Use reflexivity.
An exact proof term for the current goal is (Hzneq HzxEq).
We prove the intermediate claim HxUc: x ∈ Uc.
An exact proof term for the current goal is (setminusI X {z} x HxX Hxnotz).
We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ b ⊆ Uc.
An exact proof term for the current goal is (HBrefine Uc HUcTx HxUc).
Set b0 to be the term Eps_i (λb : set ⇒ b ∈ B ∧ b ⊆ Uc).
We prove the intermediate claim Hb0prop: b0 ∈ B ∧ b0 ⊆ Uc.
An exact proof term for the current goal is (Eps_i_ex (λb : set ⇒ b ∈ B ∧ b ⊆ Uc) Hexb).
We prove the intermediate claim Hb0B: b0 ∈ B.
An exact proof term for the current goal is (andEL (b0 ∈ B) (b0 ⊆ Uc) Hb0prop).
We prove the intermediate claim Hb0sub: b0 ⊆ Uc.
An exact proof term for the current goal is (andER (b0 ∈ B) (b0 ⊆ Uc) Hb0prop).
We prove the intermediate claim Hzz: z ∈ {z}.
An exact proof term for the current goal is (SingI z).
We prove the intermediate claim HznotUc: z ∉ Uc.
Assume HzUc: z ∈ Uc.
We prove the intermediate claim HznotZ: z ∉ {z}.
An exact proof term for the current goal is (setminusE2 X {z} z HzUc).
An exact proof term for the current goal is (HznotZ Hzz).
We prove the intermediate claim Hznotb0: z ∉ b0.
Assume Hzb: z ∈ b0.
We prove the intermediate claim HzUc: z ∈ Uc.
Apply Hb0sub to the current goal.
An exact proof term for the current goal is Hzb.
An exact proof term for the current goal is (HznotUc HzUc).
We prove the intermediate claim Hzb0: z ∈ b0.
An exact proof term for the current goal is (Hzall b0 Hb0B).
An exact proof term for the current goal is (Hznotb0 Hzb0).
Let z be given.
Assume Hz: z ∈ Sing x.
We will prove z ∈ intersection_over_family X B.
We prove the intermediate claim HzEq: z = x.
An exact proof term for the current goal is (SingE x z Hz).
We prove the intermediate claim HdefInt: intersection_over_family X B = {z0 ∈ X|∀U : set, U ∈ B → z0 ∈ U}.
Use reflexivity.
rewrite the current goal using HdefInt (from left to right).
Apply (SepI X (λz0 : set ⇒ ∀U : set, U ∈ B → z0 ∈ U) z) to the current goal.
rewrite the current goal using HzEq (from left to right).
An exact proof term for the current goal is HxX.
Let U be given.
Assume HU: U ∈ B.
rewrite the current goal using HzEq (from left to right).
An exact proof term for the current goal is (HBx U HU).
∎