Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_e5ee05cdff8551ce0d9dc58ec4d6754afa2e75276323e770f74710c8b0d2eef5 with
x0,
x1,
x1 = PSNo x0 (λ x2 . In x2 x1).
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
x1,
PSNo x0 (λ x2 . In x2 x1) leaving 2 subgoals.
Apply unknownprop_023b2e512ed9c52f995f2d07c1a06cfb4ae27f29745759c860f7e880eac7d40f with
x0,
λ x2 . In x2 x1 ⟶ In x2 (PSNo x0 (λ x3 . In x3 x1)) leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_26f5054f55e1cc99d707390045c57973d733124f73202e22abda7782932b774a with
x0,
λ x3 . In x3 x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply unknownprop_22b63889168c3c27321f1d9d99a6c13d916b48d833ad1ef7079baee20e0a05c6 with
In ((λ x3 . SetAdjoin x3 (Sing 1)) x2) x1,
In x2 x1,
In ((λ x3 . SetAdjoin x3 (Sing 1)) x2) (PSNo x0 (λ x3 . In x3 x1)) leaving 3 subgoals.
Apply H2 with
x2.
The subproof is completed by applying H3.
Assume H6:
not (In x2 x1).
Apply unknownprop_fce6c650dbf1e2382a6f6c641c5c31fbe3c5b8a0bc83e8ec16fdb3c61209be31 with
x0,
λ x3 . In x3 x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply FalseE with
In x2 x1 ⟶ In ((λ x3 . SetAdjoin x3 (Sing 1)) x2) (PSNo x0 (λ x3 . In x3 x1)).
Apply notE with
In ((λ x3 . SetAdjoin x3 (Sing 1)) x2) x1 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply L3 with
x2 leaving 2 subgoals.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x1,
SNoElts_ x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
Apply unknownprop_6a486d2f7d911fc69f373a3a2aa953ced5a8fb2233dc09710907454779c0b8a5 with
x0,
λ x2 . In x2 x1,
λ x2 . In x2 x1 leaving 2 subgoals.
Let x2 of type ι be given.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Assume H4:
not (In x2 x1).
Apply unknownprop_22b63889168c3c27321f1d9d99a6c13d916b48d833ad1ef7079baee20e0a05c6 with
In ((λ x3 . SetAdjoin x3 (Sing 1)) x2) x1,
In x2 x1,
In ((λ x3 . SetAdjoin x3 (Sing 1)) x2) x1 leaving 3 subgoals.
Apply H2 with
x2.
The subproof is completed by applying H3.
Assume H6:
not (In x2 x1).
The subproof is completed by applying H5.