Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  unisnALT Unicode version

Theorem unisnALT 30508
Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. The User manually input on a mmj2 Proof Worksheet, without labels, all steps of unisnALT 30508 except 1, 11, 15, 21, and 30. With execution of the mmj2 unification command, mmj2 could find labels for all steps except for 2, 12, 16, 22, and 31 (and the then non-existing steps 1, 11, 15, 21, and 30) . mmj2 could not find reference theorems for those five steps because the hypothesis field of each of these steps was empty and none of those steps unifies with a theorem in set.mm. Each of these five steps is a semantic variation of a theorem in set.mm and is 2-step provable. mmj2 does not have the ability to automatically generate the semantic variation in set.mm of a theorem in a mmj2 Proof Worksheet unless the theorem in the Proof Worksheet is labeled with a 1-hypothesis deduction whose hypothesis is a theorem in set.mm which unifies with the theorem in the Proof Worksheet. The stepprover.c program, which invokes mmj2, has this capability. stepprover.c automatically generated steps 1, 11, 15, 21, and 30, labeled all steps, and generated the RPN proof of unisnALT 30508. Roughly speaking, stepprover.c added to the Proof Worksheet a labeled duplicate step of each non-unifying theorem for each label in a text file, labels.txt, containing a list of labels provided by the User. Upon mmj2 unification, stepprover.c identified a label for each of the five theorems which 2-step proves it. For unisnALT 30508, the label list is a list of all 1-hypothesis propositional calculus deductions in set.mm. stepproverp.c is the same as stepprover.c except that it intermittently pauses during execution, allowing the User to observe the changes to a text file caused by the execution of particular statements of the program. (Contributed by Alan Sare, 19-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
unisnALT.1
Assertion
Ref Expression
unisnALT

Proof of Theorem unisnALT
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni 4120 . . . . . 6
21biimpi 188 . . . . 5
3 id 21 . . . . . . . . 9
4 simpl 445 . . . . . . . . 9
53, 4syl 16 . . . . . . . 8
6 simpr 449 . . . . . . . . . 10
73, 6syl 16 . . . . . . . . 9
8 elsni 3934 . . . . . . . . 9
97, 8syl 16 . . . . . . . 8
10 eleq2 2550 . . . . . . . . 9
1110biimpac 474 . . . . . . . 8
125, 9, 11syl2anc 644 . . . . . . 7
1312ax-gen 1570 . . . . . 6
14 19.23v 1918 . . . . . . 7
1514biimpi 188 . . . . . 6
1613, 15ax-mp 5 . . . . 5
17 pm3.35 572 . . . . 5
182, 16, 17sylancl 645 . . . 4
1918ax-gen 1570 . . 3
20 dfss2 3382 . . . 4
2120biimpri 199 . . 3
2219, 21ax-mp 5 . 2
23 id 21 . . . . 5
24 unisnALT.1 . . . . . 6
2524snid 3937 . . . . 5
26 elunii 4122 . . . . 5
2723, 25, 26sylancl 645 . . . 4
2827ax-gen 1570 . . 3
29 dfss2 3382 . . . 4
3029biimpri 199 . . 3
3128, 30ax-mp 5 . 2
3222, 31eqssi 3409 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  A.wal 1564  E.wex 1565  =wceq 1670  e.wcel 1732   cvv 3015  C_wss 3365  {csn 3909  U.cuni 4117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-v 3017  df-in 3372  df-ss 3379  df-sn 3915  df-uni 4118
  Copyright terms: Public domain W3C validator