Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Quasigroup MagmaHom struct_id struct_comp x1 x2 x3 x4) ⟶ x0.

Apply H0 with 3d151...

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Quasigroup MagmaHom struct_id struct_comp 3d151.. x2 x3 x4) ⟶ x1.

Apply H1 with λ x2 x3 . lam (setprod (ap x2 0) (ap x3 0)) (λ x4 . ap x4 0).

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Quasigroup MagmaHom struct_id struct_comp 3d151.. (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 0)) x3 x4) ⟶ x2.

Apply H2 with λ x3 x4 . lam (setprod (ap x3 0) (ap x4 0)) (λ x5 . ap x5 1).

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Quasigroup MagmaHom struct_id struct_comp 3d151.. (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 0)) (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 1)) x4 ⟶ x3.

Apply H3 with λ x4 x5 x6 x7 x8 . lam (ap x6 0) (λ x9 . lam 2 (λ x10 . If_i (x10 = 0) (ap x7 x9) (ap x8 x9))).

Claim L4: ...

...

Claim L5: ∀ x4 x5 . Quasigroup x4 ⟶ Quasigroup x5 ⟶ Quasigroup (3d151.. x4 x5)

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H5: Quasigroup x4.

Assume H6: Quasigroup x5.

Apply unknownprop_94c3be6982bd677952253aa29af894411b7bd1f90353a0d2fdecf3d31d757dbd with x4, λ x6 . Quasigroup (3d151.. x6 x5) leaving 2 subgoals.

The subproof is completed by applying H5.

Let x6 of type ι be given.

Let x7 of type ι → ι → ι be given.

Assume H7: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ x7 x8 x9 ∈ x6.

Assume H8: ∀ x8 . x8 ∈ x6 ⟶ bij x6 x6 (x7 x8).

Assume H9: ∀ x8 . x8 ∈ x6 ⟶ bij x6 x6 (λ x9 . x7 x9 x8).

Apply unknownprop_94c3be6982bd677952253aa29af894411b7bd1f90353a0d2fdecf3d31d757dbd with x5, λ x8 . Quasigroup (3d151.. (pack_b x6 x7) x8) leaving 2 subgoals.

The subproof is completed by applying H6.

Let x8 of type ι be given.

Let x9 of type ι → ι → ι be given.

Assume H10: ∀ x10 . x10 ∈ x8 ⟶ ∀ x11 . x11 ∈ x8 ⟶ x9 x10 x11 ∈ x8.

Assume H11: ∀ x10 . x10 ∈ x8 ⟶ bij x8 x8 (x9 x10).

Assume H12: ∀ x10 . x10 ∈ x8 ⟶ bij x8 x8 (λ x11 . x9 x11 x10).

Apply unknownprop_84b7a40932bac82c3ecf4fa49a1bea60dc509b45bddc18bf9510d8d39709513f with x6, x7, x8, x9, λ x10 x11 . Quasigroup x11.

Claim L13: ...

...

Apply unknownprop_e3d260e78a123ac716d567ab700d9fc3334efbbe9012a4545cf5b7c9b546016d with setprod x6 x8, λ x10 x11 . lam 2 (λ x12 . If_i (x12 = 0) (x7 (ap x10 0) ...) ...) leaving 3 subgoals.

...

Apply unknownprop_eb47bb5cd73cad8b4ef0b3375f134d111d4de0e7e5fceab966d004fbffa38e8d with Quasigroup leaving 2 subgoals.

The subproof is completed by applying L4.

The subproof is completed by applying L5.

■

Proofgold Proof