Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
atleastp x1 x0 ⟶ x0 ⊆ x1 ⟶ x0 = x1.
Let x2 of type ι be given.
Apply H1 with
atleastp x1 x0 ⟶ x0 ⊆ x1 ⟶ x0 = x1.
Assume H5: x0 ⊆ x1.
Apply set_ext with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H5.
Let x3 of type ι be given.
Assume H6: x3 ∈ x1.
Apply L7 with
x3 ∈ x0.
Let x4 of type ι → ι be given.
Apply bijE with
x2,
x0,
x4,
x3 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H8.
Assume H9: ∀ x5 . x5 ∈ x2 ⟶ x4 x5 ∈ x0.
Assume H10: ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Assume H11:
∀ x5 . x5 ∈ x0 ⟶ ∃ x6 . and (x6 ∈ x2) (x4 x6 = x5).
Apply H3 with
x3 ∈ x0.
Let x5 of type ι → ι be given.
Assume H12:
bij x0 x2 x5.
Apply bijE with
x0,
x2,
x5,
x3 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H12.
Assume H13: ∀ x6 . x6 ∈ x0 ⟶ x5 x6 ∈ x2.
Assume H14: ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x5 x6 = x5 x7 ⟶ x6 = x7.
Assume H15:
∀ x6 . x6 ∈ x2 ⟶ ∃ x7 . and (x7 ∈ x0) (x5 x7 = x6).
Apply H4 with
x3 ∈ x0.
Let x6 of type ι → ι be given.
Assume H16:
inj x1 x0 x6.
Apply H16 with
x3 ∈ x0.
Assume H17: ∀ x7 . x7 ∈ x1 ⟶ x6 x7 ∈ x0.
Assume H18: ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x6 x7 = x6 x8 ⟶ x7 = x8.
Apply bijE with
x2,
x2,
λ x7 . x5 (x6 (x4 x7)),
x3 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying L19.
Assume H20: ∀ x7 . x7 ∈ x2 ⟶ x5 (x6 (x4 x7)) ∈ x2.
Assume H21: ∀ x7 . x7 ∈ x2 ⟶ ∀ x8 . x8 ∈ x2 ⟶ x5 (x6 (x4 x7)) = x5 (x6 (x4 x8)) ⟶ x7 = x8.
Assume H22:
∀ x7 . x7 ∈ x2 ⟶ ∃ x8 . and (x8 ∈ x2) (x5 (x6 (x4 x8)) = x7).
Apply H22 with
x5 (x6 x3),
x3 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying L23.
Let x7 of type ι be given.
Assume H24:
(λ x8 . and (x8 ∈ x2) (x5 (x6 (x4 x8)) = x5 (x6 x3))) x7.
Apply H24 with
x3 ∈ x0.
Assume H25: x7 ∈ x2.
Assume H26: x5 (x6 ...) = ....