Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Assume H2: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2.
Let x4 of type ι → ι → ι be given.
Assume H4:
∀ x5 . x5 ∈ setprod x0 x2 ⟶ ∀ x6 . x6 ∈ setprod x0 x2 ⟶ lam 2 (λ x7 . If_i (x7 = 0) (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))) = x4 x5 x6.
Apply H1 with
0941b.. (setprod x0 x2) x4.
Assume H5: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x1 (x1 x5 x6) x7 = x1 x5 (x1 x6 x7).
Assume H6:
∃ x5 . and (x5 ∈ x0) (∀ x6 . x6 ∈ x0 ⟶ and (x1 x6 x5 = x6) (x1 x5 x6 = x6)).
Apply H3 with
0941b.. (setprod x0 x2) x4.
Assume H7: ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ x3 (x3 x5 x6) x7 = x3 x5 (x3 x6 x7).
Assume H8:
∃ x5 . and (x5 ∈ x2) (∀ x6 . x6 ∈ x2 ⟶ and (x3 x6 x5 = x6) (x3 x5 x6 = x6)).
Apply andI with
28b0a.. (setprod x0 x2) x4,
∃ x5 . and (x5 ∈ setprod x0 x2) (∀ x6 . x6 ∈ setprod x0 x2 ⟶ and (x4 x6 x5 = x6) (x4 x5 x6 = x6)) leaving 2 subgoals.
Apply unknownprop_eaaabdc027024a28dc413cf5c8f24ae2d95c1cae5e12cd1597df72e68312adf2 with
x0,
x1,
x2,
x3,
x4 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H2.
The subproof is completed by applying H7.
The subproof is completed by applying H4.
Apply H6 with
∃ x5 . and (x5 ∈ setprod x0 x2) (∀ x6 . x6 ∈ setprod x0 x2 ⟶ and (x4 x6 x5 = x6) (x4 x5 x6 = x6)).
Let x5 of type ι be given.
Assume H10:
(λ x6 . and (x6 ∈ x0) (∀ x7 . x7 ∈ x0 ⟶ and (x1 x7 x6 = x7) (x1 x6 x7 = x7))) x5.
Apply H10 with
∃ x6 . and (x6 ∈ setprod x0 x2) (∀ x7 . ... ⟶ and (x4 x7 x6 = x7) (x4 x6 x7 = x7)).