Apply andI to the current goal.

We prove the intermediate claim H0o: 0 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 0 nat_0).

An exact proof term for the current goal is (elem_implies_nonempty ω 0 H0o).

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

An exact proof term for the current goal is HabSub.

An exact proof term for the current goal is HbaSub.

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

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 HabSub HbcSub).

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.

An exact proof term for the current goal is (omega_binunion a b HaJ HbJ).

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