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.
Let x2 of type ο be given.
Assume H2: SNoCutP {x3 ∈ SNoL x0|SNoLev x3 ∈ x1} {x3 ∈ SNoR x0|SNoLev x3 ∈ x1} ⟶ binintersect x0 (SNoElts_ x1) = SNoCut {x3 ∈ SNoL x0|SNoLev x3 ∈ x1} {x3 ∈ SNoR x0|SNoLev x3 ∈ x1} ⟶ x2.
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: binintersect x0 (SNoElts_ x1) = SNoCut {x3 ∈ SNoL x0|SNoLev x3 ∈ x1} {x3 ∈ SNoR x0|SNoLev x3 ∈ x1}
Apply SNo_eta with binintersect x0 (SNoElts_ x1), λ x3 x4 . x4 = SNoCut {x5 ∈ SNoL x0|SNoLev x5 ∈ x1} {x5 ∈ SNoR x0|SNoLev x5 ∈ x1} leaving 2 subgoals.
The subproof is completed by applying L6.
set y3 to be ...
set y4 to be ...
Claim L7: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Assume H7: x5 (SNoCut {x6 ∈ SNoL x2|SNoLev x6 ∈ y3} {x6 ∈ SNoR x2|SNoLev x6 ∈ y3}).
set y6 to be ...
Apply set_ext with SNoL (binintersect x2 (SNoElts_ y3)), {x7 ∈ SNoL x2|SNoLev x7 ∈ y3}, λ x7 x8 . y6 (SNoCut x7 (SNoR (binintersect x2 (SNoElts_ y3)))) (SNoCut x8 (SNoR (binintersect x2 (SNoElts_ y3)))) leaving 3 subgoals.
Let x7 of type ι be given.
Assume H8: x7 ∈ SNoL (binintersect x2 (SNoElts_ y3)).
Apply SNoL_E with binintersect x2 (SNoElts_ y3), x7, x7 ∈ {x8 ∈ SNoL x2|SNoLev x8 ∈ y3} leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H8.
Assume H9: SNo x7.
Apply restr_SNoLev with x2, y3, λ x8 x9 . SNoLev x7 ∈ x9 ⟶ SNoLt x7 (binintersect x2 (SNoElts_ y3)) ⟶ x7 ∈ {x10 ∈ SNoL x2|SNoLev x10 ∈ y3} leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H10: SNoLev x7 ∈ y3.
Assume H11: SNoLt x7 (binintersect x2 (SNoElts_ y3)).
Apply SepI with SNoL x2, λ x8 . SNoLev x8 ∈ y3, x7 leaving 2 subgoals.
Apply SNoL_I with x2, x7 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H9.
Apply ordinal_TransSet with SNoLev x2, y3, SNoLev x7 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H1.
The subproof is completed by applying H10.
Apply SNoLtE with x7, binintersect x2 (SNoElts_ y3), SNoLt x7 x2 leaving 6 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying L6.
The subproof is completed by applying H11.
Let x8 of type ι be given.
Assume H12: SNo x8.
Apply restr_SNoLev with x2, y3, λ x9 x10 . ... ⟶ SNoEq_ ... ... ... ⟶ SNoEq_ (SNoLev x8) x8 (binintersect x2 (SNoElts_ y3)) ⟶ SNoLt x7 x8 ⟶ SNoLt x8 (binintersect x2 (SNoElts_ y3)) ⟶ nIn (SNoLev x8) x7 ⟶ SNoLev x8 ∈ binintersect x2 (SNoElts_ y3) ⟶ SNoLt x7 x2 leaving 3 subgoals.
...
...
...
...
...
...
...
...
Let x5 of type ι → ι → ο be given.
Apply L7 with λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H8: x5 y4 y4.
The subproof is completed by applying H8.
Apply H2 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L7.
■