We will prove topology_on abc_set top_abc_1 ∧ topology_on abc_set top_abc_2 ∧ topology_on abc_set top_abc_3 ∧ topology_on abc_set top_abc_4 ∧ topology_on abc_set top_abc_5 ∧ topology_on abc_set top_abc_6 ∧ topology_on abc_set top_abc_7 ∧ topology_on abc_set top_abc_8 ∧ topology_on abc_set top_abc_9 ∧ ∃finer_pairs : set, finer_pairs = {p ∈ 𝒫 (𝒫 (𝒫 abc_set))|∃T1 T2 : set, p = setprod T1 T2 ∧ (T1 = top_abc_1 ∨ T1 = top_abc_2 ∨ T1 = top_abc_3 ∨ T1 = top_abc_4 ∨ T1 = top_abc_5 ∨ T1 = top_abc_6 ∨ T1 = top_abc_7 ∨ T1 = top_abc_8 ∨ T1 = top_abc_9) ∧ (T2 = top_abc_1 ∨ T2 = top_abc_2 ∨ T2 = top_abc_3 ∨ T2 = top_abc_4 ∨ T2 = top_abc_5 ∨ T2 = top_abc_6 ∨ T2 = top_abc_7 ∨ T2 = top_abc_8 ∨ T2 = top_abc_9) ∧ T1 ⊆ T2}.
Apply andI to the current goal.
We prove the intermediate claim proof1: topology_on abc_set top_abc_1.
We prove the intermediate claim Ht1: top_abc_1 = indiscrete_topology abc_set.
Use reflexivity.
rewrite the current goal using Ht1 (from left to right).
An exact proof term for the current goal is (indiscrete_topology_on abc_set).
We prove the intermediate claim proof2: topology_on abc_set top_abc_2.
We prove the intermediate claim Ht2: top_abc_2 = discrete_topology abc_set.
Use reflexivity.
rewrite the current goal using Ht2 (from left to right).
An exact proof term for the current goal is (discrete_topology_on abc_set).
We prove the intermediate claim proof3: topology_on abc_set top_abc_3.
We prove the intermediate claim HA: {a_elt} ⊆ abc_set.
Let x be given.
Assume Hx: x ∈ {a_elt}.
We will prove x ∈ abc_set.
We prove the intermediate claim Hxeq: x = a_elt.
An exact proof term for the current goal is (SingE a_elt x Hx).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair a_elt b_elt) {c_elt} a_elt (UPairI1 a_elt b_elt)).
An exact proof term for the current goal is (topology_three_sets abc_set {a_elt} HA).
We prove the intermediate claim proof4: topology_on abc_set top_abc_4.
We prove the intermediate claim HB: {b_elt} ⊆ abc_set.
Let x be given.
Assume Hx: x ∈ {b_elt}.
We will prove x ∈ abc_set.
We prove the intermediate claim Hxeq: x = b_elt.
An exact proof term for the current goal is (SingE b_elt x Hx).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair a_elt b_elt) {c_elt} b_elt (UPairI2 a_elt b_elt)).
An exact proof term for the current goal is (topology_three_sets abc_set {b_elt} HB).
We prove the intermediate claim proof5: topology_on abc_set top_abc_5.
We prove the intermediate claim HC: {c_elt} ⊆ abc_set.
Let x be given.
Assume Hx: x ∈ {c_elt}.
We will prove x ∈ abc_set.
We prove the intermediate claim Hxeq: x = c_elt.
An exact proof term for the current goal is (SingE c_elt x Hx).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI2 (UPair a_elt b_elt) {c_elt} c_elt (SingI c_elt)).
An exact proof term for the current goal is (topology_three_sets abc_set {c_elt} HC).
We prove the intermediate claim proof6: topology_on abc_set top_abc_6.
We prove the intermediate claim HAB: (UPair a_elt b_elt) ⊆ abc_set.
Let x be given.
Assume Hx: x ∈ UPair a_elt b_elt.
We will prove x ∈ abc_set.
Apply (UPairE x a_elt b_elt Hx) to the current goal.
Assume Hxeq: x = a_elt.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair a_elt b_elt) {c_elt} a_elt (UPairI1 a_elt b_elt)).
Assume Hxeq: x = b_elt.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair a_elt b_elt) {c_elt} b_elt (UPairI2 a_elt b_elt)).
An exact proof term for the current goal is (topology_three_sets abc_set (UPair a_elt b_elt) HAB).
We prove the intermediate claim proof7: topology_on abc_set top_abc_7.
We prove the intermediate claim HAC: (UPair a_elt c_elt) ⊆ abc_set.
Let x be given.
Assume Hx: x ∈ UPair a_elt c_elt.
We will prove x ∈ abc_set.
Apply (UPairE x a_elt c_elt Hx) to the current goal.
Assume Hxeq: x = a_elt.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair a_elt b_elt) {c_elt} a_elt (UPairI1 a_elt b_elt)).
Assume Hxeq: x = c_elt.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI2 (UPair a_elt b_elt) {c_elt} c_elt (SingI c_elt)).
An exact proof term for the current goal is (topology_three_sets abc_set (UPair a_elt c_elt) HAC).
We prove the intermediate claim proof8: topology_on abc_set top_abc_8.
We prove the intermediate claim HBC: (UPair b_elt c_elt) ⊆ abc_set.
Let x be given.
Assume Hx: x ∈ UPair b_elt c_elt.
We will prove x ∈ abc_set.
Apply (UPairE x b_elt c_elt Hx) to the current goal.
Assume Hxeq: x = b_elt.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair a_elt b_elt) {c_elt} b_elt (UPairI2 a_elt b_elt)).
Assume Hxeq: x = c_elt.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (binunionI2 (UPair a_elt b_elt) {c_elt} c_elt (SingI c_elt)).
An exact proof term for the current goal is (topology_three_sets abc_set (UPair b_elt c_elt) HBC).
We prove the intermediate claim proof9: topology_on abc_set top_abc_9.
We prove the intermediate claim HAinAB: {a_elt} ⊆ UPair a_elt b_elt.
Let x be given.
Assume Hx: x ∈ {a_elt}.
We will prove x ∈ UPair a_elt b_elt.
We prove the intermediate claim Hxeq: x = a_elt.
An exact proof term for the current goal is (SingE a_elt x Hx).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (UPairI1 a_elt b_elt).
We prove the intermediate claim HABsubX: UPair a_elt b_elt ⊆ abc_set.
Let x be given.
Assume Hx: x ∈ UPair a_elt b_elt.
We will prove x ∈ abc_set.
An exact proof term for the current goal is (binunionI1 (UPair a_elt b_elt) {c_elt} x Hx).
An exact proof term for the current goal is (topology_chain_four_sets abc_set {a_elt} (UPair a_elt b_elt) HAinAB HABsubX).
We prove the intermediate claim H6: topology_on abc_set top_abc_1 ∧ topology_on abc_set top_abc_2 ∧ topology_on abc_set top_abc_3 ∧ topology_on abc_set top_abc_4 ∧ topology_on abc_set top_abc_5 ∧ topology_on abc_set top_abc_6.
Apply and6I to the current goal.
An exact proof term for the current goal is proof1.
An exact proof term for the current goal is proof2.
An exact proof term for the current goal is proof3.
An exact proof term for the current goal is proof4.
An exact proof term for the current goal is proof5.
An exact proof term for the current goal is proof6.
We prove the intermediate claim H7: (topology_on abc_set top_abc_1 ∧ topology_on abc_set top_abc_2 ∧ topology_on abc_set top_abc_3 ∧ topology_on abc_set top_abc_4 ∧ topology_on abc_set top_abc_5 ∧ topology_on abc_set top_abc_6) ∧ topology_on abc_set top_abc_7.
Apply andI to the current goal.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is proof7.
We prove the intermediate claim H8: ((topology_on abc_set top_abc_1 ∧ topology_on abc_set top_abc_2 ∧ topology_on abc_set top_abc_3 ∧ topology_on abc_set top_abc_4 ∧ topology_on abc_set top_abc_5 ∧ topology_on abc_set top_abc_6) ∧ topology_on abc_set top_abc_7) ∧ topology_on abc_set top_abc_8.
Apply andI to the current goal.
An exact proof term for the current goal is H7.
An exact proof term for the current goal is proof8.
We prove the intermediate claim H9: (((topology_on abc_set top_abc_1 ∧ topology_on abc_set top_abc_2 ∧ topology_on abc_set top_abc_3 ∧ topology_on abc_set top_abc_4 ∧ topology_on abc_set top_abc_5 ∧ topology_on abc_set top_abc_6) ∧ topology_on abc_set top_abc_7) ∧ topology_on abc_set top_abc_8) ∧ topology_on abc_set top_abc_9.
Apply andI to the current goal.
An exact proof term for the current goal is H8.
An exact proof term for the current goal is proof9.
An exact proof term for the current goal is H9.
We use {p ∈ 𝒫 (𝒫 (𝒫 abc_set))|∃T1 T2 : set, p = setprod T1 T2 ∧ (T1 = top_abc_1 ∨ T1 = top_abc_2 ∨ T1 = top_abc_3 ∨ T1 = top_abc_4 ∨ T1 = top_abc_5 ∨ T1 = top_abc_6 ∨ T1 = top_abc_7 ∨ T1 = top_abc_8 ∨ T1 = top_abc_9) ∧ (T2 = top_abc_1 ∨ T2 = top_abc_2 ∨ T2 = top_abc_3 ∨ T2 = top_abc_4 ∨ T2 = top_abc_5 ∨ T2 = top_abc_6 ∨ T2 = top_abc_7 ∨ T2 = top_abc_8 ∨ T2 = top_abc_9) ∧ T1 ⊆ T2} to witness the existential quantifier.
Use reflexivity.
∎