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

Theorem unisnALT 28380
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 28380 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 28380. 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 28380, 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 3961 . . . . . 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 3782 . . . . . . . . 9  |-  ( q  e.  { A }  ->  q  =  A )
97, 8syl 16 . . . . . . . 8  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  q  =  A )
10 eleq2 2449 . . . . . . . . 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 1552 . . . . . 6  |-  A. q
( ( x  e.  q  /\  q  e. 
{ A } )  ->  x  e.  A
)
14 19.23v 1903 . . . . . . 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 1552 . . 3  |-  A. x
( x  e.  U. { A }  ->  x  e.  A )
20 dfss2 3281 . . . 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 3785 . . . . 5  |-  A  e. 
{ A }
26 elunii 3963 . . . . 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 1552 . . 3  |-  A. x
( x  e.  A  ->  x  e.  U. { A } )
29 dfss2 3281 . . . 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 3308 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1717   _Vcvv 2900    C_ wss 3264   {csn 3758   U.cuni 3958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-in 3271  df-ss 3278  df-sn 3764  df-uni 3959
  Copyright terms: Public domain W3C validator