We will prove {ordsucc 0} ∈ 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 binunionI2 to the current goal.
Apply (SepI (đ’Ģ Zplus) (ÎģI : set ⇒ ∃b0 ∈ Zplus, I = {x ∈ Zplus|order_rel Zplus x b0}) {ordsucc 0}) to the current goal.
Apply PowerI to the current goal.
Let x be given.
Assume Hx: x ∈ {ordsucc 0}.
We will prove x ∈ Zplus.
We prove the intermediate claim HxEq: x = ordsucc 0.
An exact proof term for the current goal is (SingE (ordsucc 0) x Hx).
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is one_in_Zplus.
We use (ordsucc (ordsucc 0)) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is two_in_Zplus.
We will prove {ordsucc 0} = {x ∈ Zplus|order_rel Zplus x (ordsucc (ordsucc 0))}.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ {ordsucc 0}.
We will prove x ∈ {x ∈ Zplus|order_rel Zplus x (ordsucc (ordsucc 0))}.
We prove the intermediate claim HxEq: x = ordsucc 0.
An exact proof term for the current goal is (SingE (ordsucc 0) x Hx).
Apply (SepI Zplus (Îģt : set ⇒ order_rel Zplus t (ordsucc (ordsucc 0))) x) to the current goal.
rewrite the current goal using HxEq (from left to right).
An exact proof term for the current goal is one_in_Zplus.
rewrite the current goal using HxEq (from left to right).
We prove the intermediate claim Hmem: ordsucc 0 ∈ ordsucc (ordsucc 0).
An exact proof term for the current goal is (ordsuccI2 (ordsucc 0)).
An exact proof term for the current goal is (iffER (order_rel Zplus (ordsucc 0) (ordsucc (ordsucc 0))) (ordsucc 0 ∈ ordsucc (ordsucc 0)) (order_rel_Zplus_iff_mem (ordsucc 0) (ordsucc (ordsucc 0)) one_in_Zplus two_in_Zplus) Hmem).
Let x be given.
Assume Hx: x ∈ {x ∈ Zplus|order_rel Zplus x (ordsucc (ordsucc 0))}.
We will prove x ∈ {ordsucc 0}.
We prove the intermediate claim HxZ: x ∈ Zplus.
An exact proof term for the current goal is (SepE1 Zplus (Îģt : set ⇒ order_rel Zplus t (ordsucc (ordsucc 0))) x Hx).
We prove the intermediate claim Hrel: order_rel Zplus x (ordsucc (ordsucc 0)).
An exact proof term for the current goal is (SepE2 Zplus (Îģt : set ⇒ order_rel Zplus t (ordsucc (ordsucc 0))) x Hx).
We prove the intermediate claim Hmem: x ∈ ordsucc (ordsucc 0).
An exact proof term for the current goal is (iffEL (order_rel Zplus x (ordsucc (ordsucc 0))) (x ∈ ordsucc (ordsucc 0)) (order_rel_Zplus_iff_mem x (ordsucc (ordsucc 0)) HxZ two_in_Zplus) Hrel).
We prove the intermediate claim HxNe0: x ≠ 0.
An exact proof term for the current goal is (Zplus_mem_nonzero x HxZ).
We prove the intermediate claim Hcase: x ∈ ordsucc 0 ∨ x = ordsucc 0.
An exact proof term for the current goal is (ordsuccE (ordsucc 0) x Hmem).
We prove the intermediate claim HxEq1: x = ordsucc 0.
Apply (Hcase (x = ordsucc 0)) to the current goal.
Assume HxIn1: x ∈ ordsucc 0.
Apply FalseE to the current goal.
We prove the intermediate claim Hcase0: x ∈ 0 ∨ x = 0.
An exact proof term for the current goal is (ordsuccE 0 x HxIn1).
We prove the intermediate claim Hx0: x = 0.
Apply (Hcase0 (x = 0)) to the current goal.
Assume HxIn0: x ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxIn0).
Assume Hx0.
An exact proof term for the current goal is Hx0.
An exact proof term for the current goal is (HxNe0 Hx0).
Assume HxEq.
An exact proof term for the current goal is HxEq.
rewrite the current goal using HxEq1 (from left to right).
An exact proof term for the current goal is (SingI (ordsucc 0)).
∎