Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: x1 ⊆ x0.

Assume H1: finite x0.

Apply H1 with finite x1.

Let x2 of type ι be given.

Assume H2: (λ x3 . and (x3 ∈ omega) (equip x0 x3)) x2.

Apply H2 with finite x1.

Assume H3: x2 ∈ omega.

Assume H4: equip x0 x2.

Claim L5: atleastp x1 x2

Apply atleastp_tra with x1, x0, x2 leaving 2 subgoals.

Apply Subq_atleastp with x1, x0.

The subproof is completed by applying H0.

Apply equip_atleastp with x0, x2.

The subproof is completed by applying H4.

Apply unknownprop_8c033b5532b5ecb975cda388e43db69e003e5159ad10f70a2cd946604e0cb0f6 with x1, x2, finite x1 leaving 2 subgoals.

The subproof is completed by applying L5.

Let x3 of type ι be given.

Assume H6: x3 ⊆ x2.

Assume H7: equip x1 x3.

Apply unknownprop_8b06455b71193e811b862103510dd9b581a1532bb6bb579790ac66d65ff3dd3c with x2, x3, finite x1 leaving 3 subgoals.

Apply omega_nat_p with x2.

The subproof is completed by applying H3.

The subproof is completed by applying H6.

Let x4 of type ι be given.

Assume H8: (λ x5 . and (and (nat_p x5) (x5 ⊆ x2)) (equip x3 x5)) x4.

Apply H8 with finite x1.

Assume H9: and (nat_p x4) (x4 ⊆ x2).

Apply H9 with equip x3 x4 ⟶ finite x1.

Assume H10: nat_p x4.

Assume H11: x4 ⊆ x2.

Assume H12: equip x3 x4.

Let x5 of type ο be given.

Assume H13: ∀ x6 . and (x6 ∈ omega) (equip x1 x6) ⟶ x5.

Apply H13 with x4.

Apply andI with x4 ∈ omega, equip x1 x4 leaving 2 subgoals.

Apply nat_p_omega with x4.

The subproof is completed by applying H10.

Apply equip_tra with x1, x3, x4 leaving 2 subgoals.

The subproof is completed by applying H7.

The subproof is completed by applying H12.

■

Proofgold Proof