Let U be given.

Assume HU: U ∈ topology_family_union I (const_space_family I X Tx).

We will prove U ∈ Tx.

We prove the intermediate claim Hdef: topology_family_union I (const_space_family I X Tx) = ⋃ {space_family_topology (const_space_family I X Tx) i|i ∈ I}.

Use reflexivity.

We prove the intermediate claim HU': U ∈ ⋃ {space_family_topology (const_space_family I X Tx) i|i ∈ I}.

rewrite the current goal using Hdef (from right to left).

An exact proof term for the current goal is HU.

Apply (UnionE_impred {space_family_topology (const_space_family I X Tx) i|i ∈ I} U HU') to the current goal.

Let A be given.

Assume HUA: U ∈ A.

Assume HA: A ∈ {space_family_topology (const_space_family I X Tx) i|i ∈ I}.

Apply (ReplE_impred I (λi0 : set ⇒ space_family_topology (const_space_family I X Tx) i0) A HA (U ∈ Tx)) to the current goal.

Let i be given.

Assume HiI: i ∈ I.

Assume HAeq: A = space_family_topology (const_space_family I X Tx) i.

We prove the intermediate claim HUAi: U ∈ space_family_topology (const_space_family I X Tx) i.

rewrite the current goal using HAeq (from right to left).

An exact proof term for the current goal is HUA.

rewrite the current goal using (space_family_topology_const_space_family I X Tx i HiI) (from right to left).

An exact proof term for the current goal is HUAi.

Let U be given.

Assume HU: U ∈ Tx.

We will prove U ∈ topology_family_union I (const_space_family I X Tx).

We prove the intermediate claim Hexi0: ∃i0 : set, i0 ∈ I.

Apply (xm (∃i0 : set, i0 ∈ I)) to the current goal.

Assume Hex.

An exact proof term for the current goal is Hex.

Assume Hno: ¬ (∃i0 : set, i0 ∈ I).

Apply FalseE to the current goal.

We prove the intermediate claim Hsub0: I ⊆ Empty.

Let i be given.

Assume HiI: i ∈ I.

We will prove i ∈ Empty.

Apply FalseE to the current goal.

We will prove False.

Apply Hno to the current goal.

We use i to witness the existential quantifier.

An exact proof term for the current goal is HiI.

We prove the intermediate claim HI0: I = Empty.

An exact proof term for the current goal is (Empty_Subq_eq I Hsub0).

An exact proof term for the current goal is (HIne HI0).

Apply Hexi0 to the current goal.

Let i0 be given.

Assume Hi0I: i0 ∈ I.

Set A0 to be the term space_family_topology (const_space_family I X Tx) i0.

We prove the intermediate claim HA0fam: A0 ∈ {space_family_topology (const_space_family I X Tx) i|i ∈ I}.

An exact proof term for the current goal is (ReplI I (λi : set ⇒ space_family_topology (const_space_family I X Tx) i) i0 Hi0I).

We prove the intermediate claim HUA0: U ∈ A0.

We prove the intermediate claim HA0def: A0 = space_family_topology (const_space_family I X Tx) i0.

Use reflexivity.

rewrite the current goal using HA0def (from left to right).

rewrite the current goal using (space_family_topology_const_space_family I X Tx i0 Hi0I) (from left to right).

An exact proof term for the current goal is HU.

We prove the intermediate claim Hdef: topology_family_union I (const_space_family I X Tx) = ⋃ {space_family_topology (const_space_family I X Tx) i|i ∈ I}.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

An exact proof term for the current goal is (UnionI {space_family_topology (const_space_family I X Tx) i|i ∈ I} U A0 HUA0 HA0fam).