Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
SNo
x0
.
Let x1 of type
ι
be given.
Assume H1:
x1
∈
SNoLev
x0
.
Claim L2:
SNo_
(
SNoLev
x0
)
x0
Apply SNoLev_ with
x0
.
The subproof is completed by applying H0.
Apply L2 with
SNo_
x1
(
binintersect
x0
(
SNoElts_
x1
)
)
.
Assume H3:
x0
⊆
SNoElts_
(
SNoLev
x0
)
.
Assume H4:
∀ x2 .
x2
∈
SNoLev
x0
⟶
exactly1of2
(
SetAdjoin
x2
(
Sing
1
)
∈
x0
)
(
x2
∈
x0
)
.
Apply andI with
binintersect
x0
(
SNoElts_
x1
)
⊆
SNoElts_
x1
,
∀ x2 .
x2
∈
x1
⟶
exactly1of2
(
SetAdjoin
x2
(
Sing
1
)
∈
binintersect
x0
(
SNoElts_
x1
)
)
(
x2
∈
binintersect
x0
(
SNoElts_
x1
)
)
leaving 2 subgoals.
The subproof is completed by applying binintersect_Subq_2 with
x0
,
SNoElts_
x1
.
Let x2 of type
ι
be given.
Assume H5:
x2
∈
x1
.
Claim L6:
x2
∈
SNoLev
x0
Apply ordinal_TransSet with
SNoLev
x0
,
x1
,
x2
leaving 3 subgoals.
Apply SNoLev_ordinal with
x0
.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply exactly1of2_E with
SetAdjoin
x2
(
Sing
1
)
∈
x0
,
x2
∈
x0
,
exactly1of2
(
SetAdjoin
x2
(
Sing
1
)
∈
binintersect
x0
(
SNoElts_
x1
)
)
(
x2
∈
binintersect
x0
(
SNoElts_
x1
)
)
leaving 3 subgoals.
Apply H4 with
x2
.
The subproof is completed by applying L6.
Assume H7:
SetAdjoin
x2
(
Sing
1
)
∈
x0
.
Assume H8:
nIn
x2
x0
.
Apply exactly1of2_I1 with
SetAdjoin
x2
(
Sing
1
)
∈
binintersect
x0
(
SNoElts_
x1
)
,
x2
∈
binintersect
x0
(
SNoElts_
x1
)
leaving 2 subgoals.
Apply binintersectI with
x0
,
SNoElts_
x1
,
SetAdjoin
x2
(
Sing
1
)
leaving 2 subgoals.
The subproof is completed by applying H7.
Apply binunionI2 with
x1
,
{
SetAdjoin
x3
(
Sing
1
)
|x3 ∈
x1
}
,
SetAdjoin
x2
(
Sing
1
)
.
Apply ReplI with
x1
,
λ x3 .
SetAdjoin
x3
(
Sing
1
)
,
x2
.
The subproof is completed by applying H5.
Assume H9:
x2
∈
binintersect
x0
(
SNoElts_
x1
)
.
Apply H8.
Apply binintersectE1 with
x0
,
SNoElts_
x1
,
x2
.
The subproof is completed by applying H9.
Assume H7:
nIn
(
SetAdjoin
x2
(
Sing
1
)
)
x0
.
Assume H8:
x2
∈
x0
.
Apply exactly1of2_I2 with
SetAdjoin
x2
(
Sing
1
)
∈
binintersect
x0
(
SNoElts_
x1
)
,
x2
∈
binintersect
x0
(
SNoElts_
x1
)
leaving 2 subgoals.
Assume H9:
SetAdjoin
x2
(
Sing
1
)
∈
binintersect
x0
(
SNoElts_
x1
)
.
Apply H7.
Apply binintersectE1 with
x0
,
SNoElts_
x1
,
SetAdjoin
x2
(
Sing
1
)
.
The subproof is completed by applying H9.
Apply binintersectI with
x0
,
SNoElts_
x1
,
x2
leaving 2 subgoals.
The subproof is completed by applying H8.
Apply binunionI1 with
x1
,
{
SetAdjoin
x3
(
Sing
1
)
|x3 ∈
x1
}
,
x2
.
The subproof is completed by applying H5.
■