Let x0 of type ι → ο be given.
Assume H0: ∃ x1 . x0 x1.
Apply ZermeloWO_wo with
x0,
∃ x1 . and (x0 x1) (∀ x2 . and (x0 x2) (x2 = x1 ⟶ ∀ x3 : ο . x3) ⟶ ZermeloWOstrict x1 x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Apply H1 with
∃ x2 . and (x0 x2) (∀ x3 . and (x0 x3) (x3 = x2 ⟶ ∀ x4 : ο . x4) ⟶ ZermeloWOstrict x2 x3).
Assume H2: x0 x1.
Let x2 of type ο be given.
Assume H4:
∀ x3 . and (x0 x3) (∀ x4 . and (x0 x4) (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ZermeloWOstrict x3 x4) ⟶ x2.
Apply H4 with
x1.
Apply andI with
x0 x1,
∀ x3 . and (x0 x3) (x3 = x1 ⟶ ∀ x4 : ο . x4) ⟶ ZermeloWOstrict x1 x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H5:
and (x0 x3) (x3 = x1 ⟶ ∀ x4 : ο . x4).
Apply H5 with
ZermeloWOstrict x1 x3.
Assume H6: x0 x3.
Assume H7: x3 = x1 ⟶ ∀ x4 : ο . x4.
Apply andI with
ZermeloWO x1 x3,
x1 = x3 ⟶ ∀ x4 : ο . x4 leaving 2 subgoals.
Apply H3 with
x3.
The subproof is completed by applying H6.
Assume H8: x1 = x3.
Apply H7.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H8 with λ x5 x6 . x4 x6 x5.