 Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sucidALTVD Structured version   Visualization version   GIF version

Theorem sucidALTVD 39522
Description: A set belongs to its successor. Alternate proof of sucid 5917. 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 39523 is sucidALTVD 39522 without virtual deductions and was automatically derived from sucidALTVD 39522. 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 𝐴 = (𝐴 ∪ {𝐴}), which unifies with df-suc 5842, 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 𝐴 infers 𝑥𝐴𝑦𝐴(𝑥𝑦𝑥 = 𝑦𝑦𝑥) is a semantic variation of the theorem (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 𝑦𝐴(𝑥𝑦𝑥 = 𝑦𝑦𝑥))), which unifies with the set.mm reference definition (axiom) dford2 8630.
 h1:: ⊢ 𝐴 ∈ V 2:1: ⊢ 𝐴 ∈ {𝐴} 3:2: ⊢ 𝐴 ∈ ({𝐴} ∪ 𝐴) 4:: ⊢ suc 𝐴 = ({𝐴} ∪ 𝐴) qed:3,4: ⊢ 𝐴 ∈ suc 𝐴
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
sucidALTVD.1 𝐴 ∈ V
Assertion
Ref Expression
sucidALTVD 𝐴 ∈ suc 𝐴

Proof of Theorem sucidALTVD
StepHypRef Expression
1 sucidALTVD.1 . . . 4 𝐴 ∈ V
21snid 4316 . . 3 𝐴 ∈ {𝐴}
3 elun1 3888 . . 3 (𝐴 ∈ {𝐴} → 𝐴 ∈ ({𝐴} ∪ 𝐴))
42, 3e0a 39418 . 2 𝐴 ∈ ({𝐴} ∪ 𝐴)
5 df-suc 5842 . . 3 suc 𝐴 = (𝐴 ∪ {𝐴})
65equncomi 3867 . 2 suc 𝐴 = ({𝐴} ∪ 𝐴)
74, 6eleqtrri 2802 1 𝐴 ∈ suc 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2103  Vcvv 3304   ∪ cun 3678  {csn 4285  suc csuc 5838 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685  df-in 3687  df-ss 3694  df-sn 4286  df-suc 5842 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator