Let x0 of type ι be given.

Apply unknownprop_1ad59b907936b2a3f58528f51c1b27d67d89955cf0fe7705f9645ea773142ed8 with x0, ∃ x1 . ∀ x2 . iff (prim1 x2 x1) (Subq x2 x0).

Let x1 of type ι be given.

Assume H0: (λ x2 . and (and (and (prim1 x0 x2) (∀ x3 x4 . prim1 x3 x2 ⟶ Subq x4 x3 ⟶ prim1 x4 x2)) (∀ x3 . prim1 x3 x2 ⟶ ∃ x4 . and (prim1 x4 x2) (∀ x5 . Subq x5 x3 ⟶ prim1 x5 x4))) (∀ x3 . Subq x3 x2 ⟶ or (c2e41.. x3 x2) (prim1 x3 x2))) x1.

Apply H0 with ∃ x2 . ∀ x3 . iff (prim1 x3 x2) (Subq x3 x0).

Assume H1: and (and (prim1 x0 x1) (∀ x2 x3 . prim1 x2 x1 ⟶ Subq x3 x2 ⟶ prim1 x3 x1)) (∀ x2 . prim1 x2 x1 ⟶ ∃ x3 . and (prim1 x3 x1) (∀ x4 . Subq x4 x2 ⟶ prim1 x4 x3)).

Apply H1 with (∀ x2 . Subq x2 x1 ⟶ or (c2e41.. x2 x1) (prim1 x2 x1)) ⟶ ∃ x2 . ∀ x3 . iff (prim1 x3 x2) (Subq x3 x0).

Assume H2: and (prim1 x0 x1) (∀ x2 x3 . prim1 x2 x1 ⟶ Subq x3 x2 ⟶ prim1 x3 x1).

Apply H2 with (∀ x2 . prim1 x2 x1 ⟶ ∃ x3 . and (prim1 x3 x1) (∀ x4 . Subq x4 x2 ⟶ prim1 x4 x3)) ⟶ (∀ x2 . Subq x2 x1 ⟶ or (c2e41.. x2 x1) (prim1 x2 x1)) ⟶ ∃ x2 . ∀ x3 . iff (prim1 x3 x2) (Subq x3 x0).

Assume H3: prim1 x0 x1.

Assume H4: ∀ x2 x3 . prim1 x2 x1 ⟶ Subq x3 x2 ⟶ prim1 x3 x1.

Assume H5: ∀ x2 . prim1 x2 x1 ⟶ ∃ x3 . and (prim1 x3 x1) (∀ x4 . Subq x4 x2 ⟶ prim1 x4 x3).

Assume H6: ∀ x2 . Subq x2 x1 ⟶ or (c2e41.. x2 x1) (prim1 x2 x1).

Apply H5 with x0, ∃ x2 . ∀ x3 . iff (prim1 x3 x2) (Subq x3 x0) leaving 2 subgoals.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H7: (λ x3 . and (prim1 x3 x1) (∀ x4 . Subq x4 x0 ⟶ prim1 x4 x3)) x2.

Apply H7 with ∃ x3 . ∀ x4 . iff (prim1 x4 x3) (Subq x4 x0).

Assume H8: prim1 x2 x1.

Assume H9: ∀ x3 . Subq ... ... ⟶ prim1 x3 x2.

...

■

Proofgold Proof