Let x0 of type ι → ι → ο be given.
Assume H0:
∀ x1 . x1 ⊆ u12 ⟶ atleastp u5 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3)).
Let x1 of type ι be given.
Assume H3:
∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3).
Apply set_ext with
x1,
binunion (setminus x1 u12) (binintersect x1 u12) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H5: x2 ∈ x1.
Apply xm with
x2 ∈ u12,
x2 ∈ binunion (setminus x1 u12) (binintersect x1 u12) leaving 2 subgoals.
Apply binunionI2 with
setminus x1 u12,
binintersect x1 u12,
x2.
Apply binintersectI with
x1,
u12,
x2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply binunionI1 with
setminus x1 u12,
binintersect x1 u12,
x2.
Apply setminusI with
x1,
u12,
x2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Let x2 of type ι be given.
The subproof is completed by applying binintersect_Subq_2 with
x1,
u12.
Apply H0 with
binintersect x1 u12 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H7.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply H3 with
x2,
x3 leaving 2 subgoals.
Apply binintersectE1 with
x1,
u12,
x2.
The subproof is completed by applying H8.
Apply binintersectE1 with
x1,
u12,
x3.
The subproof is completed by applying H9.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with
u4,
binintersect x1 u12,
atleastp (binintersect x1 u12) u4 leaving 3 subgoals.
The subproof is completed by applying nat_4.
The subproof is completed by applying H8.
Apply L5 with
λ x2 x3 . atleastp x3 u5.
Apply nat_setsum_ordsucc with
u4,
λ x2 x3 . atleastp (binunion (setminus x1 u12) (binintersect x1 u12)) x2 leaving 2 subgoals.
The subproof is completed by applying nat_4.
Apply unknownprop_94b237fc7b7d3bf1a0a078f7d057802d281bf3c46c36fd56a85d339ac0f07170 with
setminus x1 u12,
binintersect x1 u12,
u1,
u4 leaving 3 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying L8.
The subproof is completed by applying L4.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
u5 leaving 2 subgoals.
The subproof is completed by applying nat_5.
Apply atleastp_tra with
u6,
x1,
u5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying L10.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with
u1,
setminus x1 u12,
atleastp u2 (setminus x1 u12) leaving 3 subgoals.
The subproof is completed by applying nat_1.
The subproof is completed by applying H10.