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.
Assume H1: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4.
Apply unknownprop_9e7ec4148d62bafcd9e146d1756f4a7aed7c3eb8fc00334b6fe1712064d0a901 with
x0,
x1,
x2,
λ x3 x4 : ο . and x4 (∃ x5 . and (x5 ∈ x0) (∀ x6 . x6 ∈ x0 ⟶ and (x2 x6 x5 = x6) (x2 x5 x6 = x6))) = and (28b0a.. x0 x1) (∃ x5 . and (x5 ∈ x0) (∀ x6 . x6 ∈ x0 ⟶ and (x1 x6 x5 = x6) (x1 x5 x6 = x6))) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply prop_ext_2 with
and (28b0a.. x0 x1) (∃ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ and (x2 x4 x3 = x4) (x2 x3 x4 = x4))),
and (28b0a.. x0 x1) (∃ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ and (x1 x4 x3 = x4) (x1 x3 x4 = x4))) leaving 2 subgoals.
Assume H2:
and (28b0a.. x0 x1) (∃ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ and (x2 x4 x3 = x4) (x2 x3 x4 = x4))).
Apply H2 with
and (28b0a.. x0 x1) (∃ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ and (x1 x4 x3 = x4) (x1 x3 x4 = x4))).
Assume H4:
∃ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ and (x2 x4 x3 = x4) (x2 x3 x4 = x4)).
Apply H4 with
and (28b0a.. x0 x1) (∃ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ and (x1 x4 x3 = x4) (x1 x3 x4 = x4))).
Let x3 of type ι be given.
Assume H5:
(λ x4 . and (x4 ∈ x0) (∀ x5 . x5 ∈ x0 ⟶ and (x2 x5 x4 = x5) (x2 x4 x5 = x5))) x3.
Apply H5 with
and (28b0a.. x0 x1) (∃ x4 . and (x4 ∈ x0) (∀ x5 . x5 ∈ x0 ⟶ and (x1 x5 x4 = x5) (x1 x4 x5 = x5))).
Assume H6: x3 ∈ x0.