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

Theorem unisnALT 33869
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 33869 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 33869. 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 33869, 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 4254 . . . . . 6  |-  ( x  e.  U. { A } 
<->  E. q ( x  e.  q  /\  q  e.  { A } ) )
21biimpi 194 . . . . 5  |-  ( x  e.  U. { A }  ->  E. q ( x  e.  q  /\  q  e.  { A } ) )
3 id 22 . . . . . . . . 9  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  (
x  e.  q  /\  q  e.  { A } ) )
4 simpl 457 . . . . . . . . 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 461 . . . . . . . . . 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 4057 . . . . . . . . 9  |-  ( q  e.  { A }  ->  q  =  A )
97, 8syl 16 . . . . . . . 8  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  q  =  A )
10 eleq2 2530 . . . . . . . . 9  |-  ( q  =  A  ->  (
x  e.  q  <->  x  e.  A ) )
1110biimpac 486 . . . . . . . 8  |-  ( ( x  e.  q  /\  q  =  A )  ->  x  e.  A )
125, 9, 11syl2anc 661 . . . . . . 7  |-  ( ( x  e.  q  /\  q  e.  { A } )  ->  x  e.  A )
1312ax-gen 1619 . . . . . 6  |-  A. q
( ( x  e.  q  /\  q  e. 
{ A } )  ->  x  e.  A
)
14 19.23v 1761 . . . . . . 7  |-  ( A. q ( ( x  e.  q  /\  q  e.  { A } )  ->  x  e.  A
)  <->  ( E. q
( x  e.  q  /\  q  e.  { A } )  ->  x  e.  A ) )
1514biimpi 194 . . . . . 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 5 . . . . 5  |-  ( E. q ( x  e.  q  /\  q  e. 
{ A } )  ->  x  e.  A
)
17 pm3.35 587 . . . . 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 662 . . . 4  |-  ( x  e.  U. { A }  ->  x  e.  A
)
1918ax-gen 1619 . . 3  |-  A. x
( x  e.  U. { A }  ->  x  e.  A )
20 dfss2 3488 . . . 4  |-  ( U. { A }  C_  A  <->  A. x ( x  e. 
U. { A }  ->  x  e.  A ) )
2120biimpri 206 . . 3  |-  ( A. x ( x  e. 
U. { A }  ->  x  e.  A )  ->  U. { A }  C_  A )
2219, 21ax-mp 5 . 2  |-  U. { A }  C_  A
23 id 22 . . . . 5  |-  ( x  e.  A  ->  x  e.  A )
24 unisnALT.1 . . . . . 6  |-  A  e. 
_V
2524snid 4060 . . . . 5  |-  A  e. 
{ A }
26 elunii 4256 . . . . 5  |-  ( ( x  e.  A  /\  A  e.  { A } )  ->  x  e.  U. { A }
)
2723, 25, 26sylancl 662 . . . 4  |-  ( x  e.  A  ->  x  e.  U. { A }
)
2827ax-gen 1619 . . 3  |-  A. x
( x  e.  A  ->  x  e.  U. { A } )
29 dfss2 3488 . . . 4  |-  ( A 
C_  U. { A }  <->  A. x ( x  e.  A  ->  x  e.  U. { A } ) )
3029biimpri 206 . . 3  |-  ( A. x ( x  e.  A  ->  x  e.  U. { A } )  ->  A  C_  U. { A } )
3128, 30ax-mp 5 . 2  |-  A  C_  U. { A }
3222, 31eqssi 3515 1  |-  U. { A }  =  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1393    = wceq 1395   E.wex 1613    e. wcel 1819   _Vcvv 3109    C_ wss 3471   {csn 4032   U.cuni 4251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-ss 3485  df-sn 4033  df-uni 4252
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator