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

Theorem unisnALT 28975
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 28975 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 28975. 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 28975, 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  |-  A  e. 
_V
Assertion
Ref Expression
unisnALT  |-  U. { A }  =  A

Proof of Theorem unisnALT
Dummy variables  x  q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluni 4010 . . . . . 6  |-  ( x  e.  U. { A } 
<->  E. q ( x  e.  q  /\  q  e.  { A } ) )
21biimpi 187 . . . . 5  |-  ( x  e.  U. { A }  ->  E. q ( x  e.  q  /\  q  e.  { A } ) )
3 id 20 . . . . . . . . 9  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  (
x  e.  q  /\  q  e.  { A } ) )
4 simpl 444 . . . . . . . . 9  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  x  e.  q )
53, 4syl 16 . . . . . . . 8  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  x  e.  q )
6 simpr 448 . . . . . . . . . 10  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  q  e.  { A } )
73, 6syl 16 . . . . . . . . 9  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  q  e.  { A } )
8 elsni 3830 . . . . . . . . 9  |-  ( q  e.  { A }  ->  q  =  A )
97, 8syl 16 . . . . . . . 8  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  q  =  A )
10 eleq2 2496 . . . . . . . . 9  |-  ( q  =  A  ->  (
x  e.  q  <->  x  e.  A ) )
1110biimpac 473 . . . . . . . 8  |-  ( ( x  e.  q  /\  q  =  A )  ->  x  e.  A )
125, 9, 11syl2anc 643 . . . . . . 7  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  x  e.  A )
1312ax-gen 1555 . . . . . 6  |-  A. q
( ( x  e.  q  /\  q  e. 
{ A } )  ->  x  e.  A
)
14 19.23v 1914 . . . . . . 7  |-  ( A. q ( ( x  e.  q  /\  q  e.  { A } )  ->  x  e.  A
)  <->  ( E. q
( x  e.  q  /\  q  e.  { A } )  ->  x  e.  A ) )
1514biimpi 187 . . . . . 6  |-  ( A. q ( ( x  e.  q  /\  q  e.  { A } )  ->  x  e.  A
)  ->  ( E. q ( x  e.  q  /\  q  e. 
{ A } )  ->  x  e.  A
) )
1613, 15ax-mp 8 . . . . 5  |-  ( E. q ( x  e.  q  /\  q  e. 
{ A } )  ->  x  e.  A
)
17 pm3.35 571 . . . . 5  |-  ( ( E. q ( x  e.  q  /\  q  e.  { A } )  /\  ( E. q
( x  e.  q  /\  q  e.  { A } )  ->  x  e.  A ) )  ->  x  e.  A )
182, 16, 17sylancl 644 . . . 4  |-  ( x  e.  U. { A }  ->  x  e.  A
)
1918ax-gen 1555 . . 3  |-  A. x
( x  e.  U. { A }  ->  x  e.  A )
20 dfss2 3329 . . . 4  |-  ( U. { A }  C_  A  <->  A. x ( x  e. 
U. { A }  ->  x  e.  A ) )
2120biimpri 198 . . 3  |-  ( A. x ( x  e. 
U. { A }  ->  x  e.  A )  ->  U. { A }  C_  A )
2219, 21ax-mp 8 . 2  |-  U. { A }  C_  A
23 id 20 . . . . 5  |-  ( x  e.  A  ->  x  e.  A )
24 unisnALT.1 . . . . . 6  |-  A  e. 
_V
2524snid 3833 . . . . 5  |-  A  e. 
{ A }
26 elunii 4012 . . . . 5  |-  ( ( x  e.  A  /\  A  e.  { A } )  ->  x  e.  U. { A }
)
2723, 25, 26sylancl 644 . . . 4  |-  ( x  e.  A  ->  x  e.  U. { A }
)
2827ax-gen 1555 . . 3  |-  A. x
( x  e.  A  ->  x  e.  U. { A } )
29 dfss2 3329 . . . 4  |-  ( A 
C_  U. { A }  <->  A. x ( x  e.  A  ->  x  e.  U. { A } ) )
3029biimpri 198 . . 3  |-  ( A. x ( x  e.  A  ->  x  e.  U. { A } )  ->  A  C_  U. { A } )
3128, 30ax-mp 8 . 2  |-  A  C_  U. { A }
3222, 31eqssi 3356 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725   _Vcvv 2948    C_ wss 3312   {csn 3806   U.cuni 4007
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-sn 3812  df-uni 4008
  Copyright terms: Public domain W3C validator