Let m be given.
Assume Hm.
We will prove {ordsucc m} ∈ order_topology_basis Zplus.
We prove the intermediate claim Hdef: order_topology_basis Zplus = (({I ∈ đ’Ģ Zplus|∃a ∈ Zplus, ∃b ∈ Zplus, I = {x ∈ Zplus|order_rel Zplus a x ∧ order_rel Zplus x b}} âˆĒ {I ∈ đ’Ģ Zplus|∃b ∈ Zplus, I = {x ∈ Zplus|order_rel Zplus x b}} âˆĒ {I ∈ đ’Ģ Zplus|∃a ∈ Zplus, I = {x ∈ Zplus|order_rel Zplus a x}}) âˆĒ {Zplus}).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply (SepI (đ’Ģ Zplus) (ÎģI : set ⇒ ∃a ∈ Zplus, ∃b ∈ Zplus, I = {x ∈ Zplus|order_rel Zplus a x ∧ order_rel Zplus x b}) {ordsucc m}) to the current goal.
Apply PowerI to the current goal.
Let x be given.
Assume Hx: x ∈ {ordsucc m}.
We will prove x ∈ Zplus.
We prove the intermediate claim HxEq: x = ordsucc m.
An exact proof term for the current goal is (SingE (ordsucc m) x Hx).
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is (Zplus_ordsucc_closed m Hm).
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
We use (ordsucc (ordsucc m)) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (Zplus_ordsucc_closed (ordsucc m) (Zplus_ordsucc_closed m Hm)).
We will prove {ordsucc m} = {x ∈ Zplus|order_rel Zplus m x ∧ order_rel Zplus x (ordsucc (ordsucc m))}.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ {ordsucc m}.
We will prove x ∈ {x ∈ Zplus|order_rel Zplus m x ∧ order_rel Zplus x (ordsucc (ordsucc m))}.
We prove the intermediate claim HxEq: x = ordsucc m.
An exact proof term for the current goal is (SingE (ordsucc m) x Hx).
Apply (SepI Zplus (Îģt : set ⇒ order_rel Zplus m t ∧ order_rel Zplus t (ordsucc (ordsucc m))) x) to the current goal.
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is (Zplus_ordsucc_closed m Hm).
rewrite the current goal using HxEq (from left to right).
Apply andI to the current goal.
We prove the intermediate claim Hmem1: m ∈ ordsucc m.
An exact proof term for the current goal is (ordsuccI2 m).
An exact proof term for the current goal is (iffER (order_rel Zplus m (ordsucc m)) (m ∈ ordsucc m) (order_rel_Zplus_iff_mem m (ordsucc m) Hm (Zplus_ordsucc_closed m Hm)) Hmem1).
We prove the intermediate claim Hmem2: ordsucc m ∈ ordsucc (ordsucc m).
An exact proof term for the current goal is (ordsuccI2 (ordsucc m)).
An exact proof term for the current goal is (iffER (order_rel Zplus (ordsucc m) (ordsucc (ordsucc m))) (ordsucc m ∈ ordsucc (ordsucc m)) (order_rel_Zplus_iff_mem (ordsucc m) (ordsucc (ordsucc m)) (Zplus_ordsucc_closed m Hm) (Zplus_ordsucc_closed (ordsucc m) (Zplus_ordsucc_closed m Hm))) Hmem2).
Let x be given.
Assume Hx: x ∈ {x ∈ Zplus|order_rel Zplus m x ∧ order_rel Zplus x (ordsucc (ordsucc m))}.
We will prove x ∈ {ordsucc m}.
We prove the intermediate claim HxZ: x ∈ Zplus.
An exact proof term for the current goal is (SepE1 Zplus (Îģt : set ⇒ order_rel Zplus m t ∧ order_rel Zplus t (ordsucc (ordsucc m))) x Hx).
We prove the intermediate claim Hconj: order_rel Zplus m x ∧ order_rel Zplus x (ordsucc (ordsucc m)).
An exact proof term for the current goal is (SepE2 Zplus (Îģt : set ⇒ order_rel Zplus m t ∧ order_rel Zplus t (ordsucc (ordsucc m))) x Hx).
We prove the intermediate claim Hrel1: order_rel Zplus m x.
An exact proof term for the current goal is (andEL (order_rel Zplus m x) (order_rel Zplus x (ordsucc (ordsucc m))) Hconj).
We prove the intermediate claim Hrel2: order_rel Zplus x (ordsucc (ordsucc m)).
An exact proof term for the current goal is (andER (order_rel Zplus m x) (order_rel Zplus x (ordsucc (ordsucc m))) Hconj).
We prove the intermediate claim Hmemb: m ∈ x.
An exact proof term for the current goal is (iffEL (order_rel Zplus m x) (m ∈ x) (order_rel_Zplus_iff_mem m x Hm HxZ) Hrel1).
We prove the intermediate claim HbZ: ordsucc (ordsucc m) ∈ Zplus.
An exact proof term for the current goal is (Zplus_ordsucc_closed (ordsucc m) (Zplus_ordsucc_closed m Hm)).
We prove the intermediate claim HxInb: x ∈ ordsucc (ordsucc m).
An exact proof term for the current goal is (iffEL (order_rel Zplus x (ordsucc (ordsucc m))) (x ∈ ordsucc (ordsucc m)) (order_rel_Zplus_iff_mem x (ordsucc (ordsucc m)) HxZ HbZ) Hrel2).
We prove the intermediate claim Hcase: x ∈ ordsucc m ∨ x = ordsucc m.
An exact proof term for the current goal is (ordsuccE (ordsucc m) x HxInb).
We prove the intermediate claim HxEq: x = ordsucc m.
Apply (Hcase (x = ordsucc m)) to the current goal.
Assume HxIn1: x ∈ ordsucc m.
Apply FalseE to the current goal.
We prove the intermediate claim Hcase2: x ∈ m ∨ x = m.
An exact proof term for the current goal is (ordsuccE m x HxIn1).
We prove the intermediate claim HxInm: x ∈ m.
Apply (Hcase2 (x ∈ m)) to the current goal.
Assume Hxm.
An exact proof term for the current goal is Hxm.
Assume Hxeq.
Apply FalseE to the current goal.
We prove the intermediate claim Hmm: m ∈ m.
We will prove m ∈ m.
rewrite the current goal using Hxeq (from right to left) at position 2.
An exact proof term for the current goal is Hmemb.
An exact proof term for the current goal is (In_irref m Hmm).
An exact proof term for the current goal is (In_no2cycle m x Hmemb HxInm).
Assume Hxeq.
An exact proof term for the current goal is Hxeq.
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is (SingI (ordsucc m)).
∎