Let X, T, T', Y, U and U' be given.
Assume HXne: X ≠ Empty.
Assume HYne: Y ≠ Empty.
Assume HTx: topology_on X T.
Assume HTx': topology_on X T'.
Assume HTy: topology_on Y U.
Assume HTy': topology_on Y U'.
Assume Hfiner: T ⊆ T' ∧ U ⊆ U'.
We will prove product_topology X T Y U ⊆ product_topology X T' Y U'.
We prove the intermediate claim HTprod': topology_on (setprod X Y) (product_topology X T' Y U').
An exact proof term for the current goal is (product_topology_is_topology X T' Y U' HTx' HTy').
Apply (generated_topology_finer_weak (setprod X Y) (product_subbasis X T Y U) (product_topology X T' Y U') HTprod') to the current goal.
Let b be given.
Assume Hb: b ∈ product_subbasis X T Y U.
We will prove b ∈ product_topology X T' Y U'.
We prove the intermediate claim HexU0: ∃U0 ∈ T, b ∈ {rectangle_set U0 V|V ∈ U}.
An exact proof term for the current goal is (famunionE T (λU0 : set ⇒ {rectangle_set U0 V|V ∈ U}) b Hb).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0conj.
We prove the intermediate claim HU0T: U0 ∈ T.
An exact proof term for the current goal is (andEL (U0 ∈ T) (b ∈ {rectangle_set U0 V|V ∈ U}) HU0conj).
We prove the intermediate claim HbRepl: b ∈ {rectangle_set U0 V|V ∈ U}.
An exact proof term for the current goal is (andER (U0 ∈ T) (b ∈ {rectangle_set U0 V|V ∈ U}) HU0conj).
We prove the intermediate claim HexV0: ∃V0 ∈ U, b = rectangle_set U0 V0.
An exact proof term for the current goal is (ReplE U (λV0 : set ⇒ rectangle_set U0 V0) b HbRepl).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0conj.
We prove the intermediate claim HV0U: V0 ∈ U.
An exact proof term for the current goal is (andEL (V0 ∈ U) (b = rectangle_set U0 V0) HV0conj).
We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.
An exact proof term for the current goal is (andER (V0 ∈ U) (b = rectangle_set U0 V0) HV0conj).
We prove the intermediate claim HU0sub: U0 ∈ T'.
We prove the intermediate claim HTsub: T ⊆ T'.
An exact proof term for the current goal is (andEL (T ⊆ T') (U ⊆ U') Hfiner).
An exact proof term for the current goal is (HTsub U0 HU0T).
We prove the intermediate claim HV0sub: V0 ∈ U'.
We prove the intermediate claim HUsub: U ⊆ U'.
An exact proof term for the current goal is (andER (T ⊆ T') (U ⊆ U') Hfiner).
An exact proof term for the current goal is (HUsub V0 HV0U).
We prove the intermediate claim HBasis': basis_on (setprod X Y) (product_subbasis X T' Y U').
An exact proof term for the current goal is (product_subbasis_is_basis X T' Y U' HTx' HTy').
We prove the intermediate claim HbSub': b ∈ product_subbasis X T' Y U'.
We will prove b ∈ product_subbasis X T' Y U'.
We prove the intermediate claim HbV: rectangle_set U0 V0 ∈ {rectangle_set U0 V|V ∈ U'}.
An exact proof term for the current goal is (ReplI U' (λV1 : set ⇒ rectangle_set U0 V1) V0 HV0sub).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (famunionI T' (λU1 : set ⇒ {rectangle_set U1 V|V ∈ U'}) U0 (rectangle_set U0 V0) HU0sub HbV).
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X T' Y U') HBasis' b HbSub').
∎