Apply andI to the current goal.

Assume HJemp: J = Empty.

We prove the intermediate claim HEmptyPow: Empty ∈ 𝒫 S.

An exact proof term for the current goal is (Empty_In_Power S).

We prove the intermediate claim HEmptyFin: finite Empty.

An exact proof term for the current goal is finite_Empty.

We prove the intermediate claim HEmptyJ: Empty ∈ J.

An exact proof term for the current goal is (SepI (𝒫 S) (λF0 : set ⇒ finite F0) Empty HEmptyPow HEmptyFin).

We prove the intermediate claim HEmptyIn: Empty ∈ Empty.

rewrite the current goal using HJemp (from right to left) at position 2.

An exact proof term for the current goal is HEmptyJ.

An exact proof term for the current goal is (EmptyE Empty HEmptyIn).

We will prove partial_order_on J le.

We will prove relation_on le J ∧ (∀a : set, a ∈ J → (a,a) ∈ le) ∧ (∀a b : set, a ∈ J → b ∈ J → (a,b) ∈ le → (b,a) ∈ le → a = b) ∧ (∀a b c : set, a ∈ J → b ∈ J → c ∈ J → (a,b) ∈ le → (b,c) ∈ le → (a,c) ∈ le).

Apply andI to the current goal.

We will prove relation_on le J.

Let a and b be given.

Assume Hab: (a,b) ∈ le.

We will prove a ∈ J ∧ b ∈ J.

We prove the intermediate claim Hprod: (a,b) ∈ setprod J J.

An exact proof term for the current goal is (andEL ((a,b) ∈ setprod J J) (a ⊆ b) (inclusion_relE J a b Hab)).

We prove the intermediate claim Ha0: (a,b) 0 ∈ J.

An exact proof term for the current goal is (ap0_Sigma J (λ_ : set ⇒ J) (a,b) Hprod).

We prove the intermediate claim Hb1: (a,b) 1 ∈ J.

An exact proof term for the current goal is (ap1_Sigma J (λ_ : set ⇒ J) (a,b) Hprod).

Apply andI to the current goal.

rewrite the current goal using (tuple_2_0_eq a b) (from right to left).

An exact proof term for the current goal is Ha0.

rewrite the current goal using (tuple_2_1_eq a b) (from right to left).

An exact proof term for the current goal is Hb1.

Let a be given.

Assume HaJ: a ∈ J.

We will prove (a,a) ∈ le.

Apply (inclusion_relI J a a) to the current goal.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J J a a HaJ HaJ).

An exact proof term for the current goal is (Subq_ref a).

Let a and b be given.

Assume HaJ: a ∈ J.

Assume HbJ: b ∈ J.

Assume Hab: (a,b) ∈ le.

Assume Hba: (b,a) ∈ le.

We will prove a = b.

We prove the intermediate claim Habsub: a ⊆ b.

An exact proof term for the current goal is (andER ((a,b) ∈ setprod J J) (a ⊆ b) (inclusion_relE J a b Hab)).

We prove the intermediate claim Hbasub: b ⊆ a.

An exact proof term for the current goal is (andER ((b,a) ∈ setprod J J) (b ⊆ a) (inclusion_relE J b a Hba)).

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ a.

An exact proof term for the current goal is (Habsub x Hx).

Let x be given.

Assume Hx: x ∈ b.

An exact proof term for the current goal is (Hbasub x Hx).

Let a, b and c be given.

Assume HaJ: a ∈ J.

Assume HbJ: b ∈ J.

Assume HcJ: c ∈ J.

Assume Hab: (a,b) ∈ le.

Assume Hbc: (b,c) ∈ le.

We will prove (a,c) ∈ le.

We prove the intermediate claim Habsub: a ⊆ b.

An exact proof term for the current goal is (andER ((a,b) ∈ setprod J J) (a ⊆ b) (inclusion_relE J a b Hab)).

We prove the intermediate claim Hbcsub: b ⊆ c.

An exact proof term for the current goal is (andER ((b,c) ∈ setprod J J) (b ⊆ c) (inclusion_relE J b c Hbc)).

We prove the intermediate claim Hacsub: a ⊆ c.

An exact proof term for the current goal is (Subq_tra a b c Habsub Hbcsub).

Apply (inclusion_relI J a c) to the current goal.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J J a c HaJ HcJ).

An exact proof term for the current goal is Hacsub.

Let a and b be given.

Assume HaJ: a ∈ J.

Assume HbJ: b ∈ J.

We use (a ∪ b) to witness the existential quantifier.

We will prove (a ∪ b) ∈ J ∧ (a,a ∪ b) ∈ le ∧ (b,a ∪ b) ∈ le.

We prove the intermediate claim HabJ: (a ∪ b) ∈ J.

We prove the intermediate claim HaPow: a ∈ 𝒫 S.

An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) a HaJ).

We prove the intermediate claim HbPow: b ∈ 𝒫 S.

An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) b HbJ).

We prove the intermediate claim HaSub: a ⊆ S.

An exact proof term for the current goal is (PowerE S a HaPow).

We prove the intermediate claim HbSub: b ⊆ S.

An exact proof term for the current goal is (PowerE S b HbPow).

We prove the intermediate claim HabSub: (a ∪ b) ⊆ S.

An exact proof term for the current goal is (binunion_Subq_min a b S HaSub HbSub).

We prove the intermediate claim HabPow: (a ∪ b) ∈ 𝒫 S.

An exact proof term for the current goal is (PowerI S (a ∪ b) HabSub).

We prove the intermediate claim HaFin: finite a.

An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) a HaJ).

We prove the intermediate claim HbFin: finite b.

An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) b HbJ).

We prove the intermediate claim HabFin: finite (a ∪ b).

An exact proof term for the current goal is (binunion_finite a HaFin b HbFin).

An exact proof term for the current goal is (SepI (𝒫 S) (λF0 : set ⇒ finite F0) (a ∪ b) HabPow HabFin).

Apply andI to the current goal.

An exact proof term for the current goal is HabJ.

Apply (inclusion_relI J a (a ∪ b)) to the current goal.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J J a (a ∪ b) HaJ HabJ).

An exact proof term for the current goal is (binunion_Subq_1 a b).

Apply (inclusion_relI J b (a ∪ b)) to the current goal.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma J J b (a ∪ b) HbJ HabJ).

An exact proof term for the current goal is (binunion_Subq_2 a b).