Search for blocks/addresses/...

Proofgold Proof

pf
Apply finite_ind with λ x0 . ∀ x1 . x1x0finite x1 leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: x00.
Apply Empty_Subq_eq with x0, λ x1 x2 . finite x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying finite_Empty.
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: finite x0.
Assume H1: nIn x1 x0.
Assume H2: ∀ x2 . x2x0finite x2.
Let x2 of type ι be given.
Assume H3: x2binunion x0 (Sing x1).
Apply xm with x1x2, finite x2 leaving 2 subgoals.
Assume H4: x1x2.
Apply set_ext with x2, binunion (setminus x2 (Sing x1)) (Sing x1), λ x3 x4 . finite x4 leaving 3 subgoals.
Let x3 of type ι be given.
Assume H5: x3x2.
Apply xm with x3Sing x1, x3binunion (setminus x2 (Sing x1)) (Sing x1) leaving 2 subgoals.
The subproof is completed by applying binunionI2 with setminus x2 (Sing x1), Sing x1, x3.
Assume H6: nIn x3 (Sing x1).
Apply binunionI1 with setminus x2 (Sing x1), Sing x1, x3.
Apply setminusI with x2, Sing x1, x3 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Let x3 of type ι be given.
Assume H5: x3binunion (setminus x2 (Sing x1)) (Sing x1).
Apply binunionE with setminus x2 (Sing x1), Sing x1, x3, x3x2 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying setminusE1 with x2, Sing x1, x3.
Assume H6: x3Sing x1.
Apply SingE with x1, x3, λ x4 x5 . x5x2 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H4.
Apply adjoin_finite with setminus x2 (Sing x1), x1.
Apply H2 with setminus x2 (Sing x1).
Let x3 of type ι be given.
Assume H5: x3setminus x2 (Sing x1).
Apply setminusE with x2, Sing x1, x3, x3x0 leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H6: x3x2.
Assume H7: nIn x3 (Sing x1).
Apply binunionE with x0, Sing x1, x3, x3x0 leaving 3 subgoals.
Apply H3 with x3.
The subproof is completed by applying H6.
Assume H8: x3x0.
The subproof is completed by applying H8.
Assume H8: x3Sing x1.
Apply FalseE with x3x0.
Apply H7.
The subproof is completed by applying H8.
Assume H4: nIn x1 x2.
Apply H2 with x2.
Let x3 of type ι be given.
Assume H5: x3x2.
Apply binunionE with x0, Sing x1, x3, x3x0 leaving 3 subgoals.
Apply H3 with x3.
The subproof is completed by applying H5.
Assume H6: x3x0.
The subproof is completed by applying H6.
Assume H6: x3Sing x1.
Apply FalseE with x3x0.
Apply H4.
Apply SingE with x1, x3, λ x4 x5 . x4x2 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H5.