Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent Other  >  MM 100

Most recent proofs    These are the 10 (GIF, Unicode) or 1000 (GIF, Unicode) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from develop commit 1f5ae48, also available here: set.mm (30MB) or set.mm.bz2 (compressed, 8MB).

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 17-Jun-2017 .    Syndication: RSS feed (courtesy of Dan Getz).    Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.

Recent news items    (7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.

(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.

(13-Apr-2017) See equidK for a discussion of the recent theorems in my mathbox. -NM

(24-Mar-2017) Alan Sare updated his completeusersproof program.

(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.

(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).

(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.

(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60.

(28-Dec-2016) David A. Wheeler is putting together a page on Metamath (specifically set.mm) conventions. Comments are welcome on the Google Group thread.

(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph" (symbols: turned F, x, phi) in df-nf to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )". Theorem nf2 shows a version without nested quantifiers.

(22-Dec-2016) Naip Moro has developed a Metamath database for G. Spencer-Brown's Laws of Form. You can follow the Google Group discussion here.

(20-Dec-2016) In metamath program version 0.137, 'verify markup *' now checks that ax-XXX $a matches axXXX $p when the latter exists, per the discussion at https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ.

(24-Nov-2016) Mingl Yuan has kindly provided a mirror site in Beijing, China. He has also provided an rsync server; type "rsync cn.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").

(14-Aug-2016) All HTML pages on this site should now be mobile-friendly and pass the Mobile-Friendly Test. If you find one that does not, let me know.

(14-Aug-2016) Daniel Whalen wrote a paper describing the use of using deep learning to prove 14% of test theorems taken from set.mm: Holophrasm: a neural Automated Theorem Prover for higher-order logic. The associated program is called Holophrasm.

(14-Aug-2016) David A. Wheeler created a video called Metamath Proof Explorer: A Modern Principia Mathematica

(12-Aug-2016) A Gitter chat room has been created for Metamath.

(9-Aug-2016) Mario Carneiro wrote a Metamath proof verifier in the Scala language as part of the ongoing Metamath -> MMT import project

(9-Aug-2016) David A. Wheeler created a GitHub project called metamath-test (last execution run) to check that different verifiers both pass good databases and detect errors in defective ones.

(4-Aug-2016) Mario gave two presentations at CICM 2016.

(17-Jul-2016) Thierry Arnoux has written EMetamath, a Metamath plugin for the Eclipse IDE.

(16-Jul-2016) Mario recovered Chris Capel's collapsible proof demo.

(13-Jul-2016) FL sent me an updated version of PDF (LaTeX source) developed with Lamport's pf2 package. See the 23-Apr-2012 entry below.

(12-Jul-2016) David A. Wheeler produced a new video for mmj2 called "Creating functions in Metamath". It shows a more efficient approach than his previous recent video "Creating functions in Metamath" (old) but it can be of interest to see both approaches.

(10-Jul-2016) Metamath program version 0.132 changes the command 'show restricted' to 'show discouraged' and adds a new command, 'set discouragement'. See the mmnotes.txt entry of 11-May-2016 (updated 10-Jul-2016).

(12-Jun-2016) Dan Getz has written Metamath.jl, a Metamath proof verifier written in the Julia language.    Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 18-Jun-2017 at 1:06 PM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 14-May-2017 )
DateLabelDescription
Theorem
 
17-Jun-2017idomsubgmo 26867 The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.)
 |-  G  =  ( (mulGrp `  R )s  (Unit `  R ) )   =>    |-  ( ( R  e. IDomn  /\  N  e.  NN )  ->  E* y  e.  (SubGrp `  G ) ( # `  y )  =  N )
 
17-Jun-2017hilbert1.2 24139 There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.)
 |-  ( P  =/=  Q  ->  E* x  e. LinesEE ( P  e.  x  /\  Q  e.  x ) )
 
17-Jun-2017cvmliftmo 23173 A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by NM, 17-Jun-2017.)
 |-  B  =  U. C   &    |-  Y  =  U. K   &    |-  ( ph  ->  F  e.  ( C CovMap  J )
 )   &    |-  ( ph  ->  K  e.  Con )   &    |-  ( ph  ->  K  e. 𝑛Locally  Con )   &    |-  ( ph  ->  O  e.  Y )   &    |-  ( ph  ->  G  e.  ( K  Cn  J ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  ( F `  P )  =  ( G `  O ) )   =>    |-  ( ph  ->  E* f  e.  ( K  Cn  C ) ( ( F  o.  f
 )  =  G  /\  ( f `  O )  =  P )
 )
 
17-Jun-2017ply1divmo 19469 Uniqueness of a quotient in a polynomial division. For polynomials  F ,  G such that  G  =/=  0 and the leading coefficient of  G is not a zero divisor, there is at most one polynomial  q which satisfies  F  =  ( G  x.  q )  +  r where the degree of  r is less than the degree of  G. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.)
 |-  P  =  (Poly1 `  R )   &    |-  D  =  ( deg1  `  R )   &    |-  B  =  ( Base `  P )   &    |-  .-  =  ( -g `  P )   &    |-  .0.  =  ( 0g `  P )   &    |-  .xb  =  ( .r `  P )   &    |-  ( ph  ->  R  e.  Ring )   &    |-  ( ph  ->  F  e.  B )   &    |-  ( ph  ->  G  e.  B )   &    |-  ( ph  ->  G  =/=  .0.  )   &    |-  ( ph  ->  ( (coe1 `  G ) `  ( D `  G ) )  e.  E )   &    |-  E  =  (RLReg `  R )   =>    |-  ( ph  ->  E* q  e.  B ( D `  ( F  .-  ( G 
 .xb  q ) ) )  <  ( D `
  G ) )
 
17-Jun-20172ndcdisj2 17131 Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)
 |-  ( ( J  e.  2ndc  /\  A  C_  J  /\  A. y E* x  e.  A y  e.  x )  ->  A  ~<_  om )
 
17-Jun-20172ndcdisj 17130 Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)
 |-  ( ( J  e.  2ndc  /\  A. x  e.  A  B  e.  ( J  \  { (/) } )  /\  A. y E* x  e.  A y  e.  B )  ->  A  ~<_  om )
 
17-Jun-2017lspextmo 15761 A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by NM, 17-Jun-2017.)
 |-  B  =  ( Base `  S )   &    |-  K  =  (
 LSpan `  S )   =>    |-  ( ( X 
 C_  B  /\  ( K `  X )  =  B )  ->  E* g  e.  ( S LMHom  T ) ( g  |`  X )  =  F )
 
17-Jun-2017mgmidmo 14318 A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.)
 |- 
 E* u  e.  B A. x  e.  B  ( ( u  .+  x )  =  x  /\  ( x  .+  u )  =  x )
 
17-Jun-2017sqrmo 11688 Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.)
 |-  ( A  e.  CC  ->  E* x  e.  CC ( ( x ^
 2 )  =  A  /\  0  <_  ( Re
 `  x )  /\  ( _i  x.  x )  e/  RR+ ) )
 
17-Jun-2017rmorabex 4191 Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.)
 |-  ( E* x  e.  A ph  ->  { x  e.  A  |  ph }  e.  _V )
 
17-Jun-2017dfdisj2 3955 Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.)
 |-  (Disj  x  e.  A B 
 <-> 
 A. y E* x ( x  e.  A  /\  y  e.  B ) )
 
17-Jun-2017rmo2i 3038 Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.)
 |- 
 F/ y ph   =>    |-  ( E. y  e.  A  A. x  e.  A  ( ph  ->  x  =  y )  ->  E* x  e.  A ph )
 
17-Jun-2017rmo2 3037 Alternate definition of restricted "at most one." Note that  E* x  e.  A ph is not equivalent to  E. y  e.  A A. x  e.  A ( ph  ->  x  =  y ) (in analogy to reu6 2922); to see this, let  A be the empty set. However, one direction of this pattern holds; see rmo2i 3038. (Contributed by NM, 17-Jun-2017.)
 |- 
 F/ y ph   =>    |-  ( E* x  e.  A ph  <->  E. y A. x  e.  A  ( ph  ->  x  =  y ) )
 
17-Jun-2017nrexrmo 2727 Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.)
 |-  ( -.  E. x  e.  A  ph  ->  E* x  e.  A ph )
 
17-Jun-2017nfrmod 2686 Deduction version of nfrmo 2688. (Contributed by NM, 17-Jun-2017.)
 |- 
 F/ y ph   &    |-  ( ph  ->  F/_ x A )   &    |-  ( ph  ->  F/ x ps )   =>    |-  ( ph  ->  F/ x E* y  e.  A ps )
 
16-Jun-2017spwmo 14283 A poset has at most one supremum. (Contributed by NM, 13-May-2008.) (Revised by NM, 16-Jun-2017.)
 |-  ( ph  <->  ( A. y  e.  A  y R x 
 /\  A. y  e.  X  ( A. z  e.  A  z R y  ->  x R y ) ) )   =>    |-  ( R  e.  PosetRel  ->  E* x  e.  X ph )
 
16-Jun-2017poslubmo 14198 Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.)
 |- 
 .<_  =  ( le `  K )   &    |-  B  =  ( Base `  K )   =>    |-  ( ( K  e.  Poset  /\  S  C_  B )  ->  E* x  e.  B ( A. y  e.  S  y  .<_  x  /\  A. z  e.  B  ( A. y  e.  S  y  .<_  z  ->  x  .<_  z ) ) )
 
16-Jun-2017brdom7disj 8110 An equivalence to a dominance relation for disjoint sets. (Contributed by NM, 29-Mar-2007.) (Revised by NM, 16-Jun-2017.)
 |-  A  e.  _V   &    |-  B  e.  _V   &    |-  ( A  i^i  B )  =  (/)   =>    |-  ( A  ~<_  B  <->  E. f ( A. x  e.  B  E* y  e.  A { x ,  y }  e.  f  /\  A. x  e.  A  E. y  e.  B  { y ,  x }  e.  f
 ) )
 
16-Jun-2017brdom4 8109 An equivalence to a dominance relation. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
 |-  B  e.  _V   =>    |-  ( A  ~<_  B  <->  E. f ( A. x  e.  B  E* y  e.  A x f y  /\  A. x  e.  A  E. y  e.  B  y f x ) )
 
16-Jun-2017iunmapdisj 7604 The union  U_ n  e.  C ( A  ^m  n ) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.)
 |- 
 E* n  e.  C B  e.  ( A  ^m  n )
 
16-Jun-2017moriotass 6288 Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
 |-  ( ( A  C_  B  /\  E. x  e.  A  ph  /\  E* x  e.  B ph )  ->  ( iota_ x  e.  A ph )  =  ( iota_ x  e.  B ph )
 )
 
16-Jun-2017dffun9 5207 Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.)
 |-  ( Fun  A  <->  ( Rel  A  /\  A. x  e.  dom  A E* y  e.  ran  A  x A y ) )
 
16-Jun-2017reuxfr2 4516 Transfer existential uniqueness from a variable  x to another variable  y contained in expression  A. (Contributed by NM, 14-Nov-2004.) (Revised by NM, 16-Jun-2017.)
 |-  ( y  e.  B  ->  A  e.  B )   &    |-  ( x  e.  B  ->  E* y  e.  B x  =  A )   =>    |-  ( E! x  e.  B  E. y  e.  B  ( x  =  A  /\  ph )  <->  E! y  e.  B  ph )
 
16-Jun-2017reuxfr2d 4515 Transfer existential uniqueness from a variable  x to another variable  y contained in expression  A. (Contributed by NM, 16-Jan-2012.) (Revised by NM, 16-Jun-2017.)
 |-  ( ( ph  /\  y  e.  B )  ->  A  e.  B )   &    |-  ( ( ph  /\  x  e.  B ) 
 ->  E* y  e.  B x  =  A )   =>    |-  ( ph  ->  ( E! x  e.  B  E. y  e.  B  ( x  =  A  /\  ps )  <->  E! y  e.  B  ps ) )
 
16-Jun-2017somo 4306 A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by NM, 16-Jun-2017.)
 |-  ( R  Or  A  ->  E* x  e.  A A. y  e.  A  -.  y R x )
 
16-Jun-2017df-disj 3954 A collection of classes  B ( x ) is disjoint when for each element  y, it is in  B ( x ) for at most one  x. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.)
 |-  (Disj  x  e.  A B 
 <-> 
 A. y E* x  e.  A y  e.  B )
 
16-Jun-2017rmoi 3041 Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
 |-  ( x  =  B  ->  ( ph  <->  ps ) )   &    |-  ( x  =  C  ->  (
 ph 
 <->  ch ) )   =>    |-  ( ( E* x  e.  A ph  /\  ( B  e.  A  /\  ps )  /\  ( C  e.  A  /\  ch ) )  ->  B  =  C )
 
16-Jun-2017rmob 3040 Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
 |-  ( x  =  B  ->  ( ph  <->  ps ) )   &    |-  ( x  =  C  ->  (
 ph 
 <->  ch ) )   =>    |-  ( ( E* x  e.  A ph  /\  ( B  e.  A  /\  ps ) )  ->  ( B  =  C  <->  ( C  e.  A  /\  ch ) ) )
 
16-Jun-2017rmo3 3039 Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
 |- 
 F/ y ph   =>    |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  ( ( ph  /\  [
 y  /  x ] ph )  ->  x  =  y ) )
 
16-Jun-20172reuswap 2933 A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by NM, 16-Jun-2017.)
 |-  ( A. x  e.  A  E* y  e.  B ph  ->  ( E! x  e.  A  E. y  e.  B  ph 
 ->  E! y  e.  B  E. x  e.  A  ph ) )
 
16-Jun-2017imrmo 2932 Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by NM, 16-Jun-2017.)
 |-  ( A. x  e.  A  ( ph  ->  ps )  ->  ( E* x  e.  A ps  ->  E* x  e.  A ph ) )
 
16-Jun-2017rmoan 2931 Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017.)
 |-  ( E* x  e.  A ph  ->  E* x  e.  A ( ps  /\  ph ) )
 
16-Jun-2017rmo4 2926 Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  ( ( ph  /\  ps )  ->  x  =  y ) )
 
16-Jun-2017cbvrmo 2733 Change the bound variable of restricted "at most one" using implicit substitution. (Contributed by NM, 16-Jun-2017.)
 |- 
 F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E* x  e.  A ph  <->  E* y  e.  A ps )
 
16-Jun-2017rmo5 2726 Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.)
 |-  ( E* x  e.  A ph  <->  ( E. x  e.  A  ph  ->  E! x  e.  A  ph ) )
 
16-Jun-2017reurmo 2725 Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
 |-  ( E! x  e.  A  ph  ->  E* x  e.  A ph )
 
16-Jun-2017reu5 2723 Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
 |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph  /\  E* x  e.  A ph ) )
 
16-Jun-2017mormo 2722 Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.)
 |-  ( E* x ph  ->  E* x  e.  A ph )
 
16-Jun-2017rmobii 2704 Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.)
 |-  ( ph  <->  ps )   =>    |-  ( E* x  e.  A ph  <->  E* x  e.  A ps )
 
16-Jun-2017rmobiia 2703 Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.)
 |-  ( x  e.  A  ->  ( ph  <->  ps ) )   =>    |-  ( E* x  e.  A ph  <->  E* x  e.  A ps )
 
16-Jun-2017rmobidv 2702 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E* x  e.  A ps 
 <->  E* x  e.  A ch ) )
 
16-Jun-2017rmobidva 2701 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.)
 |-  ( ( ph  /\  x  e.  A )  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E* x  e.  A ps 
 <->  E* x  e.  A ch ) )
 
16-Jun-2017rmobida 2700 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.)
 |- 
 F/ x ph   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E* x  e.  A ps 
 <->  E* x  e.  A ch ) )
 
16-Jun-2017nfrmo 2688 Bound-variable hypothesis builder for restricted uniqueness. (Contributed by NM, 16-Jun-2017.)
 |-  F/_ x A   &    |-  F/ x ph   =>    |-  F/ x E* y  e.  A ph
 
16-Jun-2017nfrmo1 2684  x is not free in  E* x  e.  A ph. (Contributed by NM, 16-Jun-2017.)
 |- 
 F/ x E* x  e.  A ph
 
16-Jun-2017df-rmo 2524 Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
 |-  ( E* x  e.  A ph  <->  E* x ( x  e.  A  /\  ph )
 )
 
18-May-2017fsnunfv 5640 Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)
 |-  ( ( X  e.  V  /\  Y  e.  W  /\  -.  X  e.  dom  F )  ->  ( ( F  u.  { <. X ,  Y >. } ) `  X )  =  Y )
 
5-May-2017ballotlemsima 23021 The image by  S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( S `  C ) " (
 1 ... J ) )  =  ( ( ( S `  C ) `
  J ) ... ( I `  C ) ) )
 
2-May-2017addeq0 22990 Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.)
 |-  (
 ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  =  0  <->  A  =  -u B ) )
 
2-May-2017fzsplit3 22977 Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.)
 |-  ( K  e.  ( M ... N )  ->  ( M ... N )  =  ( ( M ... ( K  -  1
 ) )  u.  ( K ... N ) ) )
 
2-May-2017ax12b 1834 Two equivalent ways of expressing ax-12 1633. See the comment for ax-12 1633. (Contributed by NM, 2-May-2017.)
 |-  ( ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 ) 
 <->  ( -.  x  =  y  ->  ( -.  x  =  z  ->  ( y  =  z  ->  A. x  y  =  z ) ) ) )
 
1-May-2017lvecdim 15858 The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 15845 and lbsacsbs 15857 to show that being a basis for a vector space is equivalent to being a basis for the associated algebraic closure system, and then using acsexdimd 14234. (Contributed by David Moews, 1-May-2017.)
 |-  J  =  (LBasis `  W )   =>    |-  ( ( W  e.  LVec  /\  S  e.  J  /\  T  e.  J )  ->  S  ~~  T )
 
1-May-2017lbsacsbs 15857 Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 15855. (Contributed by David Moews, 1-May-2017.)
 |-  A  =  ( LSubSp `  W )   &    |-  N  =  (mrCls `  A )   &    |-  X  =  (
 Base `  W )   &    |-  I  =  (mrInd `  A )   &    |-  J  =  (LBasis `  W )   =>    |-  ( W  e.  LVec  ->  ( S  e.  J  <->  ( S  e.  I  /\  ( N `  S )  =  X ) ) )
 
1-May-2017lssacsex 15845 In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 15672 by lspsolv 15844. (Contributed by David Moews, 1-May-2017.)
 |-  A  =  ( LSubSp `  W )   &    |-  N  =  (mrCls `  A )   &    |-  X  =  (
 Base `  W )   =>    |-  ( W  e.  LVec 
 ->  ( A  e.  (ACS `  X )  /\  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y } ) )  \  ( N `  s ) ) y  e.  ( N `  ( s  u. 
 { z } )
 ) ) )
 
1-May-2017acsexdimd 14234 In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 13500 for the finite case and acsinfdimd 14233 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  e.  I
 )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   =>    |-  ( ph  ->  S  ~~  T )
 
1-May-2017acsinfdimd 14233 In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 14232 twice with acsinfd 14231. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  e.  I
 )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   &    |-  ( ph  ->  -.  S  e.  Fin )   =>    |-  ( ph  ->  S  ~~  T )
 
1-May-2017acsdomd 14232 In an algebraic closure system, if 
S and  T have the same closure and  S is infinite independent, then  T dominates  S. This follows from applying acsinfd 14231 and then applying unirnfdomd 8143 to the map given in acsmap2d 14230. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  C_  X )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   &    |-  ( ph  ->  -.  S  e.  Fin )   =>    |-  ( ph  ->  S  ~<_  T )
 
1-May-2017acsinfd 14231 In an algebraic closure system, if 
S and  T have the same closure and  S is infinite independent, then  T is infinite. This follows from applying unirnffid 7101 to the map given in acsmap2d 14230. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  C_  X )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   &    |-  ( ph  ->  -.  S  e.  Fin )   =>    |-  ( ph  ->  -.  T  e.  Fin )
 
1-May-2017acsmap2d 14230 In an algebraic closure system, if 
S and  T have the same closure and  S is independent, then there is a map  f from  T into the set of finite subsets of  S such that  S equals the union of  ran  f. This is proven by taking the map  f from acsmapd 14229 and observing that, since  S and  T have the same closure, the closure of  U. ran  f must contain  S. Since  S is independent, by mrissmrcd 13490,  U. ran  f must equal  S. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  C_  X )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   =>    |-  ( ph  ->  E. f
 ( f : T --> ( ~P S  i^i  Fin )  /\  S  =  U. ran  f ) )
 
1-May-2017acsmapd 14229 In an algebraic closure system, if 
T is contained in the closure of  S, there is a map  f from  T into the set of finite subsets of  S such that the closure of  U. ran  f contains  T. This is proven by applying acsficl2d 14227 to each element of  T. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  S 
 C_  X )   &    |-  ( ph  ->  T  C_  ( N `  S ) )   =>    |-  ( ph  ->  E. f
 ( f : T --> ( ~P S  i^i  Fin )  /\  T  C_  ( N `  U. ran  f
 ) ) )
 
1-May-2017acsfiindd 14228 In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( S  e.  I  <->  ( ~P S  i^i  Fin )  C_  I
 ) )
 
1-May-2017acsficl2d 14227 In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 14222. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( Y  e.  ( N `
  S )  <->  E. x  e.  ( ~P S  i^i  Fin ) Y  e.  ( N `  x ) ) )
 
1-May-2017acsficld 14226 In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 14222. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( N `  S )  =  U. ( N
 " ( ~P S  i^i  Fin ) ) )
 
1-May-2017acsmred 13506 An algebraic closure system is also a Moore system. Deduction form of acsmre 13502. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (ACS `  X )
 )   =>    |-  ( ph  ->  A  e.  (Moore `  X )
 )
 
1-May-2017mreexfidimd 13500 In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd 13499 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  e.  I
 )   &    |-  ( ph  ->  S  e.  Fin )   &    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )   =>    |-  ( ph  ->  S 
 ~~  T )
 
1-May-2017mreexdomd 13499 In a Moore system whose closure operator has the exchange property, if  S is independent and contained in the closure of  T, and either  S or  T is finite, then  T dominates  S. This is an immediate consequence of mreexexd 13498. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  S 
 C_  ( N `  T ) )   &    |-  ( ph  ->  T  C_  X )   &    |-  ( ph  ->  ( S  e.  Fin  \/  T  e.  Fin ) )   &    |-  ( ph  ->  S  e.  I
 )   =>    |-  ( ph  ->  S  ~<_  T )
 
1-May-2017mreexexd 13498 Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if  F and  G are disjoint from  H,  ( F  u.  H ) is independent,  F is contained in the closure of  ( G  u.  H ), and either  F or  G is finite, then there is a subset  q of  G equinumerous to  F such that  ( q  u.  H ) is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either  ( A  \  B ) or  ( B  \  A ) is finite. The theorem is proven by induction using mreexexlem3d 13496 for the base case and mreexexlem4d 13497 for the induction step. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  F 
 C_  ( X  \  H ) )   &    |-  ( ph  ->  G  C_  ( X  \  H ) )   &    |-  ( ph  ->  F  C_  ( N `  ( G  u.  H ) ) )   &    |-  ( ph  ->  ( F  u.  H )  e.  I
 )   &    |-  ( ph  ->  ( F  e.  Fin  \/  G  e.  Fin ) )   =>    |-  ( ph  ->  E. q  e.  ~P  G ( F  ~~  q  /\  ( q  u.  H )  e.  I )
 )
 
1-May-2017mreexexlem4d 13497 Induction step of the induction in mreexexd 13498. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  F 
 C_  ( X  \  H ) )   &    |-  ( ph  ->  G  C_  ( X  \  H ) )   &    |-  ( ph  ->  F  C_  ( N `  ( G  u.  H ) ) )   &    |-  ( ph  ->  ( F  u.  H )  e.  I
 )   &    |-  ( ph  ->  L  e.  om )   &    |-  ( ph  ->  A. h A. f  e. 
 ~P  ( X  \  h ) A. g  e.  ~P  ( X  \  h ) ( ( ( f  ~~  L  \/  g  ~~  L ) 
 /\  f  C_  ( N `  ( g  u.  h ) )  /\  ( f  u.  h )  e.  I )  ->  E. j  e.  ~P  g ( f  ~~  j  /\  ( j  u.  h )  e.  I
 ) ) )   &    |-  ( ph  ->  ( F  ~~  suc 
 L  \/  G  ~~  suc 
 L ) )   =>    |-  ( ph  ->  E. j  e.  ~P  G ( F  ~~  j  /\  ( j  u.  H )  e.  I )
 )
 
1-May-2017mreexexlem3d 13496 Base case of the induction in mreexexd 13498. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  F 
 C_  ( X  \  H ) )   &    |-  ( ph  ->  G  C_  ( X  \  H ) )   &    |-  ( ph  ->  F  C_  ( N `  ( G  u.  H ) ) )   &    |-  ( ph  ->  ( F  u.  H )  e.  I
 )   &    |-  ( ph  ->  ( F  =  (/)  \/  G  =  (/) ) )   =>    |-  ( ph  ->  E. i  e.  ~P  G ( F  ~~  i  /\  ( i  u.  H )  e.  I )
 )
 
1-May-2017mreexexlem2d 13495 Used in mreexexlem4d 13497 to prove the induction step in mreexexd 13498. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  F 
 C_  ( X  \  H ) )   &    |-  ( ph  ->  G  C_  ( X  \  H ) )   &    |-  ( ph  ->  F  C_  ( N `  ( G  u.  H ) ) )   &    |-  ( ph  ->  ( F  u.  H )  e.  I
 )   &    |-  ( ph  ->  Y  e.  F )   =>    |-  ( ph  ->  E. g  e.  G  ( -.  g  e.  ( F  \  { Y } )  /\  (
 ( F  \  { Y } )  u.  ( H  u.  { g }
 ) )  e.  I
 ) )
 
1-May-2017mreexexlemd 13494 This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 13498. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  X  e.  J )   &    |-  ( ph  ->  F 
 C_  ( X  \  H ) )   &    |-  ( ph  ->  G  C_  ( X  \  H ) )   &    |-  ( ph  ->  F  C_  ( N `  ( G  u.  H ) ) )   &    |-  ( ph  ->  ( F  u.  H )  e.  I
 )   &    |-  ( ph  ->  ( F  ~~  K  \/  G  ~~  K ) )   &    |-  ( ph  ->  A. t A. u  e.  ~P  ( X  \  t ) A. v  e.  ~P  ( X  \  t ) ( ( ( u  ~~  K  \/  v  ~~  K ) 
 /\  u  C_  ( N `  ( v  u.  t ) )  /\  ( u  u.  t
 )  e.  I ) 
 ->  E. i  e.  ~P  v ( u  ~~  i  /\  ( i  u.  t )  e.  I
 ) ) )   =>    |-  ( ph  ->  E. j  e.  ~P  G ( F  ~~  j  /\  ( j  u.  H )  e.  I )
 )
 
1-May-2017mreexmrid 13493 In a Moore system whose closure operator has the exchange property, if a set is independent and an element is not in its closure, then adding the element to the set gives another independent set. Lemma 4.1.5 in [FaureFrolicher] p. 84. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  Y  e.  X )   &    |-  ( ph  ->  -.  Y  e.  ( N `  S ) )   =>    |-  ( ph  ->  ( S  u.  { Y }
 )  e.  I )
 
1-May-2017mreexd 13492 In a Moore system, the closure operator is said to have the exchange property if, for all elements  y and  z of the base set and subsets  S of the base set such that  z is in the closure of  ( S  u.  { y } ) but not in the closure of  S,  y is in the closure of  ( S  u.  { z } ) (Definition 3.1.9 in [FaureFrolicher] p. 57 to 58.) This theorem allows us to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  A. s  e.  ~P  X A. y  e.  X  A. z  e.  ( ( N `  ( s  u.  { y }
 ) )  \  ( N `  s ) ) y  e.  ( N `
  ( s  u. 
 { z } )
 ) )   &    |-  ( ph  ->  S 
 C_  X )   &    |-  ( ph  ->  Y  e.  X )   &    |-  ( ph  ->  Z  e.  ( N `  ( S  u.  { Y }
 ) ) )   &    |-  ( ph  ->  -.  Z  e.  ( N `  S ) )   =>    |-  ( ph  ->  Y  e.  ( N `  ( S  u.  { Z }
 ) ) )
 
1-May-2017mrissmrid 13491 In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  T  C_  S )   =>    |-  ( ph  ->  T  e.  I )
 
1-May-2017mrissmrcd 13490 In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd 13477, and so are equal by mrieqv2d 13489.) (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S 
 C_  ( N `  T ) )   &    |-  ( ph  ->  T  C_  S )   &    |-  ( ph  ->  S  e.  I )   =>    |-  ( ph  ->  S  =  T )
 
1-May-2017mrieqv2d 13489 In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( S  e.  I  <->  A. s ( s 
 C.  S  ->  ( N `  s )  C.  ( N `  S ) ) ) )
 
1-May-2017mrieqvd 13488 In a Moore system, a set is independent if and only if, for all elements of the set, the closure of the set with the element removed is unequal to the closure of the original set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( S  e.  I  <->  A. x  e.  S  ( N `  ( S 
 \  { x }
 ) )  =/=  ( N `  S ) ) )
 
1-May-2017ismri2dad 13487 Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A  e.  (Moore `  X ) )   &    |-  ( ph  ->  S  e.  I )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  -.  Y  e.  ( N `  ( S  \  { Y }
 ) ) )
 
1-May-2017mrissd 13486 An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A  e.  (Moore `  X ) )   &    |-  ( ph  ->  S  e.  I )   =>    |-  ( ph  ->  S 
 C_  X )
 
1-May-2017mriss 13485 An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017.)
 |-  I  =  (mrInd `  A )   =>    |-  ( ( A  e.  (Moore `  X )  /\  S  e.  I )  ->  S  C_  X )
 
1-May-2017ismri2dd 13484 Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A  e.  (Moore `  X ) )   &    |-  ( ph  ->  S 
 C_  X )   &    |-  ( ph  ->  A. x  e.  S  -.  x  e.  ( N `  ( S  \  { x } ) ) )   =>    |-  ( ph  ->  S  e.  I )
 
1-May-2017ismri2d 13483 Criterion for a subset of the base set in a Moore system to be independent. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   &    |-  ( ph  ->  A  e.  (Moore `  X ) )   &    |-  ( ph  ->  S 
 C_  X )   =>    |-  ( ph  ->  ( S  e.  I  <->  A. x  e.  S  -.  x  e.  ( N `  ( S  \  { x } ) ) ) )
 
1-May-2017ismri2 13482 Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017.)
 |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   =>    |-  ( ( A  e.  (Moore `  X )  /\  S  C_  X )  ->  ( S  e.  I  <->  A. x  e.  S  -.  x  e.  ( N `  ( S  \  { x } ) ) ) )
 
1-May-2017ismri 13481 Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017.)
 |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   =>    |-  ( A  e.  (Moore `  X )  ->  ( S  e.  I  <->  ( S  C_  X  /\  A. x  e.  S  -.  x  e.  ( N `  ( S  \  { x }
 ) ) ) ) )
 
1-May-2017mrisval 13480 Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.)
 |-  N  =  (mrCls `  A )   &    |-  I  =  (mrInd `  A )   =>    |-  ( A  e.  (Moore `  X )  ->  I  =  { s  e.  ~P X  |  A. x  e.  s  -.  x  e.  ( N `  (
 s  \  { x } ) ) }
 )
 
1-May-2017mrieqvlemd 13479 In a Moore system, if  Y is a member of  S,  ( S 
\  { Y }
) and  S have the same closure if and only if  Y is in the closure of  ( S  \  { Y } ). Used in the proof of mrieqvd 13488 and mrieqv2d 13489. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  S 
 C_  X )   &    |-  ( ph  ->  Y  e.  S )   =>    |-  ( ph  ->  ( Y  e.  ( N `  ( S  \  { Y } ) )  <->  ( N `  ( S  \  { Y } ) )  =  ( N `  S ) ) )
 
1-May-2017mressmrcd 13477 In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  S 
 C_  ( N `  T ) )   &    |-  ( ph  ->  T  C_  S )   =>    |-  ( ph  ->  ( N `  S )  =  ( N `  T ) )
 
1-May-2017mrcidmd 13476 Moore closure is idempotent. Deduction form of mrcidm 13469. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  U 
 C_  X )   =>    |-  ( ph  ->  ( N `  ( N `
  U ) )  =  ( N `  U ) )
 
1-May-2017mrcssidd 13475 A set is contained in its Moore closure. Deduction form of mrcssid 13467. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  U 
 C_  X )   =>    |-  ( ph  ->  U 
 C_  ( N `  U ) )
 
1-May-2017mrcssd 13474 Moore closure preserves subset ordering. Deduction form of mrcss 13466. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   &    |-  ( ph  ->  U 
 C_  V )   &    |-  ( ph  ->  V  C_  X )   =>    |-  ( ph  ->  ( N `  U )  C_  ( N `  V ) )
 
1-May-2017mrcssvd 13473 The Moore closure of a set is a subset of the base. Deduction form of mrcssv 13464. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  (Moore `  X )
 )   &    |-  N  =  (mrCls `  A )   =>    |-  ( ph  ->  ( N `  B )  C_  X )
 
1-May-2017df-mri 13438 In a Moore system, a set is independent if no element of the set is in the closure of the set with the element removed (Section 0.6 in [Gratzer] p. 27; Definition 4.1.1 in [FaureFrolicher] p. 83.) mrInd is a class function which takes a Moore system to its set of independent sets. (Contributed by David Moews, 1-May-2017.)
 |- mrInd  =  ( c  e.  U. ran Moore 
 |->  { s  e.  ~P U. c  |  A. x  e.  s  -.  x  e.  ( (mrCls `  c
 ) `  ( s  \  { x } )
 ) } )
 
1-May-2017df-mrc 13437 Define the Moore closure of a generating set, which is the smallest closed set containing all generating elements. Definition of Moore closure in [Schechter] p. 79. This generalizes topological closure (mrccls 16764) and linear span (mrclsp 15694).

A Moore closure operation  N is (1) extensive, i.e.,  x  C_  ( N `  x ) for all subsets  x of the base set (mrcssid 13467), (2) isotone, i.e.,  x  C_  y implies that  ( N `
 x )  C_  ( N `  y ) for all subsets  x and  y of the base set (mrcss 13466), and (3) idempotent, i.e.,  ( N `  ( N `  x )
)  =  ( N `
 x ) for all subsets  x of the base set (mrcidm 13469.) Operators satisfying these three properties are in bijective correspondence with Moore collections, so these properties may be used to give an alternate characterization of a Moore collection by providing a closure operation  N on the set of subsets of a given base set which satisfies (1), (2), and (3); the closed sets can be recovered as those sets which equal their closures (Section 4.5 in [Schechter] p. 82.) (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by David Moews, 1-May-2017.)

 |- mrCls  =  ( c  e.  U. ran Moore 
 |->  ( x  e.  ~P U. c  |->  |^| { s  e.  c  |  x  C_  s } ) )
 
1-May-2017df-mre 13436 Define a Moore collection, which is a family of subsets of a base set which preserve arbitrary intersection. Elements of a Moore collection are termed closed; Moore collections generalize the notion of closedness from topologies (cldmre 16763) and vector spaces (lssmre 15671) to the most general setting in which such concepts make sense. Definition of Moore collection of sets in [Schechter] p. 78. A Moore collection may also be called a closure system (Section 0.6 in [Gratzer] p. 23.) The name Moore collection is after Eliakim Hastings Moore, who discussed these systems in Part I of [Moore] p. 53 to 76.

See ismre 13440, mresspw 13442, mre1cl 13444 and mreintcl 13445 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 13450); as such the disjoint union of all Moore collections is sometimes considered as  U. ran Moore, justified by mreunirn 13451. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.)

 |- Moore  =  ( x  e.  _V  |->  { c  e.  ~P ~P x  |  ( x  e.  c  /\  A. s  e.  ~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) }
 )
 
1-May-2017unirnfdomd 8143 The union of the range of a function from a infinite set into the class of finite sets is dominated by its domain. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  F : T --> Fin )   &    |-  ( ph  ->  -.  T  e.  Fin )   &    |-  ( ph  ->  T  e.  V )   =>    |-  ( ph  ->  U. ran  F  ~<_  T )
 
1-May-2017infinf 8142 Equivalence between two infiniteness criteria for sets. (Contributed by David Moews, 1-May-2017.)
 |-  ( A  e.  B  ->  ( -.  A  e.  Fin  <->  om  ~<_  A ) )
 
1-May-2017cardidd 8125 Any set is equinumerous to its cardinal number. Deduction form of cardid 8123. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  B )   =>    |-  ( ph  ->  ( card `  A )  ~~  A )
 
1-May-2017cardidg 8124 Any set is equinumerous to its cardinal number. Closed theorem form of cardid 8123. (Contributed by David Moews, 1-May-2017.)
 |-  ( A  e.  B  ->  ( card `  A )  ~~  A )
 
1-May-2017unirnffid 7101 The union of the range of a function from a finite set into the class of finite sets is finite. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  F : T --> Fin )   &    |-  ( ph  ->  T  e.  Fin )   =>    |-  ( ph  ->  U.
 ran  F  e.  Fin )
 
1-May-2017ensymd 6866 Symmetry of equinumerosity. Deduction form of ensym 6864. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  ~~  B )   =>    |-  ( ph  ->  B  ~~  A )
 
1-May-2017elfvexd 5476 If a function value is nonempty, its argument is a set. Deduction form of elfvex 5475. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  ( B `  C ) )   =>    |-  ( ph  ->  C  e.  _V )
 
1-May-2017ordelinel 4449 The intersection of two ordinal classes is an element of a third if and only if either one of them is. (Contributed by David Moews, 1-May-2017.)
 |-  ( ( Ord  A  /\  Ord  B  /\  Ord  C )  ->  ( ( A  i^i  B )  e.  C  <->  ( A  e.  C  \/  B  e.  C ) ) )
 
1-May-2017ordtri2or3 4448 A consequence of total ordering for ordinal classes. Similar to ordtri2or2 4447. (Contributed by David Moews, 1-May-2017.)
 |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  =  ( A  i^i  B )  \/  B  =  ( A  i^i  B ) ) )
 
1-May-2017ssexd 4121 A subclass of a set is a set. Deduction form of ssexg 4120. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  B  e.  C )   &    |-  ( ph  ->  A 
 C_  B )   =>    |-  ( ph  ->  A  e.  _V )
 
1-May-2017unissd 3811 Subclass relationship for subclass union. Deduction form of uniss 3808. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   =>    |-  ( ph  ->  U. A  C_ 
 U. B )
 
1-May-2017unissi 3810 Subclass relationship for subclass union. Inference form of uniss 3808. (Contributed by David Moews, 1-May-2017.)
 |-  A  C_  B   =>    |- 
 U. A  C_  U. B
 
1-May-2017difsnpss 3718  ( B  \  { A } ) is a proper subclass of  B if and only if  A is a member of  B. (Contributed by David Moews, 1-May-2017.)
 |-  ( A  e.  B  <->  ( B  \  { A } )  C.  B )
 
1-May-2017difsneq 3717  ( B  \  { A } ) equals  B if and only if 
A is not a member of  B. Generalization of difsn 3715. (Contributed by David Moews, 1-May-2017.)
 |-  ( -.  A  e.  B 
 <->  ( B  \  { A } )  =  B )
 
1-May-2017neldifsnd 3712  A is not in  ( B 
\  { A }
). Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  -.  A  e.  ( B  \  { A } ) )
 
1-May-2017neldifsn 3711  A is not in  ( B 
\  { A }
). (Contributed by David Moews, 1-May-2017.)
 |- 
 -.  A  e.  ( B  \  { A }
 )
 
1-May-2017elpwid 3594 An element of a power class is a subclass. Deduction form of elpwi 3593. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  ~P B )   =>    |-  ( ph  ->  A 
 C_  B )
 
1-May-2017ssnelpssd 3479 Subclass inclusion with one element of the superclass missing is proper subclass inclusion. Deduction form of ssnelpss 3478. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   &    |-  ( ph  ->  C  e.  B )   &    |-  ( ph  ->  -.  C  e.  A )   =>    |-  ( ph  ->  A  C.  B )
 
1-May-2017dfss5 3335 Another definition of subclasshood. Similar to df-ss 3127, dfss 3128, and dfss1 3334. (Contributed by David Moews, 1-May-2017.)
 |-  ( A  C_  B  <->  A  =  ( B  i^i  A ) )
 
1-May-2017unssbd 3314 If  ( A  u.  B ) is contained in  C, so is  B. One-way deduction form of unss 3310. Partial converse of unssd 3312. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  ( A  u.  B )  C_  C )   =>    |-  ( ph  ->  B  C_  C )
 
1-May-2017unssad 3313 If  ( A  u.  B ) is contained in  C, so is  A. One-way deduction form of unss 3310. Partial converse of unssd 3312. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  ( A  u.  B )  C_  C )   =>    |-  ( ph  ->  A  C_  C )
 
1-May-2017ssdif2d 3276 If  A is contained in  B and  C is contained in  D, then  ( A  \  D ) is contained in  ( B  \  C ). Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   &    |-  ( ph  ->  C 
 C_  D )   =>    |-  ( ph  ->  ( A  \  D ) 
 C_  ( B  \  C ) )
 
1-May-2017ssdifssd 3275 If  A is contained in  B, then  ( A 
\  C ) is also contained in  B. Deduction form of ssdifss 3268. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   =>    |-  ( ph  ->  ( A  \  C )  C_  B )
 
1-May-2017sscond 3274 If  A is contained in  B, then  ( C 
\  B ) is contained in  ( C  \  A ). Deduction form of sscon 3271. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   =>    |-  ( ph  ->  ( C  \  B )  C_  ( C  \  A ) )
 
1-May-2017ssdifd 3273 If  A is contained in  B, then  ( A 
\  C ) is contained in  ( B  \  C ). Deduction form of ssdif 3272. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   =>    |-  ( ph  ->  ( A  \  C )  C_  ( B  \  C ) )
 
1-May-2017difss2d 3267 If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3266. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  ( B  \  C ) )   =>    |-  ( ph  ->  A  C_  B )
 
1-May-2017difss2 3266 If a class is contained in a difference, it is contained in the minuend. (Contributed by David Moews, 1-May-2017.)
 |-  ( A  C_  ( B  \  C )  ->  A  C_  B )
 
1-May-2017difssd 3265 A difference of two classes is contained in the minuend. Deduction form of difss 3264. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  ( A  \  B )  C_  A )
 
1-May-2017psssstrd 3246 Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr 3243. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C.  B )   &    |-  ( ph  ->  B 
 C_  C )   =>    |-  ( ph  ->  A 
 C.  C )
 
1-May-2017sspsstrd 3245 Transitivity involving subclass and proper subclass inclusion. Deduction form of sspsstr 3242. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   &    |-  ( ph  ->  B 
 C.  C )   =>    |-  ( ph  ->  A 
 C.  C )
 
1-May-2017psstrd 3244 Proper subclass inclusion is transitive. Deduction form of psstr 3241. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C.  B )   &    |-  ( ph  ->  B 
 C.  C )   =>    |-  ( ph  ->  A 
 C.  C )
 
1-May-2017pssned 3235 Proper subclasses are unequal. Deduction form of pssne 3233. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C.  B )   =>    |-  ( ph  ->  A  =/=  B )
 
1-May-2017ssneldd 3144 If an element is not in a class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   &    |-  ( ph  ->  -.  C  e.  B )   =>    |-  ( ph  ->  -.  C  e.  A )
 
1-May-2017ssneld 3143 If a class is not in another class, it is also not in a subclass of that class. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  C_  B )   =>    |-  ( ph  ->  ( -.  C  e.  B  ->  -.  C  e.  A ) )
 
1-May-2017eldifbd 3126 If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3123. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  ( B  \  C ) )   =>    |-  ( ph  ->  -.  A  e.  C )
 
1-May-2017eldifad 3125 If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3123. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  ( B  \  C ) )   =>    |-  ( ph  ->  A  e.  B )
 
1-May-2017eldifd 3124 If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3123. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  -.  A  e.  C )   =>    |-  ( ph  ->  A  e.  ( B  \  C ) )
 
1-May-2017cbvrexv2 3109 Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
 |-  ( x  =  y 
 ->  ( ps  <->  ch ) )   &    |-  ( x  =  y  ->  A  =  B )   =>    |-  ( E. x  e.  A  ps  <->  E. y  e.  B  ch )
 
1-May-2017cbvralv2 3108 Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. (Contributed by David Moews, 1-May-2017.)
 |-  ( x  =  y 
 ->  ( ps  <->  ch ) )   &    |-  ( x  =  y  ->  A  =  B )   =>    |-  ( A. x  e.  A  ps  <->  A. y  e.  B  ch )
 
1-May-2017cla4dv 2834 Rule of specialization, using implicit substitution. Analogous to rcla4dv 2855. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ( ph  /\  x  =  A ) 
 ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  (
 A. x ps  ->  ch ) )
 
1-May-2017cbvrexdva 2740 Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ( ph  /\  x  =  y )  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E. x  e.  A  ps 
 <-> 
 E. y  e.  A  ch ) )
 
1-May-2017cbvraldva 2739 Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ( ph  /\  x  =  y )  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  (
 A. x  e.  A  ps 
 <-> 
 A. y  e.  A  ch ) )
 
1-May-2017cbvrexdva2 2738 Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ( ph  /\  x  =  y )  ->  ( ps 
 <->  ch ) )   &    |-  (
 ( ph  /\  x  =  y )  ->  A  =  B )   =>    |-  ( ph  ->  ( E. x  e.  A  ps 
 <-> 
 E. y  e.  B  ch ) )
 
1-May-2017cbvraldva2 2737 Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ( ph  /\  x  =  y )  ->  ( ps 
 <->  ch ) )   &    |-  (
 ( ph  /\  x  =  y )  ->  A  =  B )   =>    |-  ( ph  ->  ( A. x  e.  A  ps 
 <-> 
 A. y  e.  B  ch ) )
 
1-May-2017rexeqbii 2547 Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
 |-  A  =  B   &    |-  ( ps 
 <->  ch )   =>    |-  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
 
1-May-2017raleqbii 2546 Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
 |-  A  =  B   &    |-  ( ps 
 <->  ch )   =>    |-  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
 
1-May-2017neleqtrrd 2352 If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  -.  C  e.  B )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  -.  C  e.  A )
 
1-May-2017neleqtrd 2351 If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  -.  C  e.  A )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  -.  C  e.  B )
 
1-May-2017eqneltrrd 2350 If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  -.  A  e.  C )   =>    |-  ( ph  ->  -.  B  e.  C )
 
1-May-2017eqneltrd 2349 If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  -.  B  e.  C )   =>    |-  ( ph  ->  -.  A  e.  C )
 
1-May-2017cbvexdva 2055 Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ( ph  /\  x  =  y )  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E. x ps  <->  E. y ch )
 )
 
1-May-2017cbvaldva 2054 Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ( ph  /\  x  =  y )  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  (
 A. x ps  <->  A. y ch )
 )
 
28-Apr-2017ballotlemsel1i 23018 The range  ( 1 ... ( I `  C
) ) is invariant under  ( S `  C ). (Contributed by Thierry Arnoux, 28-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( S `  C ) `  J )  e.  ( 1 ... ( I `  C ) ) )
 
28-Apr-2017ballotlemsgt1 23016  S maps values less than  ( I `  C ) to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  J  <  ( I `  C ) )  -> 
 1  <  ( ( S `  C ) `  J ) )
 
27-Apr-2017ballotlemfrceq 23034 Value of  F for a reverse counting  ( R `  C ). (Contributed by Thierry Arnoux, 27-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( F `  C ) `  (
 ( ( S `  C ) `  J )  -  1 ) )  =  -u ( ( F `
  ( R `  C ) ) `  J ) )
 
26-Apr-2017ballotlemgun 23030 A property of the defined  .^ operator (Contributed by Thierry Arnoux, 26-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   &    |-  ( ph  ->  U  e.  Fin )   &    |-  ( ph  ->  V  e.  Fin )   &    |-  ( ph  ->  W  e.  Fin )   &    |-  ( ph  ->  ( V  i^i  W )  =  (/) )   =>    |-  ( ph  ->  ( U  .^  ( V  u.  W ) )  =  ( ( U  .^  V )  +  ( U  .^  W ) ) )
 
25-Apr-2017ballotlemfrcn0 23035 Value of  F for a reversed counting  ( R `  C ), before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  J  <  ( I `  C ) )  ->  ( ( F `  ( R `  C ) ) `  J )  =/=  0 )
 
24-Apr-2017funimass4f 22989 Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.)
 |-  F/_ x A   &    |-  F/_ x B   &    |-  F/_ x F   =>    |-  ( ( Fun 
 F  /\  A  C_  dom  F )  ->  ( ( F
 " A )  C_  B 
 <-> 
 A. x  e.  A  ( F `  x )  e.  B ) )
 
24-Apr-2017dfimafnf 22988 Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.)
 |-  F/_ x A   &    |-  F/_ x F   =>    |-  ( ( Fun  F  /\  A  C_  dom  F ) 
 ->  ( F " A )  =  { y  |  E. x  e.  A  y  =  ( F `  x ) } )
 
23-Apr-2017ax9dgenK 28158 Degenerate case of ax-9 1684. Uses only Tarski's FOL axiom schemes (see description for equidK 28136). (Contributed by NM, 23-Apr-2017.)
 |-  -.  A. x  -.  x  =  x
 
23-Apr-2017f1o3d 22984 Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.)
 |-  ( ph  ->  F  =  ( x  e.  A  |->  C ) )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  B )   &    |-  ( ( ph  /\  y  e.  B )  ->  D  e.  A )   &    |-  ( ( ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  ( x  =  D  <->  y  =  C ) )   =>    |-  ( ph  ->  ( F : A -1-1-onto-> B  /\  `' F  =  ( y  e.  B  |->  D ) ) )
 
21-Apr-2017ballotlemfrci 23033 Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( ( F `  ( R `  C ) ) `  ( I `
  C ) )  =  0 )
 
21-Apr-2017ballotlemfrc 23032 Express the value of  ( F `  ( R `  C )
) in terms of the newly defined  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( F `  ( R `  C ) ) `  J )  =  ( C  .^  ( ( ( S `
  C ) `  J ) ... ( I `  C ) ) ) )
 
21-Apr-2017ballotlemfg 23031 Express the value of  ( F `  C
) in terms of  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 0 ... ( M  +  N ) ) ) 
 ->  ( ( F `  C ) `  J )  =  ( C  .^  ( 1 ... J ) ) )
 
21-Apr-2017ballotlemgval 23029 Expand the value of  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( U  e.  Fin  /\  V  e.  Fin )  ->  ( U  .^  V )  =  ( ( # `
  ( V  i^i  U ) )  -  ( # `
  ( V  \  U ) ) ) )
 
21-Apr-2017ballotlemscr 23024 The image of  ( R `  C ) by  ( S `  C ) (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( ( S `  C ) " ( R `  C ) )  =  C )
 
20-Apr-2017stowei 27134 This theorem proves the Stone-Weierstrass theorem for real valued functions: let  J be a compact topology on  T, and  C be the set of real continuous functions on  T. Assume that  A is a subalgebra of  C (closed under addition and multiplication of functions) containing constant functions and discriminating points (if  r and  t are distinct points in  T, then there exists a function  h in  A such that h(r) is distinct from h(t) ). Then, for any continuous function 
F and for any positive real  E, there exists a function  f in the subalgebra  A, such that  f approximates  F up to  E ( E represents the usual ε value). As a classical example, given any a,b reals, the closed interval  T  =  [
a ,  b ] could be taken, along with the subalgebra  A of real polynomials on  T, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on  [ a ,  b ]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 27133: often times it will be better to use stoweid 27133 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  K  =  ( topGen `  ran  (,) )   &    |-  J  e.  Comp   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  A  C_  C   &    |-  ( ( f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( x  e.  RR  ->  ( t  e.  T  |->  x )  e.  A )   &    |-  ( ( r  e.  T  /\  t  e.  T  /\  r  =/=  t )  ->  E. h  e.  A  ( h `  r )  =/=  ( h `  t ) )   &    |-  F  e.  C   &    |-  E  e.  RR+   =>    |-  E. f  e.  A  A. t  e.  T  ( abs `  (
 ( f `  t
 )  -  ( F `
  t ) ) )  <  E
 
20-Apr-2017stoweid 27133 This theorem proves the Stone-Weierstrass theorem for real valued functions: let  J be a compact topology on  T, and  C be the set of real continuous functions on  T. Assume that  A is a subalgebra of  C (closed under addition and multiplication of functions) containing constant functions and discriminating points (if  r and  t are distinct points in  T, then there exists a function  h in  A such that h(r) is distinct from h(t) ). Then, for any continuous function 
F and for any positive real  E, there exists a function  f in the subalgebra  A, such that  f approximates  F up to  E ( E represents the usual ε value). As a classical example, given any a,b reals, the closed interval  T  =  [
a ,  b ] could be taken, along with the subalgebra  A of real polynomials on  T, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on  [ a ,  b ]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  x  e.  RR )  ->  (
 t  e.  T  |->  x )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. h  e.  A  ( h `  r )  =/=  ( h `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  E  e.  RR+ )   =>    |-  ( ph  ->  E. f  e.  A  A. t  e.  T  ( abs `  (
 ( f `  t
 )  -  ( F `
  t ) ) )  <  E )
 
20-Apr-2017stoweidlem62 27132 This theorem proves the Stone Weierstrass theorem for the non trivial case in which T is nonempty. The proof follows [BrosowskiDeutsh] p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ f ph   &    |-  F/ t ph   &    |-  H  =  ( t  e.  T  |->  ( ( F `  t )  -  sup ( ran  F ,  RR ,  `'  <  ) ) )   &    |-  K  =  ( topGen `  ran  (,) )   &    |-  T  =  U. J   &    |-  ( ph  ->  J  e.  Comp )   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  x  e.  RR )  ->  (
 t  e.  T  |->  x )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  T  =/=  (/) )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   =>    |-  ( ph  ->  E. f  e.  A  A. t  e.  T  ( abs `  ( ( f `
  t )  -  ( F `  t ) ) )  <  E )
 
20-Apr-2017stoweidlem61 27131 This lemma proves that there exists a function  g as in the proof in [BrosowskiDeutsh] p. 92:  g is in the subalgebra, and for all  t in  T, abs( f(t) - g(t) ) < 2*ε. Here  F is used to represent f in the paper, and  E is used to represent ε. For this lemma there's the further assumption that the function  F to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  T  =  U. J   &    |-  ( ph  ->  T  =/=  (/) )   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  x  e.  RR )  ->  (
 t  e.  T  |->  x )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  A. t  e.  T  0  <_  ( F `  t ) )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   =>    |-  ( ph  ->  E. g  e.  A  A. t  e.  T  ( abs `  ( ( g `
  t )  -  ( F `  t ) ) )  <  (
 2  x.  E ) )
 
20-Apr-2017stoweidlem60 27130 This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all  t in  T, there is a  j such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here  F is used to represent f in the paper, and  E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  D  =  ( j  e.  ( 0 ... n )  |->  { t  e.  T  |  ( F `  t
 )  <_  ( (
 j  -  ( 1 
 /  3 ) )  x.  E ) }
 )   &    |-  B  =  ( j  e.  ( 0 ... n )  |->  { t  e.  T  |  ( ( j  +  ( 1 
 /  3 ) )  x.  E )  <_  ( F `  t ) } )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  ( ph  ->  T  =/=  (/) )   &    |-  ( ph  ->  A 
 C_  C )   &    |-  (
 ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  y  e.  RR )  ->  (
 t  e.  T  |->  y )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  A. t  e.  T  0  <_  ( F `  t ) )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   =>    |-  ( ph  ->  E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  (
 4  /  3 )
 )  x.  E )  <  ( F `  t )  /\  ( F `
  t )  <_  ( ( j  -  ( 1  /  3
 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
 3 ) )  x.  E )  /\  (
 ( j  -  (
 4  /  3 )
 )  x.  E )  <  ( g `  t ) ) ) )
 
20-Apr-2017stoweidlem59 27129 This lemma proves that there exists a function  x as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < ε / n on Aj (meaning A in the paper), xj > 1 - \epslon / n on Bj. Here  D is used to represent A in the paper (because A is used for the subalgebra of functions),  E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  D  =  ( j  e.  ( 0 ... N )  |->  { t  e.  T  |  ( F `  t
 )  <_  ( (
 j  -  ( 1 
 /  3 ) )  x.  E ) }
 )   &    |-  B  =  ( j  e.  ( 0 ...
 N )  |->  { t  e.  T  |  ( ( j  +  ( 1 
 /  3 ) )  x.  E )  <_  ( F `  t ) } )   &    |-  Y  =  {
 y  e.  A  |  A. t  e.  T  ( 0  <_  (
 y `  t )  /\  ( y `  t
 )  <_  1 ) }   &    |-  H  =  ( j  e.  ( 0 ...
 N )  |->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `
  t )  < 
 ( E  /  N )  /\  A. t  e.  ( B `  j
 ) ( 1  -  ( E  /  N ) )  <  ( y `
  t ) ) } )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  ( ph  ->  A 
 C_  C )   &    |-  (
 ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  y  e.  RR )  ->  (
 t  e.  T  |->  y )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  E. x ( x : ( 0
 ... N ) --> A  /\  A. j  e.  ( 0
 ... N ) (
 A. t  e.  T  ( 0  <_  (
 ( x `  j
 ) `  t )  /\  ( ( x `  j ) `  t
 )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j
 ) `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `  j
 ) ( 1  -  ( E  /  N ) )  <  ( ( x `  j ) `
  t ) ) ) )
 
20-Apr-2017stoweidlem58 27128 This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t D   &    |-  F/_ t U   &    |-  F/ t ph   &    |-  K  =  ( topGen `  ran  (,) )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  J  e.  Comp
 )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  a  e.  RR )  ->  (
 t  e.  T  |->  a )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  B  e.  ( Clsd `  J ) )   &    |-  ( ph  ->  D  e.  ( Clsd `  J )
 )   &    |-  ( ph  ->  ( B  i^i  D )  =  (/) )   &    |-  U  =  ( T  \  B )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   =>    |-  ( ph  ->  E. x  e.  A  (
 A. t  e.  T  ( 0  <_  ( x `  t )  /\  ( x `  t ) 
 <_  1 )  /\  A. t  e.  D  ( x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E )  <  ( x `
  t ) ) )
 
20-Apr-2017stoweidlem57 27127 There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t D   &    |-  F/_ t U   &    |-  F/ t ph   &    |-  Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  ( h `  t )  /\  ( h `  t ) 
 <_  1 ) }   &    |-  V  =  { w  e.  J  |  A. e  e.  RR+  E. h  e.  A  (
 A. t  e.  T  ( 0  <_  ( h `  t )  /\  ( h `  t ) 
 <_  1 )  /\  A. t  e.  w  ( h `  t )  < 
 e  /\  A. t  e.  ( T  \  U ) ( 1  -  e )  <  ( h `
  t ) ) }   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  U  =  ( T  \  B )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  ( ph  ->  A 
 C_  C )   &    |-  (
 ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  a  e.  RR )  ->  (
 t  e.  T  |->  a )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  B  e.  ( Clsd `  J ) )   &    |-  ( ph  ->  D  e.  ( Clsd `  J )
 )   &    |-  ( ph  ->  ( B  i^i  D )  =  (/) )   &    |-  ( ph  ->  D  =/=  (/) )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   =>    |-  ( ph  ->  E. x  e.  A  (
 A. t  e.  T  ( 0  <_  ( x `  t )  /\  ( x `  t ) 
 <_  1 )  /\  A. t  e.  D  ( x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E )  <  ( x `
  t ) ) )
 
20-Apr-2017stoweidlem56 27126 This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here  Z is used to represent t0 in the paper,  v is used to represent  V in the paper, and  e is used to represent ε (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t U   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  y  e.  RR )  ->  (
 t  e.  T  |->  y )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  U  e.  J )   &    |-  ( ph  ->  Z  e.  U )   =>    |-  ( ph  ->  E. v  e.  J  ( ( Z  e.  v  /\  v  C_  U )  /\  A. e  e.  RR+  E. x  e.  A  ( A. t  e.  T  ( 0  <_  ( x `  t ) 
 /\  ( x `  t )  <_  1 ) 
 /\  A. t  e.  v  ( x `  t )  <  e  /\  A. t  e.  ( T  \  U ) ( 1  -  e )  < 
 ( x `  t
 ) ) ) )
 
20-Apr-2017stoweidlem55 27125 This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Here Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t U   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  x  e.  RR )  ->  (
 t  e.  T  |->  x )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  U  e.  J )   &    |-  ( ph  ->  Z  e.  U )   &    |-  Q  =  { h  e.  A  |  ( ( h `  Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  ( h `  t ) 
 <_  1 ) ) }   &    |-  W  =  { w  e.  J  |  E. h  e.  Q  w  =  { t  e.  T  |  0  < 
 ( h `  t
 ) } }   =>    |-  ( ph  ->  E. p  e.  A  (
 A. t  e.  T  ( 0  <_  ( p `  t )  /\  ( p `  t ) 
 <_  1 )  /\  ( p `  Z )  =  0  /\  A. t  e.  ( T  \  U ) 0  <  ( p `  t ) ) )
 
20-Apr-2017stoweidlem54 27124 There exists a function  x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here  D is used to represent  A in the paper, because here  A is used for the subalgebra of functions.  E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/ i ph   &    |-  F/ t ph   &    |-  F/ y ph   &    |-  F/ w ph   &    |-  T  =  U. J   &    |-  Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  ( h `  t )  /\  ( h `  t ) 
 <_  1 ) }   &    |-  P  =  ( f  e.  Y ,  g  e.  Y  |->  ( t  e.  T  |->  ( ( f `  t )  x.  (
 g `  t )
 ) ) )   &    |-  F  =  ( t  e.  T  |->  ( i  e.  (
 1 ... M )  |->  ( ( y `  i
 ) `  t )
 ) )   &    |-  Z  =  ( t  e.  T  |->  ( 
 seq  1 (  x. 
 ,  ( F `  t ) ) `  M ) )   &    |-  V  =  { w  e.  J  |  A. e  e.  RR+  E. h  e.  A  (
 A. t  e.  T  ( 0  <_  ( h `  t )  /\  ( h `  t ) 
 <_  1 )  /\  A. t  e.  w  ( h `  t )  < 
 e  /\  A. t  e.  ( T  \  U ) ( 1  -  e )  <  ( h `
  t ) ) }   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  x.  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A )  ->  f : T --> RR )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  W : ( 1 ...
 M ) --> V )   &    |-  ( ph  ->  B  C_  T )   &    |-  ( ph  ->  D  C_ 
 U. ran  W )   &    |-  ( ph  ->  D  C_  T )   &    |-  ( ph  ->  E. y
 ( y : ( 1 ... M ) --> Y  /\  A. i  e.  ( 1 ... M ) ( A. t  e.  ( W `  i
 ) ( ( y `
  i ) `  t )  <  ( E 
 /  M )  /\  A. t  e.  B  ( 1  -  ( E 
 /  M ) )  <  ( ( y `
  i ) `  t ) ) ) )   &    |-  ( ph  ->  T  e.  _V )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  /  3
 ) )   =>    |-  ( ph  ->  E. x  e.  A  ( A. t  e.  T  ( 0  <_  ( x `  t ) 
 /\  ( x `  t )  <_  1 ) 
 /\  A. t  e.  D  ( x `  t )  <  E  /\  A. t  e.  B  (
 1  -  E )  <  ( x `  t ) ) )
 
20-Apr-2017stoweidlem53 27123 This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t U   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  Q  =  { h  e.  A  |  ( ( h `  Z )  =  0  /\  A. t  e.  T  ( 0  <_  ( h `  t )  /\  ( h `  t ) 
 <_  1 ) ) }   &    |-  W  =  { w  e.  J  |  E. h  e.  Q  w  =  { t  e.  T  |  0  < 
 ( h `  t
 ) } }   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  J  e.  Comp
 )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  x  e.  RR )  ->  (
 t  e.  T  |->  x )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  U  e.  J )   &    |-  ( ph  ->  ( T  \  U )  =/=  (/) )   &    |-  ( ph  ->  Z  e.  U )   =>    |-  ( ph  ->  E. p  e.  A  (
 A. t  e.  T  ( 0  <_  ( p `  t )  /\  ( p `  t ) 
 <_  1 )  /\  ( p `  Z )  =  0  /\  A. t  e.  ( T  \  U ) 0  <  ( p `  t ) ) )
 
20-Apr-2017stoweidlem52 27122 There exists a neighborood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t U   &    |- 
 F/ t ph   &    |-  F/_ t P   &    |-  K  =  ( topGen `  ran  (,) )   &    |-  V  =  { t  e.  T  |  ( P `  t
 )  <  ( D  /  2 ) }   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph