Description: A set belongs to its successor. Alternate proof of sucid .
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. sucidALT is sucidALTVD without virtual deductions and was automatically derived from
sucidALTVD . This proof illustrates that
completeusersproof.cmd will generate a Metamath proof from any
User's Proof which is "conventional" in the sense that no step
is a virtual deduction, provided that all necessary unification
theorems and transformation deductions are in set.mm.
completeusersproof.cmd automatically converts such a
conventional proof into a Virtual Deduction proof for which each
step happens to be a 0-virtual hypothesis virtual deduction.
The user does not need to search for reference theorem labels or
deduction labels nor does he(she) need to use theorems and
deductions which unify with reference theorems and deductions in
set.mm. All that is necessary is that each theorem or deduction
of the User's Proof unifies with some reference theorem or
deduction in set.mm or is a semantic variation of some theorem
or deduction which unifies with some reference theorem or
deduction in set.mm. The definition of "semantic variation" has
not been precisely defined. If it is obvious that a theorem or
deduction has the same meaning as another theorem or deduction,
then it is a semantic variation of the latter theorem or
deduction. For example, step 4 of the User's Proof is a
semantic variation of the definition (axiom)
suc A = ( A u. { A } ) , which unifies with df-suc , a
reference definition (axiom) in set.mm. Also, a theorem or
deduction is said to be a semantic variation of another
theorem or deduction if it is obvious upon cursory inspection
that it has the same meaning as a weaker form of the latter
theorem or deduction. For example, the deduction Ord A
infers A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) is a
semantic variation of the theorem ( Ord A <-> ( Tr A /\ A. x e. AA. y e. A ( x e. y \/ x = y \/ y e. x ) ) ) , which unifies with
the set.mm reference definition (axiom) dford2 .
h1::
|- A e. _V
2:1:
|- A e. { A }
3:2:
|- A e. ( { A } u. A )
4::
|- suc A = ( { A } u. A )
qed:3,4:
|- A e. suc A
(Contributed by Alan Sare, 18-Feb-2012) (Proof modification is
discouraged.) (New usage is discouraged.)