| pf |
|---|
Apply set_ext with eps_ 0, 1 leaving 2 subgoals.
Let x0 of type ι be given.
Apply binunionE with Sing 0, {(λ x2 . SetAdjoin x2 (Sing 1)) (ordsucc x1)|x1 ∈ 0}, x0, x0 ∈ 1 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply SingE with 0, x0, λ x1 x2 . x2 ∈ 1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying In_0_1.
Apply ReplE_impred with 0, λ x1 . (λ x2 . SetAdjoin x2 (Sing 1)) (ordsucc x1), x0, x0 ∈ 1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H2: x1 ∈ 0.
Apply FalseE with x0 = SetAdjoin (ordsucc x1) (Sing 1) ⟶ x0 ∈ 1.
Apply EmptyE with x1.
The subproof is completed by applying H2.
Let x0 of type ι be given.
Assume H0: x0 ∈ 1.
Apply cases_1 with x0, λ x1 . x1 ∈ eps_ 0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply binunionI1 with Sing 0, {(λ x2 . SetAdjoin x2 (Sing 1)) (ordsucc x1)|x1 ∈ 0}, 0.
The subproof is completed by applying SingI with 0.
■ |
|