Let X, Tx, Y and B be given.
Assume HTx: topology_on X Tx.
Assume HYsub: Y ⊆ X.
Assume HB: basis_on X B ∧ generated_topology X B = Tx.
We will prove basis_on Y {b ∩ Y|b ∈ B} ∧ generated_topology Y {b ∩ Y|b ∈ B} = subspace_topology X Tx Y.
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (generated_topology X B = Tx) HB).
We prove the intermediate claim HgenEq: generated_topology X B = Tx.
An exact proof term for the current goal is (andER (basis_on X B) (generated_topology X B = Tx) HB).
We prove the intermediate claim HtopSub: topology_on Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HYsub).
We prove the intermediate claim HCsub: ∀c ∈ {b ∩ Y|b ∈ B}, c ∈ subspace_topology X Tx Y.
Let c be given.
Assume HcC.
We prove the intermediate claim Hexb: ∃b ∈ B, c = b ∩ Y.
An exact proof term for the current goal is (ReplE B (λb0 : set ⇒ b0 ∩ Y) c HcC).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (c = b ∩ Y) Hbpair).
We prove the intermediate claim Hceq: c = b ∩ Y.
An exact proof term for the current goal is (andER (b ∈ B) (c = b ∩ Y) Hbpair).
We prove the intermediate claim HbGen: b ∈ generated_topology X B.
An exact proof term for the current goal is (generated_topology_contains_basis X B HBasis b HbB).
We prove the intermediate claim HbTx: b ∈ Tx.
We will prove b ∈ Tx.
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HbGen.
We prove the intermediate claim HcPowY: c ∈ 𝒫 Y.
Apply PowerI Y c to the current goal.
Let y be given.
Assume Hyc: y ∈ c.
We prove the intermediate claim HycBY: y ∈ b ∩ Y.
We will prove y ∈ b ∩ Y.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is Hyc.
An exact proof term for the current goal is (binintersectE2 b Y y HycBY).
We prove the intermediate claim HcProp: ∃V ∈ Tx, c = V ∩ Y.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbTx.
An exact proof term for the current goal is Hceq.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ ∃V ∈ Tx, U0 = V ∩ Y) c HcPowY HcProp).
We prove the intermediate claim Href: ∀U ∈ subspace_topology X Tx Y, ∀x ∈ U, ∃Cx ∈ {b ∩ Y|b ∈ B}, x ∈ Cx ∧ Cx ⊆ U.
Let U be given.
Assume HU: U ∈ subspace_topology X Tx Y.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HUprop: ∃V ∈ Tx, U = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HU).
Apply HUprop to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U = V ∩ Y) HVpair).
We prove the intermediate claim HUeq: U = V ∩ Y.
An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ Y) HVpair).
We prove the intermediate claim HxVY: x ∈ V ∩ Y.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 V Y x HxVY).
We prove the intermediate claim HVGen: V ∈ generated_topology X B.
We will prove V ∈ generated_topology X B.
rewrite the current goal using HgenEq (from left to right).
An exact proof term for the current goal is HVTx.
We prove the intermediate claim HVref: ∀z ∈ V, ∃b ∈ B, z ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀z0 ∈ U0, ∃b0 ∈ B, z0 ∈ b0 ∧ b0 ⊆ U0) V HVGen).
We prove the intermediate claim Hexb: ∃b ∈ B, x ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (HVref x HxV).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair2.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b ∧ b ⊆ V) Hbpair2).
We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ V) Hbpair2).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ V) Hbprop).
We prove the intermediate claim HbsubV: b ⊆ V.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ V) Hbprop).
Set Cx to be the term b ∩ Y.
We use Cx to witness the existential quantifier.
Apply andI to the current goal.
We will prove Cx ∈ {b0 ∩ Y|b0 ∈ B}.
An exact proof term for the current goal is (ReplI B (λb0 : set ⇒ b0 ∩ Y) b HbB).
Apply andI to the current goal.
We will prove x ∈ Cx.
An exact proof term for the current goal is (binintersectI b Y x Hxb HxY).
We will prove Cx ⊆ U.
Let y be given.
Assume HyCx: y ∈ Cx.
We prove the intermediate claim Hyb: y ∈ b.
An exact proof term for the current goal is (binintersectE1 b Y y HyCx).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (binintersectE2 b Y y HyCx).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (HbsubV y Hyb).
We prove the intermediate claim HyVY: y ∈ V ∩ Y.
An exact proof term for the current goal is (binintersectI V Y y HyV HyY).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HyVY.
An exact proof term for the current goal is (basis_refines_topology Y (subspace_topology X Tx Y) {b ∩ Y|b ∈ B} HtopSub HCsub Href).
∎