Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: ZermeloWO x0 x1.

Assume H1: ZermeloWO x1 x0.

Apply ZermeloWO_Eps with x0, λ x2 x3 . x2 = x1.

Apply ZermeloWO_Eps with x1, λ x2 x3 . prim0 (ZermeloWO x0) = x2.

Claim L2: ZermeloWO x0 = ZermeloWO x1

Apply pred_ext_2 with ZermeloWO x0, ZermeloWO x1 leaving 2 subgoals.

Let x2 of type ι be given.

Assume H2: ZermeloWO x0 x2.

Apply ZermeloWO_tra with x1, x0, x2 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Let x2 of type ι be given.

Assume H2: ZermeloWO x1 x2.

Apply ZermeloWO_tra with x0, x1, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

Apply L2 with λ x2 x3 : ι → ο . prim0 x3 = prim0 (ZermeloWO x1).

Let x2 of type ι → ι → ο be given.

Assume H3: x2 (prim0 (ZermeloWO x1)) (prim0 (ZermeloWO x1)).

The subproof is completed by applying H3.

■

Proofgold Proof