Let X, Tx and Basis be given.
Assume Hsc: second_countable_space X Tx.
Assume HBg: basis_generates X Basis Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hsc).
We prove the intermediate claim HexB: ∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hsc).
We prove the intermediate claim HBasisOn: basis_on X Basis.
An exact proof term for the current goal is (andEL (basis_on X Basis) (generated_topology X Basis = Tx) HBg).
We prove the intermediate claim HBasisEq: generated_topology X Basis = Tx.
An exact proof term for the current goal is (andER (basis_on X Basis) (generated_topology X Basis = Tx) HBg).
Apply HexB to the current goal.
Let Bx be given.
Assume HBxAll: basis_on X Bx ∧ countable_set Bx ∧ basis_generates X Bx Tx.
We prove the intermediate claim HBxMid: (basis_on X Bx ∧ countable_set Bx) ∧ basis_generates X Bx Tx.
An exact proof term for the current goal is HBxAll.
We prove the intermediate claim HBxPair: basis_on X Bx ∧ countable_set Bx.
An exact proof term for the current goal is (andEL (basis_on X Bx ∧ countable_set Bx) (basis_generates X Bx Tx) HBxMid).
We prove the intermediate claim HBxBasis: basis_on X Bx.
An exact proof term for the current goal is (andEL (basis_on X Bx) (countable_set Bx) HBxPair).
We prove the intermediate claim HBxCount: countable_set Bx.
An exact proof term for the current goal is (andER (basis_on X Bx) (countable_set Bx) HBxPair).
We prove the intermediate claim HBxGener: basis_generates X Bx Tx.
An exact proof term for the current goal is (andER (basis_on X Bx ∧ countable_set Bx) (basis_generates X Bx Tx) HBxMid).
We prove the intermediate claim HBxEq: generated_topology X Bx = Tx.
An exact proof term for the current goal is (andER (basis_on X Bx) (generated_topology X Bx = Tx) HBxGener).
Set PairB to be the term ∑b1 ∈ Bx, Bx.
Set P to be the term {z ∈ PairB|∃c : set, c ∈ Basis ∧ z 0 ⊆ c ∧ c ⊆ z 1}.
Set choose to be the term λz : set ⇒ Eps_i (λc : set ⇒ c ∈ Basis ∧ z 0 ⊆ c ∧ c ⊆ z 1) of type set → set.
Set CountableSub to be the term {choose z|z ∈ P}.
We prove the intermediate claim HPairBcount: countable PairB.
Set Y to be the term λ_ : set ⇒ Bx of type set → set.
We prove the intermediate claim HY: ∀b1 : set, b1 ∈ Bx → countable (Y b1).
Let b1 be given.
Assume _.
An exact proof term for the current goal is HBxCount.
An exact proof term for the current goal is (Sigma_countable Bx HBxCount Y HY).
We prove the intermediate claim HPsub: P ⊆ PairB.
Let z be given.
Assume HzP: z ∈ P.
An exact proof term for the current goal is (SepE1 PairB (λz0 : set ⇒ ∃c : set, c ∈ Basis ∧ z0 0 ⊆ c ∧ c ⊆ z0 1) z HzP).
We prove the intermediate claim HPcount: countable P.
An exact proof term for the current goal is (Subq_countable P PairB HPairBcount HPsub).
We prove the intermediate claim HCountSubCount: countable CountableSub.
An exact proof term for the current goal is (countable_image P HPcount choose).
We prove the intermediate claim HCountSubSubBasis: CountableSub ⊆ Basis.
Let c be given.
Assume Hc: c ∈ CountableSub.
Apply (ReplE_impred P choose c Hc) to the current goal.
Let z be given.
Assume HzP: z ∈ P.
Assume Hceq: c = choose z.
We prove the intermediate claim HzPprop: ∃c0 : set, c0 ∈ Basis ∧ z 0 ⊆ c0 ∧ c0 ⊆ z 1.
An exact proof term for the current goal is (SepE2 PairB (λz0 : set ⇒ ∃c0 : set, c0 ∈ Basis ∧ z0 0 ⊆ c0 ∧ c0 ⊆ z0 1) z HzP).
We prove the intermediate claim HchooseProp: choose z ∈ Basis ∧ z 0 ⊆ (choose z) ∧ (choose z) ⊆ z 1.
An exact proof term for the current goal is (Eps_i_ex (λc0 : set ⇒ c0 ∈ Basis ∧ z 0 ⊆ c0 ∧ c0 ⊆ z 1) HzPprop).
rewrite the current goal using Hceq (from left to right).
We prove the intermediate claim Htmp: choose z ∈ Basis ∧ z 0 ⊆ choose z.
An exact proof term for the current goal is (andEL (choose z ∈ Basis ∧ z 0 ⊆ choose z) (choose z ⊆ z 1) HchooseProp).
An exact proof term for the current goal is (andEL (choose z ∈ Basis) (z 0 ⊆ choose z) Htmp).
We prove the intermediate claim HCountSubOpen: ∀c ∈ CountableSub, c ∈ Tx.
Let c be given.
Assume Hc: c ∈ CountableSub.
We prove the intermediate claim HcBasis: c ∈ Basis.
An exact proof term for the current goal is (HCountSubSubBasis c Hc).
We prove the intermediate claim HcGen: c ∈ generated_topology X Basis.
An exact proof term for the current goal is (generated_topology_contains_basis X Basis HBasisOn c HcBasis).
We will prove c ∈ Tx.
rewrite the current goal using HBasisEq (from right to left).
An exact proof term for the current goal is HcGen.
We prove the intermediate claim HCountSubRefines: ∀U ∈ Tx, ∀x ∈ U, ∃Cx ∈ CountableSub, x ∈ Cx ∧ Cx ⊆ U.
Let U be given.
Assume HU: U ∈ Tx.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HUGenB: U ∈ generated_topology X Bx.
We will prove U ∈ generated_topology X Bx.
rewrite the current goal using HBxEq (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUpropB: ∀x0 ∈ U, ∃b ∈ Bx, x0 ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ Bx, x0 ∈ b ∧ b ⊆ U0) U HUGenB).
We prove the intermediate claim Hexb2: ∃b2 ∈ Bx, x ∈ b2 ∧ b2 ⊆ U.
An exact proof term for the current goal is (HUpropB x HxU).
Apply Hexb2 to the current goal.
Let b2 be given.
Assume Hb2pair.
We prove the intermediate claim Hb2Bx: b2 ∈ Bx.
An exact proof term for the current goal is (andEL (b2 ∈ Bx) (x ∈ b2 ∧ b2 ⊆ U) Hb2pair).
We prove the intermediate claim Hb2prop: x ∈ b2 ∧ b2 ⊆ U.
An exact proof term for the current goal is (andER (b2 ∈ Bx) (x ∈ b2 ∧ b2 ⊆ U) Hb2pair).
We prove the intermediate claim Hxb2: x ∈ b2.
An exact proof term for the current goal is (andEL (x ∈ b2) (b2 ⊆ U) Hb2prop).
We prove the intermediate claim Hb2subU: b2 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b2) (b2 ⊆ U) Hb2prop).
We prove the intermediate claim Hb2GenB: b2 ∈ generated_topology X Bx.
An exact proof term for the current goal is (generated_topology_contains_basis X Bx HBxBasis b2 Hb2Bx).
We prove the intermediate claim Hb2Tx: b2 ∈ Tx.
We will prove b2 ∈ Tx.
rewrite the current goal using HBxEq (from right to left).
An exact proof term for the current goal is Hb2GenB.
We prove the intermediate claim Hb2GenC: b2 ∈ generated_topology X Basis.
We will prove b2 ∈ generated_topology X Basis.
rewrite the current goal using HBasisEq (from left to right).
An exact proof term for the current goal is Hb2Tx.
We prove the intermediate claim Hb2propC: ∀x0 ∈ b2, ∃c0 ∈ Basis, x0 ∈ c0 ∧ c0 ⊆ b2.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃c0 ∈ Basis, x0 ∈ c0 ∧ c0 ⊆ U0) b2 Hb2GenC).
We prove the intermediate claim Hexc0: ∃c0 ∈ Basis, x ∈ c0 ∧ c0 ⊆ b2.
An exact proof term for the current goal is (Hb2propC x Hxb2).
Apply Hexc0 to the current goal.
Let c0 be given.
Assume Hc0pair.
We prove the intermediate claim Hc0Basis: c0 ∈ Basis.
An exact proof term for the current goal is (andEL (c0 ∈ Basis) (x ∈ c0 ∧ c0 ⊆ b2) Hc0pair).
We prove the intermediate claim Hc0prop: x ∈ c0 ∧ c0 ⊆ b2.
An exact proof term for the current goal is (andER (c0 ∈ Basis) (x ∈ c0 ∧ c0 ⊆ b2) Hc0pair).
We prove the intermediate claim Hxc0: x ∈ c0.
An exact proof term for the current goal is (andEL (x ∈ c0) (c0 ⊆ b2) Hc0prop).
We prove the intermediate claim Hc0subb2: c0 ⊆ b2.
An exact proof term for the current goal is (andER (x ∈ c0) (c0 ⊆ b2) Hc0prop).
We prove the intermediate claim Hc0GenC: c0 ∈ generated_topology X Basis.
An exact proof term for the current goal is (generated_topology_contains_basis X Basis HBasisOn c0 Hc0Basis).
We prove the intermediate claim Hc0Tx: c0 ∈ Tx.
We will prove c0 ∈ Tx.
rewrite the current goal using HBasisEq (from right to left).
An exact proof term for the current goal is Hc0GenC.
We prove the intermediate claim Hc0GenB: c0 ∈ generated_topology X Bx.
We will prove c0 ∈ generated_topology X Bx.
rewrite the current goal using HBxEq (from left to right).
An exact proof term for the current goal is Hc0Tx.
We prove the intermediate claim Hc0propB: ∀x0 ∈ c0, ∃b ∈ Bx, x0 ∈ b ∧ b ⊆ c0.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ Bx, x0 ∈ b ∧ b ⊆ U0) c0 Hc0GenB).
We prove the intermediate claim Hexb1: ∃b1 ∈ Bx, x ∈ b1 ∧ b1 ⊆ c0.
An exact proof term for the current goal is (Hc0propB x Hxc0).
Apply Hexb1 to the current goal.
Let b1 be given.
Assume Hb1pair.
We prove the intermediate claim Hb1Bx: b1 ∈ Bx.
An exact proof term for the current goal is (andEL (b1 ∈ Bx) (x ∈ b1 ∧ b1 ⊆ c0) Hb1pair).
We prove the intermediate claim Hb1prop: x ∈ b1 ∧ b1 ⊆ c0.
An exact proof term for the current goal is (andER (b1 ∈ Bx) (x ∈ b1 ∧ b1 ⊆ c0) Hb1pair).
We prove the intermediate claim Hxb1: x ∈ b1.
An exact proof term for the current goal is (andEL (x ∈ b1) (b1 ⊆ c0) Hb1prop).
We prove the intermediate claim Hb1subc0: b1 ⊆ c0.
An exact proof term for the current goal is (andER (x ∈ b1) (b1 ⊆ c0) Hb1prop).
Set z to be the term (b1,b2).
We prove the intermediate claim HzPairB: z ∈ PairB.
An exact proof term for the current goal is (tuple_2_Sigma Bx (λ_ : set ⇒ Bx) b1 Hb1Bx b2 Hb2Bx).
We prove the intermediate claim HzP: z ∈ P.
We prove the intermediate claim Hexc: ∃c : set, c ∈ Basis ∧ z 0 ⊆ c ∧ c ⊆ z 1.
We use c0 to witness the existential quantifier.
Apply andI to the current goal.
We will prove c0 ∈ Basis ∧ z 0 ⊆ c0.
Apply andI to the current goal.
An exact proof term for the current goal is Hc0Basis.
rewrite the current goal using (tuple_2_0_eq b1 b2) (from left to right).
An exact proof term for the current goal is Hb1subc0.
rewrite the current goal using (tuple_2_1_eq b1 b2) (from left to right).
An exact proof term for the current goal is Hc0subb2.
Apply (SepI PairB (λz0 : set ⇒ ∃c : set, c ∈ Basis ∧ z0 0 ⊆ c ∧ c ⊆ z0 1) z HzPairB Hexc) to the current goal.
Set Cx to be the term choose z.
We use Cx to witness the existential quantifier.
Apply andI to the current goal.
We will prove Cx ∈ CountableSub.
An exact proof term for the current goal is (ReplI P choose z HzP).
Apply andI to the current goal.
We prove the intermediate claim HzPprop: ∃c : set, c ∈ Basis ∧ z 0 ⊆ c ∧ c ⊆ z 1.
An exact proof term for the current goal is (SepE2 PairB (λz0 : set ⇒ ∃c : set, c ∈ Basis ∧ z0 0 ⊆ c ∧ c ⊆ z0 1) z HzP).
We prove the intermediate claim HchooseProp: choose z ∈ Basis ∧ z 0 ⊆ choose z ∧ choose z ⊆ z 1.
An exact proof term for the current goal is (Eps_i_ex (λc : set ⇒ c ∈ Basis ∧ z 0 ⊆ c ∧ c ⊆ z 1) HzPprop).
We prove the intermediate claim Hb1subCx: z 0 ⊆ Cx.
We prove the intermediate claim Htmp: choose z ∈ Basis ∧ z 0 ⊆ choose z.
An exact proof term for the current goal is (andEL (choose z ∈ Basis ∧ z 0 ⊆ choose z) (choose z ⊆ z 1) HchooseProp).
We prove the intermediate claim Hz0sub: z 0 ⊆ choose z.
An exact proof term for the current goal is (andER (choose z ∈ Basis) (z 0 ⊆ choose z) Htmp).
We prove the intermediate claim HCxDef: Cx = choose z.
Use reflexivity.
rewrite the current goal using HCxDef (from left to right).
An exact proof term for the current goal is Hz0sub.
We prove the intermediate claim Hz0eq: z 0 = b1.
An exact proof term for the current goal is (tuple_2_0_eq b1 b2).
We prove the intermediate claim Hxz0: x ∈ z 0.
rewrite the current goal using Hz0eq (from left to right).
An exact proof term for the current goal is Hxb1.
An exact proof term for the current goal is (Hb1subCx x Hxz0).
We prove the intermediate claim HzPprop: ∃c : set, c ∈ Basis ∧ z 0 ⊆ c ∧ c ⊆ z 1.
An exact proof term for the current goal is (SepE2 PairB (λz0 : set ⇒ ∃c : set, c ∈ Basis ∧ z0 0 ⊆ c ∧ c ⊆ z0 1) z HzP).
We prove the intermediate claim HchooseProp: choose z ∈ Basis ∧ z 0 ⊆ choose z ∧ choose z ⊆ z 1.
An exact proof term for the current goal is (Eps_i_ex (λc : set ⇒ c ∈ Basis ∧ z 0 ⊆ c ∧ c ⊆ z 1) HzPprop).
We prove the intermediate claim HCxsubb2: Cx ⊆ z 1.
We prove the intermediate claim HCxDef: Cx = choose z.
Use reflexivity.
rewrite the current goal using HCxDef (from left to right).
An exact proof term for the current goal is (andER (choose z ∈ Basis ∧ z 0 ⊆ choose z) (choose z ⊆ z 1) HchooseProp).
We prove the intermediate claim HCxsubb2': Cx ⊆ b2.
We prove the intermediate claim Hz1eq: z 1 = b2.
An exact proof term for the current goal is (tuple_2_1_eq b1 b2).
Let y be given.
Assume Hy: y ∈ Cx.
We will prove y ∈ b2.
We prove the intermediate claim Hyz1: y ∈ z 1.
An exact proof term for the current goal is (HCxsubb2 y Hy).
rewrite the current goal using Hz1eq (from right to left).
An exact proof term for the current goal is Hyz1.
An exact proof term for the current goal is (Subq_tra Cx b2 U HCxsubb2' Hb2subU).
We prove the intermediate claim HCountSubBasisEq: basis_on X CountableSub ∧ generated_topology X CountableSub = Tx.
An exact proof term for the current goal is (basis_refines_topology X Tx CountableSub HTx HCountSubOpen HCountSubRefines).
We prove the intermediate claim HCountSubGener: basis_generates X CountableSub Tx.
We will prove basis_on X CountableSub ∧ generated_topology X CountableSub = Tx.
An exact proof term for the current goal is HCountSubBasisEq.
We use CountableSub to witness the existential quantifier.
We will prove CountableSub ⊆ Basis ∧ countable CountableSub ∧ basis_generates X CountableSub Tx.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HCountSubSubBasis.
An exact proof term for the current goal is HCountSubCount.
An exact proof term for the current goal is HCountSubGener.
∎