| pf |
|---|
Let x0 of type ι → ι be given.
Apply nat_ind with λ x1 . (∀ x2 . x2 ∈ x1 ⟶ finite (x0 x2)) ⟶ finite (famunion x1 (λ x2 . x0 x2)) leaving 2 subgoals.
Assume H0: ∀ x1 . x1 ∈ 0 ⟶ finite (x0 x1). Apply famunion_Empty with λ x1 . x0 x1, λ x1 x2 . finite x2.
The subproof is completed by applying finite_Empty.
Let x1 of type ι be given.
Apply set_ext with famunion (ordsucc x1) (λ x2 . x0 x2), binunion (famunion x1 (λ x2 . x0 x2)) (x0 x1), λ x2 x3 . finite x3 leaving 3 subgoals.
Let x2 of type ι be given.
Apply famunionE_impred with ordsucc x1, x0, x2, x2 ∈ binunion (famunion x1 x0) (x0 x1) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H5: x2 ∈ x0 x3.
Apply ordsuccE with x1, x3, x2 ∈ binunion (famunion x1 x0) (x0 x1) leaving 3 subgoals.
The subproof is completed by applying H4.
Assume H6: x3 ∈ x1.
Apply binunionI1 with famunion x1 x0, x0 x1, x2.
Apply famunionI with x1, x0, x3, x2 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
Assume H6: x3 = x1.
Apply binunionI2 with famunion x1 x0, x0 x1, x2.
Apply H6 with λ x4 x5 . x2 ∈ x0 x4.
The subproof is completed by applying H5.
Let x2 of type ι be given.
Apply binunionE' with famunion x1 x0, x0 x1, x2, x2 ∈ famunion (ordsucc x1) x0 leaving 2 subgoals.
Apply famunionE_impred with x1, x0, x2, x2 ∈ famunion (ordsucc x1) x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H4: x3 ∈ x1.
Apply famunionI with ordsucc x1, x0, x3, x2.
Apply ordsuccI1 with x1, x3.
The subproof is completed by applying H4.
Apply famunionI with ordsucc x1, x0, x1, x2.
The subproof is completed by applying ordsuccI2 with x1.
Apply binunion_finite with famunion x1 (λ x2 . x0 x2), x0 x1 leaving 2 subgoals.
Apply H1.
Let x2 of type ι be given.
Assume H3: x2 ∈ x1.
Apply H2 with x2.
Apply ordsuccI1 with x1, x2.
The subproof is completed by applying H3.
Apply H2 with x1.
The subproof is completed by applying ordsuccI2 with x1.
■ |
|