Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: finite x0.
Apply H0 with finite (binunion x0 (Sing x1)).
Let x2 of type ι be given.
Assume H1: (λ x3 . and (x3 ∈ omega) (equip x0 x3)) x2.
Apply H1 with finite (binunion x0 (Sing x1)).
Assume H2: x2 ∈ omega.
Assume H3: equip x0 x2.
Apply equip_sym with x0, x2, finite (binunion x0 (Sing x1)) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι → ι be given.
Assume H4: bij x2 x0 x3.
Apply bijE with x2, x0, x3, finite (binunion x0 (Sing x1)) leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H5: ∀ x4 . x4 ∈ x2 ⟶ x3 x4 ∈ x0.
Assume H6: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Assume H7: ∀ x4 . x4 ∈ x0 ⟶ ∃ x5 . and (x5 ∈ x2) (x3 x5 = x4).
Apply xm with x1 ∈ x0, finite (binunion x0 (Sing x1)) leaving 2 subgoals.
Assume H8: x1 ∈ x0.
Apply set_ext with binunion x0 (Sing x1), x0, λ x4 x5 . finite x5 leaving 3 subgoals.
Let x4 of type ι be given.
Assume H9: x4 ∈ binunion x0 (Sing x1).
Apply binunionE with x0, Sing x1, x4, x4 ∈ x0 leaving 3 subgoals.
The subproof is completed by applying H9.
Assume H10: x4 ∈ x0.
The subproof is completed by applying H10.
Assume H10: x4 ∈ Sing x1.
Apply SingE with x1, x4, λ x5 x6 . x6 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H8.
The subproof is completed by applying binunion_Subq_1 with x0, Sing x1.
The subproof is completed by applying H0.
Assume H8: nIn x1 x0.
Let x4 of type ο be given.
Assume H9: ∀ x5 . and (x5 ∈ omega) (equip (binunion x0 (Sing x1)) x5) ⟶ x4.
Apply H9 with ordsucc x2.
Apply andI with ordsucc x2 ∈ omega, equip (binunion x0 (Sing x1)) (ordsucc x2) leaving 2 subgoals.
Apply omega_ordsucc with x2.
The subproof is completed by applying H2.
Apply equip_sym with ordsucc x2, binunion x0 (Sing x1).
set y5 to be ...
Claim L10: ...
...
Apply L10 with ∃ x6 : ι → ι . bij (ordsucc x2) (binunion x0 (Sing x1)) x6.
Assume H11: ∀ x6 . x6 ∈ x2 ⟶ y5 x6 = x3 x6.
Assume H12: y5 x2 = x1.
Let x6 of type ο be given.
Assume H13: ∀ x7 : ι → ι . bij (ordsucc x2) (binunion x0 (Sing x1)) x7 ⟶ x6.
Apply H13 with y5.
Apply bijI with ordsucc x2, binunion x0 (Sing x1), y5 leaving 3 subgoals.
Let x7 of type ι be given.
Assume H14: x7 ∈ ordsucc x2.
Apply ordsuccE with x2, x7, y5 x7 ∈ binunion x0 (Sing x1) leaving 3 subgoals.
The subproof is completed by applying H14.
Assume H15: x7 ∈ x2.
Apply binunionI1 with x0, Sing x1, y5 x7.
Apply H11 with x7, λ x8 x9 . x9 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H15.
Apply H5 with x7.
The subproof is completed by applying H15.
Assume H15: x7 = x2.
Apply binunionI2 with x0, Sing x1, y5 x7.
Apply H15 with λ x8 x9 . y5 x9 ∈ Sing x1.
Apply H12 with λ x8 x9 . x9 ∈ Sing x1.
The subproof is completed by applying SingI with x1.
Let x7 of type ι be given.
...
...
■