Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with
x0,
x1,
x2,
bij x1 x0 (ed93b.. x0 x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x0,
x1,
x2,
(∀ x3 . In x3 x1 ⟶ ∃ x4 . and (In x4 x0) (x2 x4 = x3)) ⟶ bij x1 x0 (ed93b.. x0 x2) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2:
∀ x3 . In x3 x0 ⟶ In (x2 x3) x1.
Assume H3:
∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Assume H4:
∀ x3 . In x3 x1 ⟶ ∃ x4 . and (In x4 x0) (x2 x4 = x3).
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with
x1,
x0,
ed93b.. x0 x2 leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with
x1,
x0,
ed93b.. x0 x2 leaving 2 subgoals.
Let x3 of type ι be given.
Apply L6 with
x3,
In ((λ x4 . ed93b.. x0 x2 x4) x3) x0 leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H9:
x2 (ed93b.. x0 x2 x3) = x3.
The subproof is completed by applying H8.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H9:
(λ x5 . ed93b.. x0 x2 x5) x3 = (λ x5 . ed93b.. x0 x2 x5) x4.
Apply L6 with
x3,
x3 = x4 leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H10:
In ((λ x5 . ed93b.. x0 x2 x5) x3) x0.
Assume H11:
x2 ((λ x5 . ed93b.. x0 x2 x5) x3) = x3.
Apply L6 with
x4,
x3 = x4 leaving 2 subgoals.
The subproof is completed by applying H8.
Assume H12:
In ((λ x5 . ed93b.. x0 x2 x5) x4) x0.
Assume H13:
x2 ((λ x5 . ed93b.. x0 x2 x5) x4) = x4.
Apply H11 with
λ x5 x6 . x5 = x4.
Apply H13 with
λ x5 x6 . x2 ((λ x7 . ed93b.. x0 x2 x7) x3) = x5.
Apply H9 with
λ x5 x6 . x2 ((λ x7 . ed93b.. x0 x2 x7) x3) = x2 x5.
Let x5 of type ι → ι → ο be given.
The subproof is completed by applying H14.
Let x3 of type ι be given.
Let x4 of type ο be given.
Assume H9:
∀ x5 . and (In x5 x1) ((λ x6 . ed93b.. x0 x2 x6) x5 = x3) ⟶ x4.
Apply H9 with
x2 x3.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In (x2 x3) x1,
(λ x5 . ed93b.. x0 x2 x5) (x2 x3) = x3 leaving 2 subgoals.