Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι → ι be given.
Assume H3: ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 x6 x5 ⟶ x6 = x4 x5.
Assume H4: ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Apply dneg with
∃ x5 . and (x5 ∈ x0) (∀ x6 . x6 ∈ x3 ⟶ not (x1 x5 x6)).
Assume H5:
not (∃ x5 . and (x5 ∈ x0) (∀ x6 . x6 ∈ x3 ⟶ not (x1 x5 x6))).
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply atleastp_tra with
ordsucc x2,
x0,
x2 leaving 2 subgoals.
Apply equip_atleastp with
ordsucc x2,
x0.
Apply equip_sym with
x0,
ordsucc x2.
The subproof is completed by applying H1.
Apply atleastp_tra with
x0,
{x4 x5|x5 ∈ x3},
x2 leaving 2 subgoals.
Apply Subq_atleastp with
x0,
{x4 x5|x5 ∈ x3}.
Let x5 of type ι be given.
Assume H6: x5 ∈ x0.
Apply dneg with
x5 ∈ prim5 x3 x4.
Assume H7:
nIn x5 {x4 x6|x6 ∈ x3}.
Apply H5.
Let x6 of type ο be given.
Assume H8:
∀ x7 . and (x7 ∈ x0) (∀ x8 . x8 ∈ x3 ⟶ not (x1 x7 x8)) ⟶ x6.
Apply H8 with
x5.
Apply andI with
x5 ∈ x0,
∀ x7 . x7 ∈ x3 ⟶ not (x1 x5 x7) leaving 2 subgoals.
The subproof is completed by applying H6.
Let x7 of type ι be given.
Assume H9: x7 ∈ x3.
Assume H10: x1 x5 x7.
Apply H7.
Claim L11: x5 = x4 x7
Apply H3 with
x7,
x5 leaving 3 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply L11 with
λ x8 x9 . x9 ∈ {x4 x10|x10 ∈ x3}.
Apply ReplI with
x3,
x4,
x7.
The subproof is completed by applying H9.
Apply equip_atleastp with
{x4 x5|x5 ∈ x3},
x2.
Apply equip_tra with
{x4 x5|x5 ∈ x3},
x3,
x2 leaving 2 subgoals.
Apply equip_sym with
x3,
prim5 x3 x4.
Apply unknownprop_6f924010899e62355200d41f1cef23d6373bef28ff540d0bdb872dcb6e86d39f with
x3,
x4.
The subproof is completed by applying H4.
The subproof is completed by applying H2.