Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: x0 0.
Assume H1: ∀ x1 x2 . finite x1 ⟶ nIn x2 x1 ⟶ x0 x1 ⟶ x0 (binunion x1 (Sing x2)).
Let x1 of type ι be given.
Assume H2: finite x1.
Apply H2 with x0 x1.
Let x2 of type ι be given.
Assume H3: (λ x3 . and (x3 ∈ omega) (equip x1 x3)) x2.
Apply H3 with x0 x1.
Assume H4: x2 ∈ omega.
Apply nat_ind with λ x3 . ∀ x4 . equip x4 x3 ⟶ x0 x4, x2, x1 leaving 3 subgoals.
Let x3 of type ι be given.
Assume H5: equip x3 0.
Apply equip_0_Empty with x3, λ x4 x5 . x0 x5 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H5: nat_p x3.
Assume H6: ∀ x4 . equip x4 x3 ⟶ x0 x4.
Let x4 of type ι be given.
Assume H7: equip x4 (ordsucc x3).
Apply equip_sym with x4, ordsucc x3, x0 x4 leaving 2 subgoals.
The subproof is completed by applying H7.
Let x5 of type ι → ι be given.
Assume H8: bij (ordsucc x3) x4 x5.
Apply bijE with ordsucc x3, x4, x5, x0 x4 leaving 2 subgoals.
The subproof is completed by applying H8.
Assume H9: ∀ x6 . x6 ∈ ordsucc x3 ⟶ x5 x6 ∈ x4.
Assume H10: ∀ x6 . x6 ∈ ordsucc x3 ⟶ ∀ x7 . x7 ∈ ordsucc x3 ⟶ x5 x6 = x5 x7 ⟶ x6 = x7.
Assume H11: ∀ x6 . x6 ∈ x4 ⟶ ∃ x7 . and (x7 ∈ ordsucc x3) (x5 x7 = x6).
Claim L12: ...
...
Apply set_ext with x4, binunion {x5 x6|x6 ∈ x3} (Sing (x5 x3)), λ x6 x7 . x0 x7 leaving 3 subgoals.
Let x6 of type ι be given.
Assume H13: x6 ∈ x4.
Apply H11 with x6, x6 ∈ binunion (prim5 x3 x5) (Sing (x5 x3)) leaving 2 subgoals.
The subproof is completed by applying H13.
Let x7 of type ι be given.
Assume H14: (λ x8 . and (x8 ∈ ordsucc x3) (x5 x8 = x6)) x7.
Apply H14 with x6 ∈ binunion (prim5 x3 x5) (Sing (x5 x3)).
Assume H15: x7 ∈ ordsucc x3.
Assume H16: x5 x7 = x6.
Apply ordsuccE with x3, x7, x6 ∈ binunion (prim5 x3 x5) (Sing (x5 x3)) leaving 3 subgoals.
The subproof is completed by applying H15.
Assume H17: x7 ∈ x3.
Apply binunionI1 with prim5 x3 x5, Sing (x5 x3), x6.
Apply H16 with λ x8 x9 . x8 ∈ {x5 x10|x10 ∈ x3}.
Apply ReplI with x3, x5, x7.
The subproof is completed by applying H17.
Assume H17: x7 = x3.
Apply binunionI2 with prim5 x3 x5, Sing (x5 x3), x6.
Apply H16 with λ x8 x9 . x8 ∈ Sing (x5 x3).
Apply H17 with λ x8 x9 . x5 x9 ∈ Sing (x5 x3).
The subproof is completed by applying SingI with x5 x3.
Let x6 of type ι be given.
Assume H13: x6 ∈ binunion {x5 x7|x7 ∈ x3} (Sing (x5 x3)).
Apply binunionE with {x5 x7|x7 ∈ x3}, Sing (x5 x3), x6, x6 ∈ x4 leaving 3 subgoals.
The subproof is completed by applying H13.
Assume H14: x6 ∈ {x5 ...|x7 ∈ x3}.
...
...
...
...
■