Let x0 of type ι be given.
Assume H0: x0 ⊆ 3.
Let x1 of type ι be given.
Assume H1: x1 ⊆ 3.
Assume H2: 0 ∈ x0 = 0 ∈ x1.
Assume H3: 1 ∈ x0 = 1 ∈ x1.
Assume H4: 2 ∈ x0 = 2 ∈ x1.
Apply set_ext with
x0,
x1 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H5: x2 ∈ x0.
Apply cases_3 with
x2,
λ x3 . x3 ∈ x0 ⟶ x3 ∈ x1 leaving 5 subgoals.
Apply H0 with
x2.
The subproof is completed by applying H5.
Apply H2 with
λ x3 x4 : ο . x4 ⟶ 0 ∈ x1.
Assume H6: 0 ∈ x1.
The subproof is completed by applying H6.
Apply H3 with
λ x3 x4 : ο . x4 ⟶ 1 ∈ x1.
Assume H6: 1 ∈ x1.
The subproof is completed by applying H6.
Apply H4 with
λ x3 x4 : ο . x4 ⟶ 2 ∈ x1.
Assume H6: 2 ∈ x1.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
Let x2 of type ι be given.
Assume H5: x2 ∈ x1.
Apply cases_3 with
x2,
λ x3 . x3 ∈ x1 ⟶ x3 ∈ x0 leaving 5 subgoals.
Apply H1 with
x2.
The subproof is completed by applying H5.
Apply H2 with
λ x3 x4 : ο . 0 ∈ x1 ⟶ x4.
Assume H6: 0 ∈ x1.
The subproof is completed by applying H6.
Apply H3 with
λ x3 x4 : ο . 1 ∈ x1 ⟶ x4.
Assume H6: 1 ∈ x1.
The subproof is completed by applying H6.
Apply H4 with
λ x3 x4 : ο . 2 ∈ x1 ⟶ x4.
Assume H6: 2 ∈ x1.
The subproof is completed by applying H6.
The subproof is completed by applying H5.