Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H0: atleastp x0 x2.
Assume H1: atleastp x1 x3.
Assume H2: ∀ x4 . x4x0nIn x4 x1.
Apply H0 with atleastp (binunion x0 x1) (setsum x2 x3).
Let x4 of type ιι be given.
Assume H3: inj x0 x2 x4.
Apply H3 with atleastp (binunion x0 x1) (setsum x2 x3).
Assume H4: ∀ x5 . x5x0x4 x5x2.
Assume H5: ∀ x5 . x5x0∀ x6 . x6x0x4 x5 = x4 x6x5 = x6.
Apply H1 with atleastp (binunion x0 x1) (setsum x2 x3).
Let x5 of type ιι be given.
Assume H6: inj x1 x3 x5.
Apply H6 with atleastp (binunion x0 x1) (setsum x2 x3).
Assume H7: ∀ x6 . x6x1x5 x6x3.
Assume H8: ∀ x6 . x6x1∀ x7 . x7x1x5 x6 = x5 x7x6 = x7.
Let x6 of type ο be given.
Assume H9: ∀ x7 : ι → ι . inj (binunion x0 x1) (setsum x2 x3) x7x6.
Apply H9 with λ x7 . If_i (x7x0) (Inj0 (x4 x7)) (Inj1 (x5 x7)).
Apply andI with ∀ x7 . x7binunion x0 x1(λ x8 . If_i (x8x0) (Inj0 (x4 x8)) (Inj1 (x5 x8))) x7setsum x2 x3, ∀ x7 . x7binunion x0 x1∀ x8 . x8binunion x0 x1(λ x9 . If_i (x9x0) (Inj0 (x4 x9)) (Inj1 (x5 x9))) x7 = (λ x9 . If_i (x9x0) (Inj0 (x4 x9)) (Inj1 (x5 x9))) x8x7 = x8 leaving 2 subgoals.
Let x7 of type ι be given.
Assume H10: x7binunion x0 x1.
Apply binunionE with x0, x1, x7, (λ x8 . If_i (x8x0) (Inj0 (x4 x8)) (Inj1 (x5 x8))) x7setsum x2 x3 leaving 3 subgoals.
The subproof is completed by applying H10.
Assume H11: x7x0.
Apply If_i_1 with x7x0, Inj0 (x4 x7), Inj1 (x5 x7), λ x8 x9 . x9setsum x2 x3 leaving 2 subgoals.
The subproof is completed by applying H11.
Apply Inj0_setsum with x2, x3, x4 x7.
Apply H4 with x7.
The subproof is completed by applying H11.
Assume H11: x7x1.
Claim L12: nIn x7 x0
Assume H12: x7x0.
Apply H2 with x7 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H11.
Apply If_i_0 with x7x0, Inj0 (x4 x7), Inj1 (x5 x7), λ x8 x9 . x9setsum x2 x3 leaving 2 subgoals.
The subproof is completed by applying L12.
Apply Inj1_setsum with x2, x3, x5 x7.
Apply H7 with x7.
The subproof is completed by applying H11.
...