Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Apply set_ext with SNoL (minus_SNo x0), {minus_SNo x1|x1 ∈ SNoR x0} leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: x1 ∈ SNoL (minus_SNo x0).
Apply SNoL_E with minus_SNo x0, x1, x1 ∈ prim5 (SNoR x0) minus_SNo leaving 3 subgoals.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2: SNo x1.
Apply minus_SNo_Lev with x0, λ x2 x3 . SNoLev x1 ∈ x3 ⟶ SNoLt x1 (minus_SNo x0) ⟶ x1 ∈ prim5 (SNoR x0) minus_SNo leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H3: SNoLev x1 ∈ SNoLev x0.
Assume H4: SNoLt x1 (minus_SNo x0).
Apply minus_SNo_invol with x1, λ x2 x3 . x2 ∈ {minus_SNo x4|x4 ∈ SNoR x0} leaving 2 subgoals.
The subproof is completed by applying H2.
Apply ReplI with SNoR x0, minus_SNo, minus_SNo x1.
Apply SNoR_I with x0, minus_SNo x1 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying H2.
Apply minus_SNo_Lev with x1, λ x2 x3 . x3 ∈ SNoLev x0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply minus_SNo_Lt_contra2 with x1, x0 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H1: x1 ∈ {minus_SNo x2|x2 ∈ SNoR x0}.
Apply ReplE_impred with SNoR x0, minus_SNo, x1, x1 ∈ SNoL (minus_SNo x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ SNoR x0.
Assume H3: x1 = minus_SNo x2.
Apply H3 with λ x3 x4 . x4 ∈ SNoL (minus_SNo x0).
Apply SNoR_E with x0, x2, minus_SNo x2 ∈ SNoL (minus_SNo x0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Assume H4: SNo x2.
Assume H5: SNoLev x2 ∈ SNoLev x0.
Assume H6: SNoLt x0 x2.
Apply SNoL_I with minus_SNo x0, minus_SNo x2 leaving 4 subgoals.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with x2.
The subproof is completed by applying H4.
Apply minus_SNo_Lev with x2, λ x3 x4 . x4 ∈ SNoLev (minus_SNo x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply minus_SNo_Lev with x0, λ x3 x4 . SNoLev x2 ∈ x4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
Apply minus_SNo_Lt_contra with x0, x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
■