Apply andI to the current goal.

We prove the intermediate claim H0J: Empty ∈ J.

We will prove Empty ∈ {F ∈ 𝒫 I|finite F}.

Apply (SepI (𝒫 I) (λF : set ⇒ finite F) Empty) to the current goal.

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

An exact proof term for the current goal is finite_Empty.

An exact proof term for the current goal is (elem_implies_nonempty J Empty H0J).

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 prove the intermediate claim HabE: (a,b) ∈ setprod J J ∧ a ⊆ b.

An exact proof term for the current goal is (inclusion_relE J a b Hab).

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

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

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

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

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

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

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 HaJ0.

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

An exact proof term for the current goal is HbJ1.

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 Hasub: 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 Hbsub: 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.

An exact proof term for the current goal is Hasub.

An exact proof term for the current goal is Hbsub.

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 Hasub: 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 Hbsub: 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)).

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 (Subq_tra a b c Hasub Hbsub).

Let a and b be given.

Assume HaJ: a ∈ J.

Assume HbJ: b ∈ J.

Set c to be the term a ∪ b.

We use c to witness the existential quantifier.

We prove the intermediate claim HcJ: c ∈ J.

We prove the intermediate claim HaPI: a ∈ 𝒫 I.

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

We prove the intermediate claim HbPI: b ∈ 𝒫 I.

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

We prove the intermediate claim Hafin: finite a.

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

We prove the intermediate claim Hbfin: finite b.

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

We prove the intermediate claim HaSubI: a ⊆ I.

An exact proof term for the current goal is (PowerE I a HaPI).

We prove the intermediate claim HbSubI: b ⊆ I.

An exact proof term for the current goal is (PowerE I b HbPI).

We prove the intermediate claim HcSubI: c ⊆ I.

An exact proof term for the current goal is (binunion_Subq_min a b I HaSubI HbSubI).

We prove the intermediate claim HcPI: c ∈ 𝒫 I.

An exact proof term for the current goal is (PowerI I c HcSubI).

We prove the intermediate claim Hcfin: finite c.

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 (𝒫 I) (λF : set ⇒ finite F) c HcPI Hcfin).

Apply andI to the current goal.

An exact proof term for the current goal is HcJ.

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 (binunion_Subq_1 a b).

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

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

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