Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H1: x1 ⊆ x0.
Let x2 of type ι be given.
Assume H2: x2 ⊆ x0.
Apply dneg with
∃ x3 . and (x3 ∈ x1) (x3 ∈ x2).
Assume H5:
not (∃ x3 . and (x3 ∈ x1) (x3 ∈ x2)).
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
u3 leaving 2 subgoals.
The subproof is completed by applying nat_3.
Apply atleastp_tra with
u4,
binunion x1 x2,
u3 leaving 2 subgoals.
Apply unknownprop_a056e7e1d4164d24a60c8047a73979083395e5609e36aaee67608ba08eded8a1 with
λ x3 x4 . atleastp x3 (binunion x1 x2).
Apply atleastp_tra with
add_nat u2 u2,
setsum u2 u2,
binunion x1 x2 leaving 2 subgoals.
Apply equip_atleastp with
add_nat u2 u2,
setsum u2 u2.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
u2,
u2,
u2,
u2 leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_2.
The subproof is completed by applying equip_ref with
u2.
The subproof is completed by applying equip_ref with
u2.
Apply unknownprop_f59d6b770984c869c1e5c6fa6c966bf2e7f31a21d93561635565b3e8dc0de299 with
u2,
u2,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Assume H6: x3 ∈ x1.
Assume H7: x3 ∈ x2.
Apply H5.
Let x4 of type ο be given.
Assume H8:
∀ x5 . and (x5 ∈ x1) (x5 ∈ x2) ⟶ x4.
Apply H8 with
x3.
Apply andI with
x3 ∈ x1,
x3 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Apply atleastp_tra with
binunion x1 x2,
x0,
u3 leaving 2 subgoals.
Apply Subq_atleastp with
binunion x1 x2,
x0.
Apply binunion_Subq_min with
x1,
x2,
x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H0.