| pf |
|---|
Let x0 of type ι → ι be given.
Apply finite_ind with λ x1 . finite {x0 x2|x2 ∈ x1} leaving 2 subgoals.
Apply Repl_Empty with x0, λ x1 x2 . finite x2.
The subproof is completed by applying finite_Empty.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H2: finite {x0 x3|x3 ∈ x1}. Apply set_ext with {x0 x3|x3 ∈ binunion x1 (Sing x2)}, binunion {x0 x3|x3 ∈ x1} (Sing (x0 x2)), λ x3 x4 . finite x4 leaving 3 subgoals.
Let x3 of type ι be given.
Apply ReplE_impred with binunion x1 (Sing x2), x0, x3, x3 ∈ binunion (prim5 x1 x0) (Sing (x0 x2)) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Assume H5: x3 = x0 x4.
Apply binunionE with x1, Sing x2, x4, x3 ∈ binunion {x0 x5|x5 ∈ x1} (Sing (x0 x2)) leaving 3 subgoals.
The subproof is completed by applying H4.
Assume H6: x4 ∈ x1.
Apply binunionI1 with {x0 x5|x5 ∈ x1}, Sing (x0 x2), x3.
Apply H5 with λ x5 x6 . x6 ∈ {x0 x7|x7 ∈ x1}.
Apply ReplI with x1, x0, x4.
The subproof is completed by applying H6.
Apply binunionI2 with {x0 x5|x5 ∈ x1}, Sing (x0 x2), x3.
Apply H5 with λ x5 x6 . x6 ∈ Sing (x0 x2).
Apply SingE with x2, x4, λ x5 x6 . x0 x6 ∈ Sing (x0 x2) leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying SingI with x0 x2.
Let x3 of type ι be given.
Apply binunionE with {x0 x4|x4 ∈ x1}, Sing (x0 x2), x3, x3 ∈ prim5 (binunion x1 (Sing x2)) x0 leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H4: x3 ∈ {x0 x4|x4 ∈ x1}.
Apply ReplE_impred with x1, x0, x3, x3 ∈ prim5 (binunion x1 (Sing x2)) x0 leaving 2 subgoals.
The subproof is completed by applying H4.
Let x4 of type ι be given.
Assume H5: x4 ∈ x1.
Assume H6: x3 = x0 x4.
Apply H6 with λ x5 x6 . x6 ∈ prim5 (binunion x1 (Sing x2)) x0.
Apply ReplI with binunion x1 (Sing x2), x0, x4.
Apply binunionI1 with x1, Sing x2, x4.
The subproof is completed by applying H5.
Assume H4: x3 ∈ Sing (x0 x2). Apply SingE with x0 x2, x3, λ x4 x5 . x5 ∈ prim5 (binunion x1 (Sing x2)) x0 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply ReplI with binunion x1 (Sing x2), x0, x2.
Apply binunionI2 with x1, Sing x2, x2.
The subproof is completed by applying SingI with x2.
Apply binunion_finite with {x0 x3|x3 ∈ x1}, Sing (x0 x2) leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_f7016afae9c8976834aae8fd87dfbc66905d8d8b02412954fb76543365d9f363 with x0 x2.
■ |
|