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 ceddb01, also available here: set.mm (30MB) or set.mm.bz2 (compressed, 8MB).

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

Recent news items    (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!).

(17-Feb-2017) Alan Sare updated his completeusersproof that enhances mmj2 for certain kinds of proofs.

(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 2-Mar-2017 at 3:12 AM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 10-Jul-16 )
DateLabelDescription
Theorem
 
28-Feb-2017chordthm 19878 The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA  x. PB and PC  x. PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to  pi. The result is proven by using chordthmlem5 19877 twice to show that PA  x. PB and PC  x. PD both equal BQ2  - PQ2. This is similar to the proof of the theorem given in Euclid's Elements, where it is Proposition III.35. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  P  e.  CC )   &    |-  ( ph  ->  A  =/=  P )   &    |-  ( ph  ->  B  =/=  P )   &    |-  ( ph  ->  C  =/=  P )   &    |-  ( ph  ->  D  =/=  P )   &    |-  ( ph  ->  ( ( A  -  P ) F ( B  -  P ) )  =  pi )   &    |-  ( ph  ->  ( ( C  -  P ) F ( D  -  P ) )  =  pi )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( C  -  Q ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( D  -  Q ) ) )   =>    |-  ( ph  ->  (
 ( abs `  ( P  -  A ) )  x.  ( abs `  ( P  -  B ) ) )  =  ( ( abs `  ( P  -  C ) )  x.  ( abs `  ( P  -  D ) ) ) )
 
28-Feb-2017chordthmlem5 19877 If P is on the segment AB and AQ = BQ, then PA  x. PB = BQ2  - PQ2. This follows from two uses of chordthmlem3 19875 to show that PQ2 = QM2  + PM2 and BQ2 = QM2  + BM2, so BQ2  - PQ2 = (QM2  + BM2)  - (QM2  + PM2) = BM2  - PM2, which equals PA  x. PB by chordthmlem4 19876. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  X  e.  ( 0 [,] 1
 ) )   &    |-  ( ph  ->  P  =  ( ( X  x.  A )  +  ( ( 1  -  X )  x.  B ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   =>    |-  ( ph  ->  (
 ( abs `  ( P  -  A ) )  x.  ( abs `  ( P  -  B ) ) )  =  ( ( ( abs `  ( B  -  Q ) ) ^ 2 )  -  ( ( abs `  ( P  -  Q ) ) ^ 2 ) ) )
 
28-Feb-2017chordthmlem4 19876 If P is on the segment AB and M is the midpoint of AB, then PA  x. PB = BM2  - PM2. If all lengths are reexpressed as fractions of AB, this reduces to the identity  X  x.  (
1  -  X )  =  ( 1  / 
2 )2  -  ( ( 1  /  2 )  -  X )2. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  X  e.  (
 0 [,] 1 ) )   &    |-  ( ph  ->  M  =  ( ( A  +  B )  /  2
 ) )   &    |-  ( ph  ->  P  =  ( ( X  x.  A )  +  ( ( 1  -  X )  x.  B ) ) )   =>    |-  ( ph  ->  ( ( abs `  ( P  -  A ) )  x.  ( abs `  ( P  -  B ) ) )  =  ( ( ( abs `  ( B  -  M ) ) ^ 2 )  -  ( ( abs `  ( P  -  M ) ) ^ 2 ) ) )
 
28-Feb-2017chordthmlem3 19875 If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then PQ2 = QM2  + PM2. This follows from chordthmlem2 19874 and the Pythagorean theorem (pythag 19859) in the case where P and Q are unequal to M. If either P or Q equals M, the result is trivial. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  M  =  ( ( A  +  B )  / 
 2 ) )   &    |-  ( ph  ->  P  =  ( ( X  x.  A )  +  ( (
 1  -  X )  x.  B ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   =>    |-  ( ph  ->  (
 ( abs `  ( P  -  Q ) ) ^
 2 )  =  ( ( ( abs `  ( Q  -  M ) ) ^ 2 )  +  ( ( abs `  ( P  -  M ) ) ^ 2 ) ) )
 
28-Feb-2017chordthmlem2 19874 If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then QMP is a right angle. This is proven by reduction to the special case chordthmlem 19873, where P = B, and using angrtmuld 19850 to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  M  =  ( ( A  +  B )  /  2 ) )   &    |-  ( ph  ->  P  =  ( ( X  x.  A )  +  (
 ( 1  -  X )  x.  B ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   &    |-  ( ph  ->  P  =/=  M )   &    |-  ( ph  ->  Q  =/=  M )   =>    |-  ( ph  ->  (
 ( Q  -  M ) F ( P  -  M ) )  e. 
 { ( pi  / 
 2 ) ,  -u ( pi  /  2 ) }
 )
 
28-Feb-2017chordthmlem 19873 If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 19866 to observe that, since AMQ and BMQ have equal sides, the angles QMB and QMA must be equal. Since they are supplementary, both must be right. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  M  =  ( ( A  +  B )  / 
 2 ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  Q  =/=  M )   =>    |-  ( ph  ->  (
 ( Q  -  M ) F ( B  -  M ) )  e. 
 { ( pi  / 
 2 ) ,  -u ( pi  /  2 ) }
 )
 
28-Feb-2017angpieqvd 19872 The angle ABC is  pi iff B is a nontrivial convex combination of A and C, i.e., iff B is in the interior of the segment AC. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  (
 ( ( A  -  B ) F ( C  -  B ) )  =  pi  <->  E. w  e.  (
 0 (,) 1 ) B  =  ( ( w  x.  A )  +  ( ( 1  -  w )  x.  C ) ) ) )
 
28-Feb-2017angpined 19871 If the angle at ABC is  pi, then A is not equal to C. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  (
 ( ( A  -  B ) F ( C  -  B ) )  =  pi  ->  A  =/=  C ) )
 
28-Feb-2017angpieqvdlem2 19870 Equivalence used in angpieqvd 19872. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  ( -u ( ( C  -  B )  /  ( A  -  B ) )  e.  RR+  <->  ( ( A  -  B ) F ( C  -  B ) )  =  pi ) )
 
28-Feb-2017angpieqvdlem 19869 Equivalence used in the proof of angpieqvd 19872. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  A  =/=  C )   =>    |-  ( ph  ->  (
 -u ( ( C  -  B )  /  ( A  -  B ) )  e.  RR+  <->  ( ( C  -  B )  /  ( C  -  A ) )  e.  (
 0 (,) 1 ) ) )
 
28-Feb-2017affineequiv2 19868 Equivalence between two ways of expressing  B as an affine combination of  A and  C. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   =>    |-  ( ph  ->  ( B  =  ( ( D  x.  A )  +  ( ( 1  -  D )  x.  C ) )  <->  ( B  -  A )  =  (
 ( 1  -  D )  x.  ( C  -  A ) ) ) )
 
28-Feb-2017affineequiv 19867 Equivalence between two ways of expressing  B as an affine combination of  A and  C. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   =>    |-  ( ph  ->  ( B  =  ( ( D  x.  A )  +  ( ( 1  -  D )  x.  C ) )  <->  ( C  -  B )  =  ( D  x.  ( C  -  A ) ) ) )
 
28-Feb-2017ssscongptld 19866 If two triangles have equal sides, one angle in one triangle has the same cosine as the corresponding angle in the other triangle. This is a partial form of the SSS congruence theorem.

This theorem is proven by using lawcos 19858 on both triangles to express one side in terms of the other two, and then equating these expressions and reducing this algebraically to get an equality of cosines of angles. (Contributed by David Moews, 28-Feb-2017.)

 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  E  e.  CC )   &    |-  ( ph  ->  G  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  B  =/=  C )   &    |-  ( ph  ->  D  =/=  E )   &    |-  ( ph  ->  E  =/=  G )   &    |-  ( ph  ->  ( abs `  ( A  -  B ) )  =  ( abs `  ( D  -  E ) ) )   &    |-  ( ph  ->  ( abs `  ( B  -  C ) )  =  ( abs `  ( E  -  G ) ) )   &    |-  ( ph  ->  ( abs `  ( C  -  A ) )  =  ( abs `  ( G  -  D ) ) )   =>    |-  ( ph  ->  ( cos `  ( ( A  -  B ) F ( C  -  B ) ) )  =  ( cos `  (
 ( D  -  E ) F ( G  -  E ) ) ) )
 
28-Feb-2017angrtmuld 19850 Perpendicularity of two vectors does not change under rescaling the second. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Z  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   &    |-  ( ph  ->  Y  =/=  0
 )   &    |-  ( ph  ->  Z  =/=  0 )   &    |-  ( ph  ->  ( Z  /  Y )  e.  RR )   =>    |-  ( ph  ->  ( ( X F Y )  e.  { ( pi  /  2 ) ,  -u ( pi  /  2
 ) }  <->  ( X F Z )  e.  { ( pi  /  2 ) ,  -u ( pi  /  2
 ) } ) )
 
28-Feb-2017cosangneg2d 19849 The cosine of the angle between  X and  -u Y is the negative of that between  X and  Y. If A, B and C are collinear points, this implies that the cosines of DBA and DBC sum to zero, i.e., that DBA and DBC are supplementary. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0
 )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Y  =/=  0 )   =>    |-  ( ph  ->  ( cos `  ( X F -u Y ) )  =  -u ( cos `  ( X F Y ) ) )
 
28-Feb-2017angrteqvd 19848 Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0
 )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Y  =/=  0 )   =>    |-  ( ph  ->  ( ( X F Y )  e.  { ( pi  /  2 ) ,  -u ( pi  /  2
 ) }  <->  ( Re `  ( Y  /  X ) )  =  0 ) )
 
28-Feb-2017angcld 19847 The (signed) angle between two vectors is in  (
-u pi (,] pi ). Deduction form. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0
 )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Y  =/=  0 )   =>    |-  ( ph  ->  ( X F Y )  e.  ( -u pi (,] pi ) )
 
28-Feb-2017angvald 19846 The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval 19843. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0
 )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Y  =/=  0 )   =>    |-  ( ph  ->  ( X F Y )  =  ( Im `  ( log `  ( Y  /  X ) ) ) )
 
28-Feb-2017cosarg0d 19795 The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  ( ( cos `  ( Im `  ( log `  X ) ) )  =  0  <->  ( Re `  X )  =  0
 ) )
 
28-Feb-2017cosargd 19794 The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 19793. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  ( cos `  ( Im `  ( log `  X ) ) )  =  ( ( Re `  X )  /  ( abs `  X ) ) )
 
28-Feb-2017logimclad 19762 The imaginary part of the logarithm is in  ( -u pi (,] pi ). Alternate form of logimcld 19761. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  ( Im `  ( log `  X ) )  e.  ( -u pi (,] pi ) )
 
28-Feb-2017logimcld 19761 The imaginary part of the logarithm is in  ( -u pi (,] pi ). Deduction form of logimcl 19759. Compare logimclad 19762. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  (
 -u pi  <  ( Im `  ( log `  X ) )  /\  ( Im
 `  ( log `  X ) )  <_  pi ) )
 
28-Feb-2017logcld 19760 The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 19758. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  ( log `  X )  e.  CC )
 
28-Feb-2017negpitopissre 19734  ( -u pi (,] pi ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( -u pi (,] pi )  C_  RR
 
28-Feb-2017coseq0negpitopi 19703 Location of the zeroes of cosine in 
( -u pi (,] pi ). (Contributed by David Moews, 28-Feb-2017.)
 |-  ( A  e.  ( -u pi (,] pi ) 
 ->  ( ( cos `  A )  =  0  <->  A  e.  { ( pi  /  2 ) ,  -u ( pi  /  2
 ) } ) )
 
28-Feb-2017coseq00topi 19702 Location of the zeroes of cosine in 
( 0 [,] pi ). (Contributed by David Moews, 28-Feb-2017.)
 |-  ( A  e.  (
 0 [,] pi )  ->  ( ( cos `  A )  =  0  <->  A  =  ( pi  /  2 ) ) )
 
28-Feb-2017cosneghalfpi 19670 The cosine of  -u pi  /  2 is zero. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( cos `  -u ( pi  /  2 ) )  =  0
 
28-Feb-2017halfpire 19667  pi  /  2 is real. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( pi  /  2
 )  e.  RR
 
28-Feb-2017abs00bd 11653 If a complex number is zero, its absolute value is zero. Converse of abs00d 11805. One-way deduction form of abs00 11651. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  =  0 )   =>    |-  ( ph  ->  ( abs `  A )  =  0 )
 
28-Feb-2017abs00ad 11652 A complex number is zero iff its absolute value is zero. Deduction form of abs00 11651. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  (
 ( abs `  A )  =  0  <->  A  =  0
 ) )
 
28-Feb-2017sq0id 11075 If a number is zero, its square is zero. Deduction form of sq0i 11074. Converse of sqeq0d 11122. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  =  0 )   =>    |-  ( ph  ->  ( A ^ 2 )  =  0 )
 
28-Feb-2017unitssre 10659  ( 0 [,] 1 ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( 0 [,] 1
 )  C_  RR
 
28-Feb-2017xov1plusxeqvd 10658 A complex number  X is positive real iff  X  /  (
1  +  X ) is in  ( 0 (,) 1 ). Deduction form. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  -u 1 )   =>    |-  ( ph  ->  ( X  e.  RR+  <->  ( X  /  ( 1  +  X ) )  e.  (
 0 (,) 1 ) ) )
 
28-Feb-2017rehalfcli 9839 Half a real number is real. Inference form. (Contributed by David Moews, 28-Feb-2017.)
 |-  A  e.  RR   =>    |-  ( A  / 
 2 )  e.  RR
 
28-Feb-2017div2subd 9466 Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 9465. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  C  =/=  D )   =>    |-  ( ph  ->  ( ( A  -  B )  /  ( C  -  D ) )  =  ( ( B  -  A )  /  ( D  -  C ) ) )
 
28-Feb-2017diveq1bd 9464 If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 9334. Converse of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B  =/=  0 )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( A  /  B )  =  1 )
 
28-Feb-2017dmdcan2d 9446 Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  B  =/=  0 )   &    |-  ( ph  ->  C  =/=  0 )   =>    |-  ( ph  ->  ( ( A  /  B )  x.  ( B  /  C ) )  =  ( A  /  C ) )
 
28-Feb-2017divne1d 9427 If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B  =/=  0
 )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  ( A  /  B )  =/=  1 )
 
28-Feb-2017diveq0ad 9426 A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 9314. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B  =/=  0
 )   =>    |-  ( ph  ->  (
 ( A  /  B )  =  0  <->  A  =  0
 ) )
 
28-Feb-2017diveq1ad 9425 The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 9334. Generalization of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B  =/=  0
 )   =>    |-  ( ph  ->  (
 ( A  /  B )  =  1  <->  A  =  B ) )
 
28-Feb-2017eqnegad 9362 If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 9360. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A  =  -u A )   =>    |-  ( ph  ->  A  =  0 )
 
28-Feb-2017eqnegd 9361 A complex number equals its negative iff it is zero. Deduction form of eqneg 9360. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  ( A  =  -u A  <->  A  =  0
 ) )
 
28-Feb-2017mulne0bbd 9302 A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 9300 and consequence of mulne0bd 9299. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  ( A  x.  B )  =/=  0
 )   =>    |-  ( ph  ->  B  =/=  0 )
 
28-Feb-2017mulne0bad 9301 A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 9300 and consequence of mulne0bd 9299. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  ( A  x.  B )  =/=  0
 )   =>    |-  ( ph  ->  A  =/=  0 )
 
28-Feb-2017mulcan2ad 9284 Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcan2d 9282. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  C  =/=  0 )   &    |-  ( ph  ->  ( A  x.  C )  =  ( B  x.  C ) )   =>    |-  ( ph  ->  A  =  B )
 
28-Feb-2017mulcanad 9283 Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcand 9281. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  C  =/=  0 )   &    |-  ( ph  ->  ( C  x.  A )  =  ( C  x.  B ) )   =>    |-  ( ph  ->  A  =  B )
 
28-Feb-2017lt0ne0d 9218 Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  <  0 )   =>    |-  ( ph  ->  A  =/=  0 )
 
28-Feb-2017subeq0bd 9089 If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 9047. Converse of subeq0d 9045. Contrapositive of subne0ad 9048. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( A  -  B )  =  0 )
 
28-Feb-2017subneintr2d 9083 Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcan2d 9079. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  ( A  -  C )  =/=  ( B  -  C ) )
 
28-Feb-2017subcan2ad 9082 Cancellation law for subtraction. Deduction form of subcan2 8952. Generalization of subcan2d 9079. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   =>    |-  ( ph  ->  (
 ( A  -  C )  =  ( B  -  C )  <->  A  =  B ) )
 
28-Feb-2017subneintrd 9081 Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcand 9078. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  ( A  -  B )  =/=  ( A  -  C ) )
 
28-Feb-2017subcanad 9080 Cancellation law for subtraction. Deduction form of subcan 8982. Generalization of subcand 9078. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   =>    |-  ( ph  ->  (
 ( A  -  B )  =  ( A  -  C )  <->  B  =  C ) )
 
28-Feb-2017subne0ad 9048 If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d 9046. Contrapositive of subeq0bd 9089. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  ( A  -  B )  =/=  0
 )   =>    |-  ( ph  ->  A  =/=  B )
 
28-Feb-2017subeq0ad 9047 The difference of two complex numbers is zero iff they are equal. Deduction form of subeq0 8953. Generalization of subeq0d 9045. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( ( A  -  B )  =  0  <->  A  =  B ) )
 
28-Feb-2017negned 9034 If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 9049. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  -u A  =/=  -u B )
 
28-Feb-2017neg11ad 9033 The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 8978. Generalization of neg11d 9049. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  (
 -u A  =  -u B 
 <->  A  =  B ) )
 
28-Feb-2017negcon1ad 9032 Contraposition law for unary minus. One-way deduction form of negcon1 8979. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  -u A  =  B )   =>    |-  ( ph  ->  -u B  =  A )
 
28-Feb-2017negcon1d 9031 Contraposition law for unary minus. Deduction form of negcon1 8979. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  (
 -u A  =  B  <->  -u B  =  A )
 )
 
28-Feb-2017addneintr2d 8900 Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8898. Consequence of addcan2d 8896. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  ( A  +  C )  =/=  ( B  +  C ) )
 
28-Feb-2017addneintrd 8899 Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 8897. Consequence of addcand 8895. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  ( A  +  B )  =/=  ( A  +  C ) )
 
28-Feb-2017addcan2ad 8898 Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 8896. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  ( A  +  C )  =  ( B  +  C ) )   =>    |-  ( ph  ->  A  =  B )
 
28-Feb-2017addcanad 8897 Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 8895. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  ( A  +  B )  =  ( A  +  C ) )   =>    |-  ( ph  ->  B  =  C )
 
28-Feb-2017rexri 8764 A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
 |-  A  e.  RR   =>    |-  A  e.  RR*
 
28-Feb-2017pm2.21ddne 2486 A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  ps )
 
28-Feb-2017neneqad 2482 If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2428. One-way deduction form of df-ne 2414. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  -.  A  =  B )   =>    |-  ( ph  ->  A  =/=  B )
 
19-Feb-2017ex-natded9.20-2 20663 A more efficient proof of Theorem 9.20 of [Laboreo] p. 45. Compare with ex-natded9.20 20662. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.)
 |-  ( ph  ->  ( ps  /\  ( ch  \/  th ) ) )   =>    |-  ( ph  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )
 
19-Feb-2017ex-natded9.20 20662 Theorem 9.20 of [Laboreo] p. 43, translated line by line using the usual translation of natural deduction (ND) in the Metamath Proof Explorer (MPE) notation. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
11  ( ps  /\  ( ch  \/  th ) )  ( ph  ->  ( ps  /\  ( ch  \/  th ) ) ) Given $e
22  ps  ( ph  ->  ps )  /\EL 1 simpld 447 1
311  ( ch  \/  th )  ( ph  ->  ( ch  \/  th ) )  /\ER 1 simprd 451 1
44 ...|  ch  ( ( ph  /\  ch )  ->  ch ) ND hypothesis assumption simpr 449
55 ...  ( ps  /\  ch )  ( ( ph  /\  ch )  ->  ( ps  /\  ch ) )  /\I 2,4 jca 520 3,4
66 ...  ( ( ps  /\  ch )  \/  ( ps  /\  th ) )  ( ( ph  /\  ch )  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )  \/IR 5 orcd 383 5
78 ...|  th  ( ( ph  /\  th )  ->  th ) ND hypothesis assumption simpr 449
89 ...  ( ps  /\  th )  ( ( ph  /\  th )  ->  ( ps  /\  th ) )  /\I 2,7 jca 520 7,8
910 ...  ( ( ps  /\  ch )  \/  ( ps  /\  th ) )  ( ( ph  /\  th )  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )  \/IL 8 olcd 384 9
1012  ( ( ps  /\  ch )  \/  ( ps  /\  th ) )  ( ph  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )  \/E 3,6,9 mpjaodan 764 6,10,11

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps).

A much more efficient proof is ex-natded9.20-2 20663. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.)

 |-  ( ph  ->  ( ps  /\  ( ch  \/  th ) ) )   =>    |-  ( ph  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )
 
19-Feb-2017ex-natded5.5 20655 Theorem 5.5 of [Laboreo] p. 18, translated line by line using the usual translation of natural deduction (ND) in the Metamath Proof Explorer (MPE) notation. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
12;3  ( ps  ->  ch )  ( ph  ->  ( ps  ->  ch ) ) Given $e; adantr 453 to move it into the ND hypothesis
25  -.  ch  ( ph  ->  -.  ch ) Given $e; we'll use adantr 453 to move it into the ND hypothesis
31 ...|  ps  ( ph  ->  ps ) ND hypothesis assumption simpr 449
44 ...  ch  ( ( ph  /\  ps )  ->  ch )  ->E 1,3 mpd 16 1,3
56 ...  -.  ch  ( ( ph  /\  ps )  ->  -.  ch ) IT 2 adantr 453 5
67  -.  ps  ( ph  ->  -.  ps )  /\I 3,4,5 pm2.65da 562 4,6

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps).

A much more efficient proof is mtod 170; a proof without context is shown in mto 169.

(Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.)

 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( ph  ->  -.  ch )   =>    |-  ( ph  ->  -.  ps )
 
18-Feb-2017sbidd-misc 26878 An identity theorem for substitution. See sbid 1895. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
 |-  (
 ( ph  ->  [ x  /  x ] ps )  <->  (
 ph  ->  ps ) )
 
18-Feb-2017sbidd 26877 An identity theorem for substitution. See sbid 1895. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
 |-  ( ph  ->  [ x  /  x ] ps )   =>    |-  ( ph  ->  ps )
 
18-Feb-2017ex-natded9.26 20664 Theorem 9.26 of [Laboreo] p. 45, translated line by line using an interpretation of natural deduction in Metamath. This proof has some additional complications due to the fact that Metamath's existential elimination rule does not change bound variables, so we need to verify that  x is bound in the conclusion. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
13  E. x A. y ps ( x ,  y )  ( ph  ->  E. x A. y ps ) Given $e.
26 ...|  A. y ps ( x ,  y )  ( ( ph  /\  A. y ps )  ->  A. y ps ) ND hypothesis assumption simpr 449. Later statements will have this scope.
37;5,4 ...  ps ( x ,  y )  ( ( ph  /\  A. y ps )  ->  ps )  A.E 2,y a4sbcd 2934 ( A.E), 5,6. To use it we need a1i 12 and vex 2730. This could be immediately done with 19.21bi 1774, but we want to show the general approach for substitution.
412;8,9,10,11 ...  E. x ps ( x ,  y )  ( ( ph  /\  A. y ps )  ->  E. x ps )  E.I 3,a a4esbcd 3003 ( E.I), 11. To use it we need sylibr 205, which in turn requires sylib 190 and two uses of sbcid 2937. This could be more immediately done using 19.8a 1758, but we want to show the general approach for substitution.
513;1,2  E. x ps ( x ,  y )  ( ph  ->  E. x ps )  E.E 1,2,4,a exlimdd 1933 ( E.E), 1,2,3,12. We'll need supporting assertions that the variable is free (not bound), as provided in nfv 1629 and nfe1 1566 (MPE# 1,2)
614  A. y E. x ps ( x ,  y )  ( ph  ->  A. y E. x ps )  A.I 5 alrimiv 2012 ( A.I), 13

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps).

Note that in the original proof,  ps ( x ,  y ) has explicit parameters. In Metamath, these parameters are always implicit, and the parameters upon which a wff variable can depend are recorded in the "allowed substitution hints" below.

A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded9.26-2 20665.

(Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.)

 |-  ( ph  ->  E. x A. y ps )   =>    |-  ( ph  ->  A. y E. x ps )
 
18-Feb-2017sbcid 2937 An identity theorem for substitution. See sbid 1895. (Contributed by Mario Carneiro, 18-Feb-2017.)
 |-  ( [. x  /  x ]. ph  <->  ph )
 
13-Feb-201719.8ad 26876 If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1758. (Contributed by DAW, 13-Feb-2017.)
 |-  ( ph  ->  ps )   =>    |-  ( ph  ->  E. x ps )
 
9-Feb-2017resolution 26954 Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.)
 |-  (
 ( ( ph  /\  ps )  \/  ( -.  ph  /\ 
 ch ) )  ->  ( ps  \/  ch )
 )
 
9-Feb-2017ex-natded9.26-2 20665 A more efficient proof of Theorem 9.26 of [Laboreo] p. 45. Compare with ex-natded9.26 20664. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  E. x A. y ps )   =>    |-  ( ph  ->  A. y E. x ps )
 
9-Feb-2017ex-natded5.13-2 20661 A more efficient proof of Theorem 5.13 of [Laboreo] p. 20. Compare with ex-natded5.13 20660. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ( ps  \/  ch ) )   &    |-  ( ph  ->  ( ps  ->  th ) )   &    |-  ( ph  ->  ( -.  ta  ->  -.  ch ) )   =>    |-  ( ph  ->  ( th  \/  ta ) )
 
9-Feb-2017ex-natded5.13 20660 Theorem 5.13 of [Laboreo] p. 20, translated line by line using the interpretation of natural deduction in Metamath. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.13-2 20661. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
115  ( ps  \/  ch )  ( ph  ->  ( ps  \/  ch ) ) Given $e.
2;32  ( ps  ->  th )  ( ph  ->  ( ps  ->  th ) ) Given $e. adantr 453 to move it into the ND hypothesis
39  ( -.  ta  ->  -.  ch )  ( ph  ->  ( -.  ta  ->  -.  ch ) ) Given $e. ad2antrr 709 to move it into the ND sub-hypothesis
41 ...|  ps  ( ( ph  /\  ps )  ->  ps ) ND hypothesis assumption simpr 449
54 ...  th  ( ( ph  /\  ps )  ->  th )  ->E 2,4 mpd 16 1,3
65 ...  ( th  \/  ta )  ( ( ph  /\  ps )  ->  ( th  \/  ta ) )  \/I 5 orcd 383 4
76 ...|  ch  ( ( ph  /\  ch )  ->  ch ) ND hypothesis assumption simpr 449
88 ... ...|  -.  ta  ( ( ( ph  /\  ch )  /\  -.  ta )  ->  -.  ta ) (sub) ND hypothesis assumption simpr 449
911 ... ...  -.  ch  ( ( ( ph  /\  ch )  /\  -.  ta )  ->  -.  ch )  ->E 3,8 mpd 16 8,10
107 ... ...  ch  ( ( ( ph  /\  ch )  /\  -.  ta )  ->  ch ) IT 7 adantr 453 6
1112 ...  -.  -.  ta  ( ( ph  /\  ch )  ->  -.  -.  ta )  -.I 8,9,10 pm2.65da 562 7,11
1213 ...  ta  ( ( ph  /\  ch )  ->  ta )  -.E 11 notnotrd 107 12
1314 ...  ( th  \/  ta )  ( ( ph  /\  ch )  ->  ( th  \/  ta ) )  \/I 12 olcd 384 13
1416  ( th  \/  ta )  ( ph  ->  ( th  \/  ta ) )  \/E 1,6,13 mpjaodan 764 5,14,15

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  ( ps  \/  ch ) )   &    |-  ( ph  ->  ( ps  ->  th ) )   &    |-  ( ph  ->  ( -.  ta  ->  -.  ch ) )   =>    |-  ( ph  ->  ( th  \/  ta ) )
 
9-Feb-2017ex-natded5.8-2 20659 A more efficient proof of Theorem 5.8 of [Laboreo] p. 20. For a longer line-by-line translation, see ex-natded5.8 20658. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  (
 ( ps  /\  ch )  ->  -.  th )
 )   &    |-  ( ph  ->  ( ta  ->  th ) )   &    |-  ( ph  ->  ch )   &    |-  ( ph  ->  ta )   =>    |-  ( ph  ->  -.  ps )
 
9-Feb-2017ex-natded5.8 20658 Theorem 5.8 of [Laboreo] p. 20, translated line by line using the usual translation of natural deduction (ND) in the Metamath Proof Explorer (MPE) notation. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
110;11  ( ( ps  /\  ch )  ->  -.  th )  ( ph  ->  ( ( ps  /\  ch )  ->  -.  th ) ) Given $e; adantr 453 to move it into the ND hypothesis
23;4  ( ta  ->  th )  ( ph  ->  ( ta  ->  th ) ) Given $e; adantr 453 to move it into the ND hypothesis
37;8  ch  ( ph  ->  ch ) Given $e; adantr 453 to move it into the ND hypothesis
41;2  ta  ( ph  ->  ta ) Given $e. adantr 453 to move it into the ND hypothesis
56 ...|  ps  ( ( ph  /\  ps )  ->  ps ) ND Hypothesis/Assumption simpr 449. New ND hypothesis scope, each reference outside the scope must change antedent  ph to  ( ph  /\  ps ).
69 ...  ( ps  /\  ch )  ( ( ph  /\  ps )  ->  ( ps  /\  ch ) )  /\I 5,3 jca 520 ( /\I), 6,8 (adantr 453 to bring in scope)
75 ...  -.  th  ( ( ph  /\  ps )  ->  -.  th )  ->E 1,6 mpd 16 ( ->E), 2,4
812 ...  th  ( ( ph  /\  ps )  ->  th )  ->E 2,4 mpd 16 ( ->E), 9,11; note the contradiction with ND line 7 (MPE line 5)
913  -.  ps  ( ph  ->  -.  ps )  -.I 5,7,8 pm2.65da 562 ( -.I), 5,12; proof by contradiction. MPE step 6 (ND#5) does not need a reference here, because the assumption is embedded in the antecedents

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps).

A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.8-2 20659.

(Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  (
 ( ps  /\  ch )  ->  -.  th )
 )   &    |-  ( ph  ->  ( ta  ->  th ) )   &    |-  ( ph  ->  ch )   &    |-  ( ph  ->  ta )   =>    |-  ( ph  ->  -.  ps )
 
9-Feb-2017ex-natded5.7-2 20657 A more efficient proof of Theorem 5.7 of [Laboreo] p. 19. Compare with ex-natded5.7 20656. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ( ps  \/  ( ch  /\  th ) ) )   =>    |-  ( ph  ->  ( ps  \/  ch )
 )
 
9-Feb-2017ex-natded5.7 20656 Theorem 5.7 of [Laboreo] p. 19, translated line by line using the interpretation of natural deduction in Metamath. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.7-2 20657. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows:

#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
16  ( ps  \/  ( ch  /\  th ) )  ( ph  ->  ( ps  \/  ( ch  /\  th ) ) ) Given $e. No need for adantr 453 because we do not move this into an ND hypothesis
21 ...|  ps  ( ( ph  /\  ps )  ->  ps ) ND hypothesis assumption (new scope) simpr 449
32 ...  ( ps  \/  ch )  ( ( ph  /\  ps )  ->  ( ps  \/  ch ) )  \/IL 2 orcd 383, the MPE equivalent of  \/IL, 1
43 ...|  ( ch  /\  th )  ( ( ph  /\  ( ch  /\  th ) )  ->  ( ch  /\  th ) ) ND hypothesis assumption (new scope) simpr 449
54 ...  ch  ( ( ph  /\  ( ch  /\  th ) )  ->  ch )  /\EL 4 simpld 447, the MPE equivalent of  /\EL, 3
66 ...  ( ps  \/  ch )  ( ( ph  /\  ( ch  /\  th ) )  ->  ( ps  \/  ch ) )  \/IR 5 olcd 384, the MPE equivalent of  \/IR, 4
77  ( ps  \/  ch )  ( ph  ->  ( ps  \/  ch ) )  \/E 1,3,6 mpjaodan 764, the MPE equivalent of  \/E, 2,5,6

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  ( ps  \/  ( ch  /\  th ) ) )   =>    |-  ( ph  ->  ( ps  \/  ch )
 )
 
9-Feb-2017ex-natded5.3i 20654 The same as ex-natded5.3 20652 and ex-natded5.3-2 20653 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ps  ->  ch )   &    |-  ( ch  ->  th )   =>    |-  ( ps  ->  ( ch  /\  th ) )
 
9-Feb-2017ex-natded5.3-2 20653 A more efficient proof of Theorem 5.3 of [Laboreo] p. 16. Compare with ex-natded5.3 20652 and ex-natded5.3i 20654. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( ph  ->  ( ch  ->  th ) )   =>    |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
 
9-Feb-2017ex-natded5.3 20652 Theorem 5.3 of [Laboreo] p. 16, translated line by line using an interpretation of natural deduction in Metamath. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.3-2 20653. A proof without context is shown in ex-natded5.3i 20654. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows:

#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
12;3  ( ps  ->  ch )  ( ph  ->  ( ps  ->  ch ) ) Given $e; adantr 453 to move it into the ND hypothesis
25;6  ( ch  ->  th )  ( ph  ->  ( ch  ->  th ) ) Given $e; adantr 453 to move it into the ND hypothesis
31 ...|  ps  ( ( ph  /\  ps )  ->  ps ) ND hypothesis assumption simpr 449, to access the new assumption
44 ...  ch  ( ( ph  /\  ps )  ->  ch )  ->E 1,3 mpd 16, the MPE equivalent of  ->E, 1.3. adantr 453 was used to transform its dependency (we could also use imp 420 to get this directly from 1)
57 ...  th  ( ( ph  /\  ps )  ->  th )  ->E 2,4 mpd 16, the MPE equivalent of  ->E, 4,6. adantr 453 was used to transform its dependency
68 ...  ( ch  /\  th )  ( ( ph  /\  ps )  ->  ( ch  /\  th ) )  /\I 4,5 jca 520, the MPE equivalent of  /\I, 4,7
79  ( ps  ->  ( ch  /\  th ) )  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )  ->I 3,6 ex 425, the MPE equivalent of  ->I, 8

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( ph  ->  ( ch  ->  th ) )   =>    |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
 
9-Feb-2017ex-natded5.2i 20651 The same as ex-natded5.2 20649 and ex-natded5.2-2 20650 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ps  /\  ch )  ->  th )   &    |-  ( ch  ->  ps )   &    |-  ch   =>    |- 
 th
 
9-Feb-2017ex-natded5.2-2 20650 A more efficient proof of Theorem 5.2 of [Laboreo] p. 15. Compare with ex-natded5.2 20649 and ex-natded5.2i 20651. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  (
 ( ps  /\  ch )  ->  th ) )   &    |-  ( ph  ->  ( ch  ->  ps ) )   &    |-  ( ph  ->  ch )   =>    |-  ( ph  ->  th )
 
9-Feb-2017ex-natded5.2 20649 Theorem 5.2 of [Laboreo] p. 15, translated line by line using the interpretation of natural deduction in Metamath. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows:
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
15  ( ( ps  /\  ch )  ->  th )  ( ph  ->  ( ( ps  /\  ch )  ->  th ) ) Given $e.
22  ( ch  ->  ps )  ( ph  ->  ( ch  ->  ps ) ) Given $e.
31  ch  ( ph  ->  ch ) Given $e.
43  ps  ( ph  ->  ps )  ->E 2,3 mpd 16, the MPE equivalent of  ->E, 1,2
54  ( ps  /\  ch )  ( ph  ->  ( ps  /\  ch ) )  /\I 4,3 jca 520, the MPE equivalent of  /\I, 3,1
66  th  ( ph  ->  th )  ->E 1,5 mpd 16, the MPE equivalent of  ->E, 4,5

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps). A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.2-2 20650. A proof without context is shown in ex-natded5.2i 20651. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  (
 ( ps  /\  ch )  ->  th ) )   &    |-  ( ph  ->  ( ch  ->  ps ) )   &    |-  ( ph  ->  ch )   =>    |-  ( ph  ->  th )
 
9-Feb-2017a4esbcd 3003 form of a4sbc 2933. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  [. A  /  x ]. ps )   =>    |-  ( ph  ->  E. x ps )
 
9-Feb-2017a4sbcd 2934 Specialization: if a formula is true for all sets, it is true for any class which is a set. Similar to Theorem 6.11 of [Quine] p. 44. See also stdpc4 1896 and ra4sbc 2999. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  A. x ps )   =>    |-  ( ph  ->  [. A  /  x ]. ps )
 
9-Feb-2017sbceq1dd 2927 Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  [. A  /  x ]. ph )   =>    |-  ( ph  ->  [. B  /  x ]. ph )
 
9-Feb-2017sbceq1d 2926 Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( [. A  /  x ].
 ph 
 <-> 
 [. B  /  x ].
 ph ) )
 
9-Feb-2017exlimdd 1933 Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |- 
 F/ x ph   &    |-  F/ x ch   &    |-  ( ph  ->  E. x ps )   &    |-  (
 ( ph  /\  ps )  ->  ch )   =>    |-  ( ph  ->  ch )
 
9-Feb-2017pm2.21fal 1331 If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  F.  )
 
9-Feb-2017efald 1330 Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  -.  ps )  ->  F.  )   =>    |-  ( ph  ->  ps )
 
9-Feb-2017inegd 1329 Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  ps )  ->  F.  )   =>    |-  ( ph  ->  -. 
 ps )
 
9-Feb-2017dfnot 1328 Given falsum, we can define the negation of a wff  ph as the statement that a contradiction follows from assuming  ph. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( -.  ph  <->  ( ph  ->  F.  ) )
 
9-Feb-2017falimd 1326  F. implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  F.  )  ->  ps )
 
9-Feb-2017pm2.18da 432 Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  -.  ps )  ->  ps )   =>    |-  ( ph  ->  ps )
 
9-Feb-2017pm2.01da 431 Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  ps )  ->  -.  ps )   =>    |-  ( ph  ->  -.  ps )
 
9-Feb-2017exmidd 407 Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ( ps  \/  -.  ps )
 )
 
9-Feb-2017pm2.21dd 101 A contradiction implies anything. Deduction from pm2.21 102. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  ch )
 
8-Feb-2017notnotrd 107 Deduction converting double-negation into the original wff, aka the double negation rule. A translation of natural deduction rule  -.  -. -C,  _G |-  -.  -.  ps =>  _G |-  ps; see natded 4. THis is definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (which MPE uses), but not intuitionistic logic. (Contributed by DAW, 8-Feb-2017.)
 |-  ( ph  ->  -.  -.  ps )   =>    |-  ( ph  ->  ps )
 
5-Feb-2017eelT 27238 An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ( ph  ->  ps )   =>    |- 
 ps
 
4-Feb-20173impdirp1 27281 A deduction unionizing a non-unionized collection of virtual hypotheses. 3impdir 1243 is ~? uun3132 and is in set.mm. 3impdirp1 27281 is ~? uun3132p1. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ch  /\  ps )  /\  ( ph  /\ 
 ps ) )  ->  th )   =>    |-  ( ( ph  /\  ch  /\ 
 ps )  ->  th )
 
4-Feb-2017uun2221p2 27280 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ps  /\  ph )  /\  ph  /\  ph )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
4-Feb-2017uun2221p1 27279 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ( ps 
 /\  ph )  /\  ph )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
4-Feb-2017uun123p4 27277 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ch  /\  ps  /\  ph )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-2017uun123p3 27276 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ch  /\  ph )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-2017uun123p2 27275 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ch  /\  ph  /\  ps )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
4-Feb-2017uun123p1 27274 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  ch )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
4-Feb-2017uun123 27273 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ch  /\  ps )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-20173anidm12p2 27272 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  ph )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
4-Feb-20173anidm12p1 27271 A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1244 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uun111 27270 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ph  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunT12p5 27269 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  T.  )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12p4 27268 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps  /\  T.  )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12p3 27267 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  T.  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12p2 27266 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  ps )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12p1 27265 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ps  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12 27264 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  ps )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT11p2 27263 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ph  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunT11p1 27262 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunT11 27261 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunTT1p2 27260 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunTT1p1 27259 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunTT1 27258 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  T.  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uun2131p1 27257 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ch )  /\  ( ph  /\  ps ) )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-2017uun2131 27256 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps )  /\  ( ph  /\  ch ) )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-2017anabss7p1 27252 A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 797. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ps  /\  ph )  /\  ph )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
4-Feb-2017uun132p1 27251 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ps  /\  ch )  /\  ph )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
4-Feb-2017uun132 27250 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ( ps 
 /\  ch ) )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
4-Feb-2017uun121p1 27249 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps )  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uun121 27248 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ( ph  /\ 
 ps ) )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT1p1 27246 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017eelT0 27240 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ps   &    |-  ( ( ph  /\ 
 ps )  ->  ch )   =>    |-  ch
 
4-Feb-2017eel0cT 27239 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  ( ph  ->  ps )   =>    |-  (  T.  ->  ps )
 
4-Feb-2017eelTT 27236 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  (  T.  ->  ps )   &    |-  ( ( ph  /\ 
 ps )  ->  ch )   =>    |-  ch
 
4-Feb-2017eel00cT 27235 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  ps   &    |-  ( ( ph  /\ 
 ps )  ->  ch )   =>    |-  (  T.  ->  ch )
 
4-Feb-2017eel0T1 27180 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  (  T.  ->  ps )   &    |-  ( ch  ->  th )   &    |-  ( ( ph  /\ 
 ps  /\  th )  ->  ta )   =>    |-  ( ch  ->  ta )
 
4-Feb-2017eelT01 27179 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ps   &    |-  ( ch  ->  th )   &    |-  ( ( ph  /\ 
 ps  /\  th )  ->  ta )   =>    |-  ( ch  ->  ta )
 
4-Feb-2017eelTT1 27178 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  (  T.  ->  ps )   &    |-  ( ch  ->  th )   &    |-  ( ( ph  /\ 
 ps  /\  th )  ->  ta )   =>    |-  ( ch  ->  ta )
 
4-Feb-2017eelT12 27176 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ( ps  ->  ch )   &    |-  ( th  ->  ta )   &    |-  ( ( ph  /\ 
 ch  /\  ta )  ->  et )   =>    |-  ( ( ps  /\  th )  ->  et )
 
4-Feb-2017eelT11 27173 A elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ( ps  ->  ch )   &    |-  ( ps  ->  th )   &    |-  ( ( ph  /\ 
 ch  /\  th )  ->  ta )   =>    |-  ( ps  ->  ta )
 
4-Feb-2017eelTTT 27171 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  (  T.  ->  ps )   &    |-  (  T.  ->  ch )   &    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )   =>    |- 
 th
 
4-Feb-2017eelT00 27170 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ps   &    |-  ch   &    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )   =>    |- 
 th
 
4-Feb-2017eel0TT 27169 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  (  T.  ->  ps )   &    |-  (  T.  ->  ch )   &    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )   =>    |- 
 th
 
4-Feb-2017eel000cT 27168 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  ps   &    |-  ch   &    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )   =>    |-  (  T.  ->  th )
 
4-Feb-2017sbtT 27029 A substitution into a theorem remains true. sbt 1905 with the existence of no virtual hypotheses for the hypothesis expressed as the empty virtual hypothesis collection. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   =>    |- 
 [ y  /  x ] ph
 
4-Feb-2017natded 4 Here are typical natural deduction (ND) rules in the style of Gentzen and Jaśkowski, along with MPE translations of them. This also shows the recommended theorems when you find yourself needing these rules (the recommendations encourage a slightly different proof style that works more naturally with metamath). A decent list of the standard rules of natural deduction can be found beginning with definition /\I in [Pfenning] p. 18. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. Many more citations could be added.

NameNatural Deduction RuleTranslation RecommendationComments
IT  _G |-  ps =>  _G |-  ps idi 2 nothing Reiteration is always redundant in Metamath. Definition "new rule" in [Pfenning] p. 18, definition IT in [Laboreo] p. 10.
 /\I  _G |-  ps &  _G |-  ch =>  _G |-  ps  /\  ch jca 520 jca 520, pm3.2i 443 Definition  /\I in [Pfenning] p. 18, definition I /\m,n in [Laboreo] p. 10, and definition  /\I in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
 /\EL  _G |-  ps  /\  ch =>  _G |-  ps simpld 447 simpld 447, adantr 453 Definition  /\EL in [Pfenning] p. 18, definition E /\(1) in [Laboreo] p. 11, and definition  /\E in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
 /\ER  _G |-  ps  /\  ch =>  _G |-  ch simprd 451 simpr 449, adantl 454 Definition  /\ER in [Pfenning] p. 18, definition E /\(2) in [Laboreo] p. 11, and definition  /\E in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
 ->I  _G ,  ps |-  ch =>  _G |-  ps  ->  ch ex 425 ex 425 Definition  ->I in [Pfenning] p. 18, definition I=>m,n in [Laboreo] p. 11, and definition  ->I in [Indrzejczak] p. 33.
 ->E  _G |-  ps  ->  ch &  _G |-  ps =>  _G |-  ch mpd 16 ax-mp 10, mpd 16, mpdan 652, imp 420 Definition  ->E in [Pfenning] p. 18, definition E=>m,n in [Laboreo] p. 11, and definition  ->E in [Indrzejczak] p. 33.
 \/IL  _G |-  ps =>  _G |-  ps  \/  ch olcd 384 olc 375, olci 382, olcd 384 Definition  \/I in [Pfenning] p. 18, definition I \/n(1) in [Laboreo] p. 12
 \/IR  _G |-  ch =>  _G |-  ps  \/  ch orcd 383 orc 376, orci 381, orcd 383 Definition  \/IR in [Pfenning] p. 18, definition I \/n(2) in [Laboreo] p. 12.
 \/E  _G |-  ps  \/  ch &  _G ,  ps |-  th &  _G ,  ch |-  th =>  _G |-  th mpjaodan 764 mpjaodan 764, jaodan 763, jaod 371 Definition  \/E in [Pfenning] p. 18, definition E \/m,n,p in [Laboreo] p. 12.
 -.I  _G ,  ps |-  F. =>  _G |-  -.  ps inegd 1329 pm2.01d 163
 -.I  _G ,  ps |-  th &  _G |-  -.  th =>  _G |-  -.  ps mtand 643 mtand 643 definition I -.m,n,p in [Laboreo] p. 13.
 -.I  _G ,  ps |-  ch &  _G ,  ps |-  -.  ch =>  _G |-  -.  ps pm2.65da 562 pm2.65da 562 Contradiction.
 -.I  _G ,  ps |-  -.  ps =>  _G |-  -.  ps pm2.01da 431 pm2.01d 163, pm2.65da 562, pm2.65d 168 For an alternative falsum-free natural deduction ruleset
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  F. pm2.21fal 1331 pm2.21dd 101
 -.E  _G ,  -.  ps |-  F. =>  _G |-  ps pm2.21dd 101 definition  ->E in [Indrzejczak] p. 33.
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  th pm2.21dd 101 pm2.21dd 101, pm2.21d 100, pm2.21 102 For an alternative falsum-free natural deduction ruleset. Definition  -.E in [Pfenning] p. 18.
 T.I  _G |-  T. a1tru 1327 tru 1317, a1tru 1327, trud 1320 Definition  T.I in [Pfenning] p. 18.
 F.E  _G ,  F.  |-  th falimd 1326 falim 1325 Definition  F.E in [Pfenning] p. 18.
 A.I  _G |-  [ a  /  x ] ps =>  _G |-  A. x ps alrimiv 2012 alrimiv 2012, ralrimiva 2588 Definition  A.Ia in [Pfenning] p. 18, definition I A.n in [Laboreo] p. 32.
 A.E  _G |-  A. x ps =>  _G |-  [ t  /  x ] ps a4sbcd 2934 cla4v 2811, rcla4v 2817 Definition  A.E in [Pfenning] p. 18, definition E A.n,t in [Laboreo] p. 32.
 E.I  _G |-  [ t  /  x ] ps =>  _G |-  E. x ps a4esbcd 3003 cla4ev 2812, rcla4ev 2821 Definition  E.I in [Pfenning] p. 18, definition I E.n,t in [Laboreo] p. 32.
 E.E  _G |-  E. x ps &  _G ,  [ a  /  x ] ps |-  th =>  _G |-  th exlimddv 1934 exlimddv 1934, exlimdd 1933, exlimdv 1932, rexlimdva 2629 Definition  E.Ea,u in [Pfenning] p. 18, definition E E.m,n,p,a in [Laboreo] p. 32.
 F.C  _G ,  -.  ps |-  F. =>  _G |-  ps efald 1330 efald 1330 Proof by contradiction (classical logic), definition  F.C in [Pfenning] p. 17.
 F.C  _G ,  -.  ps |-  ps =>  _G |-  ps pm2.18da 432 pm2.18da 432, pm2.18d 105, pm2.18 104 For an alternative falsum-free natural deduction ruleset
 -.  -.C  _G |-  -.  -.  ps =>  _G |-  ps notnotrd 107 notnotrd 107, notnot2 106 Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E -.n in [Laboreo] p. 14.
EM  _G |-  ps  \/  -.  ps exmidd 407 exmid 406 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Laboreo] p. 14.
 =I  _G |-  A  =  A eqidd 2254 eqid 2253, eqidd 2254 Introduce equality, definition =I in [Pfenning] p. 127.
 =E  _G |-  A  =  B &  _G [. A  /  x ]. ps =>  _G |-  [. B  /  x ]. ps sbceq1dd 2927 sbceq1d 2926, equality theorems Eliminate equality, definition =E in [Pfenning] p. 127. (Both E1 and E2.)

Note that MPE uses classical logic, not intuitionist logic. As is conventional, the "I" rules are introduction rules, "E" rules are elimination rules, the "C" rules are conversion rules, and  _G represents the set of (current) hypotheses. We use wff variable names beginning with  ps to provide a closer representation of the Metamath equivalents (which typically use the antedent  ph to represent the context  _G).

Most of this information was developed by Mario Carneiro and posted on 3-Feb-2017. For more information, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer.

For annotated examples where some traditional ND rules are directly applied in MPE, see ex-natded5.2 20649, ex-natded5.3 20652, ex-natded5.5 20655, ex-natded5.7 20656, ex-natded5.8 20658, ex-natded5.13 20660, ex-natded9.20 20662, and ex-natded9.26 20664.

(Contributed by DAW, 4-Feb-2017.)

 |-  ph   =>    |-  ph
 
31-Jan-20172p2ne5 26953 Prove that  2  +  2  =/=  5. In George Orwell's "1984", Part One, Chapter Seven, the protagonist Winston notes that, "In the end the Party would announce that two and two made five, and you would have to believe it." http://www.sparknotes.com/lit/1984/section4.rhtml. More generally, the phrase  2  +  2  =  5 has come to represent an obviously false dogma one may be required to believe. See the Wikipedia article for more about this: https://en.wikipedia.org/wiki/2_%2B_2_%3D_5. Unsurprisingly, we can easily prove that this claim is false. (Contributed by David A. Wheeler, 31-Jan-2017.)
 |-  (
 2  +  2 )  =/=  5
 
31-Jan-20175m4e1 26952 Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.)
 |-  (
 5  -  4 )  =  1
 
30-Jan-2017yoniso 13903 If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from  C into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  (
 SetCat `  U )   &    |-  D  =  (CatCat `  V )   &    |-  B  =  ( Base `  D )   &    |-  I  =  (  Iso  `  D )   &    |-  Q  =  ( O FuncCat  S )   &    |-  E  =  ( Qs 
 ran  ( 1st `  Y ) )   &    |-  ( ph  ->  V  e.  X )   &    |-  ( ph  ->  C  e.  B )   &    |-  ( ph  ->  U  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  E  e.  B )   &    |-  ( ( ph  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) ) 
 ->  ( F `  ( x (  Hom  `  C ) y ) )  =  y )   =>    |-  ( ph  ->  Y  e.  ( C I E ) )
 
30-Jan-2017fullres2c 13657 Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
 |-  A  =  ( Base `  C )   &    |-  E  =  ( Ds  S )   &    |-  ( ph  ->  D  e.  Cat )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  F : A --> S )   =>    |-  ( ph  ->  ( F ( C Full  D ) G  <->  F ( C Full  E ) G ) )
 
30-Jan-2017fthres2c 13649 Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
 |-  A  =  ( Base `  C )   &    |-  E  =  ( Ds  S )   &    |-  ( ph  ->  D  e.  Cat )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  F : A --> S )   =>    |-  ( ph  ->  ( F ( C Faith  D ) G  <->  F ( C Faith  E ) G ) )
 
30-Jan-2017funcres2c 13619 Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
 |-  A  =  ( Base `  C )   &    |-  E  =  ( Ds  S )   &    |-  ( ph  ->  D  e.  Cat )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  F : A --> S )   =>    |-  ( ph  ->  ( F ( C  Func  D ) G  <->  F ( C  Func  E ) G ) )
 
29-Jan-2017yonffth 13902 The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category  C as a full subcategory of the category  Q of presheaves on  C. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  (
 SetCat `  U )   &    |-  Q  =  ( O FuncCat  S )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  U  e.  V )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   =>    |-  ( ph  ->  Y  e.  ( ( C Full  Q )  i^i  ( C Faith  Q ) ) )
 
29-Jan-2017yoneda 13901 The Yoneda Lemma. There is a natural isomorphism between the functors  Z and  E, where  Z ( F ,  X ) is the natural transformations from Yon ( X )  =  Hom  (  -  ,  X ) to  F, and  E ( F ,  X )  =  F ( X ) is the evaluation functor. Here we need two universes to state the claim: the smaller universe  U is used for forming the functor category  Q  =  C op  ->  SetCat ( U ), which itself does not (necessarily) live in  U but instead is an element of the larger universe  V. (If  U is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set  U  =  V in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   &    |-  I  =  (  Iso  `  R )   =>    |-  ( ph  ->  M  e.  ( Z I E ) )
 
29-Jan-2017yonffthlem 13900 Lemma for yonffth 13902. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   &    |-  I  =  (Inv `  R )   &    |-  N  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f ) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y ( 
 Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   =>    |-  ( ph  ->  Y  e.  ( ( C Full  Q )  i^i  ( C Faith  Q ) ) )
 
29-Jan-2017yonedainv 13899 The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   &    |-  I  =  (Inv `  R )   &    |-  N  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f ) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y ( 
 Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   =>    |-  ( ph  ->  M ( Z I E ) N )
 
29-Jan-2017yonedalem3b 13897 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  G  e.  ( O  Func  S ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  A  e.  ( F ( O Nat  S ) G ) )   &    |-  ( ph  ->  K  e.  ( P (  Hom  `  C ) X ) )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   =>    |-  ( ph  ->  ( ( G M P ) ( <. ( F ( 1st `  Z ) X ) ,  ( G ( 1st `  Z ) P ) >. (comp `  T ) ( G ( 1st `  E ) P ) ) ( A ( <. F ,  X >. ( 2nd `  Z ) <. G ,  P >. ) K ) )  =  ( ( A ( <. F ,  X >. ( 2nd `  E ) <. G ,  P >. ) K ) (
 <. ( F ( 1st `  Z ) X ) ,  ( F ( 1st `  E ) X ) >. (comp `  T ) ( G ( 1st `  E ) P ) ) ( F M X ) ) )
 
29-Jan-2017yonedalem22 13896 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  G  e.  ( O  Func  S ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  A  e.  ( F ( O Nat  S ) G ) )   &    |-  ( ph  ->  K  e.  ( P (  Hom  `  C ) X ) )   =>    |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z ) <. G ,  P >. ) K )  =  ( ( ( P ( 2nd `  Y ) X ) `  K ) ( <. ( ( 1st `  Y ) `  X ) ,  F >. ( 2nd `  H ) <. ( ( 1st `  Y ) `  P ) ,  G >. ) A ) )
 
29-Jan-2017yonedalem4c 13895 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  N  =  ( f  e.  ( O 
 Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
 ) `  x )  |->  ( y  e.  B  |->  ( g  e.  (
 y (  Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   &    |-  ( ph  ->  A  e.  ( ( 1st `  F ) `  X ) )   =>    |-  ( ph  ->  (
 ( F N X ) `  A )  e.  ( ( ( 1st `  Y ) `  X ) ( O Nat  S ) F ) )
 
29-Jan-2017yonedalem4b 13894 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  N  =  ( f  e.  ( O 
 Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
 ) `  x )  |->  ( y  e.  B  |->  ( g  e.  (
 y (  Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   &    |-  ( ph  ->  A  e.  ( ( 1st `  F ) `  X ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  G  e.  ( P (  Hom  `  C ) X ) )   =>    |-  ( ph  ->  ( ( ( ( F N X ) `  A ) `  P ) `  G )  =  ( ( ( X ( 2nd `  F ) P ) `  G ) `  A ) )
 
29-Jan-2017yonedalem4a 13893 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  N  =  ( f  e.  ( O 
 Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
 ) `  x )  |->  ( y  e.  B  |->  ( g  e.  (
 y (  Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   &    |-  ( ph  ->  A  e.  ( ( 1st `  F ) `  X ) )   =>    |-  ( ph  ->  (
 ( F N X ) `  A )  =  ( y  e.  B  |->  ( g  e.  (
 y (  Hom  `  C ) X )  |->  ( ( ( X ( 2nd `  F ) y ) `
  g ) `  A ) ) ) )
 
29-Jan-2017yonedalem3a 13892 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  M  =  ( f  e.  ( O 
 Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `  x ) `  (  .1.  `  x ) ) ) )   =>    |-  ( ph  ->  ( ( F M X )  =  ( a  e.  (
 ( ( 1st `  Y ) `  X ) ( O Nat  S ) F )  |->  ( ( a `
  X ) `  (  .1.  `  X )
 ) )  /\  ( F M X ) : ( F ( 1st `  Z ) X ) --> ( F ( 1st `  E ) X ) ) )
 
29-Jan-2017catciso 13783 A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  C  =  (CatCat `  U )   &    |-  B  =  ( Base `  C )   &    |-  R  =  (
 Base `  X )   &    |-  S  =  ( Base `  Y )   &    |-  ( ph  ->  U  e.  V )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   &    |-  I  =  (  Iso  `  C )   =>    |-  ( ph  ->  ( F  e.  ( X I Y )  <->  ( F  e.  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  /\  ( 1st `  F ) : R -1-1-onto-> S ) ) )
 
29-Jan-2017catcisolem 13782 Lemma for catciso 13783. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  C  =  (CatCat `  U )   &    |-  B  =  ( Base `  C )   &    |-  R  =  (
 Base `  X )   &    |-  S  =  ( Base `  Y )   &    |-  ( ph  ->  U  e.  V )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   &    |-  I  =  (Inv `  C )   &    |-  H  =  ( x  e.  S ,  y  e.  S  |->  `' ( ( `' F `  x ) G ( `' F `  y ) ) )   &    |-  ( ph  ->  F ( ( X Full  Y )  i^i  ( X Faith  Y ) ) G )   &    |-  ( ph  ->  F : R
 -1-1-onto-> S )   =>    |-  ( ph  ->  <. F ,  G >. ( X I Y ) <. `' F ,  H >. )
 
29-Jan-2017ffthf1o 13637 The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  B  =  ( Base `  C )   &    |-  H  =  ( 
 Hom  `  C )   &    |-  J  =  (  Hom  `  D )   &    |-  ( ph  ->  F ( ( C Full  D )  i^i  ( C Faith  D ) ) G )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   =>    |-  ( ph  ->  ( X G Y ) : ( X H Y ) -1-1-onto-> ( ( F `  X ) J ( F `  Y ) ) )
 
28-Jan-2017yonedalem3 13898 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   =>    |-  ( ph  ->  M  e.  ( Z ( ( Q  X.c  O ) Nat  T ) E ) )
 
28-Jan-2017yonedalem21 13891 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   =>    |-  ( ph  ->  ( F ( 1st `  Z ) X )  =  ( ( ( 1st `  Y ) `  X ) ( O Nat  S ) F ) )
 
28-Jan-2017yonedalem1 13890 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   =>    |-  ( ph  ->  ( Z  e.  ( ( Q  X.c  O )  Func  T ) 
 /\  E  e.  (
 ( Q  X.c  O )  Func  T ) ) )
 
28-Jan-2017funcsetcres2 13769 A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  C  =  ( SetCat `  U )   &    |-  D  =  (
 SetCat `  V )   &    |-  ( ph  ->  U  e.  W )   &    |-  ( ph  ->  V  C_  U )   =>    |-  ( ph  ->  ( E  Func  D )  C_  ( E  Func  C ) )
 
28-Jan-2017fuciso 13693 A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  Q  =  ( C FuncCat  D )   &    |-  B  =  (
 Base `  C )   &    |-  N  =  ( C Nat  D )   &    |-  ( ph  ->  F  e.  ( C  Func  D ) )   &    |-  ( ph  ->  G  e.  ( C  Func  D ) )   &    |-  I  =  ( 
 Iso  `  Q )   &    |-  J  =  (  Iso  `  D )   =>    |-  ( ph  ->  ( A  e.  ( F I G )  <->  ( A  e.  ( F N G ) 
 /\  A. x  e.  B  ( A `  x )  e.  ( ( ( 1st `  F ) `  x ) J ( ( 1st `  G ) `  x ) ) ) ) )
 
28-Jan-2017invfuc 13692 If  V (
x ) is an inverse to  U ( x ) for each  x, and  U is a natural transformation, then  V is also a natural transformation and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  Q  =  ( C FuncCat  D )   &    |-  B  =  (
 Base `  C )   &    |-  N  =  ( C Nat  D )   &    |-  ( ph  ->  F  e.  ( C  Func  D ) )   &    |-  ( ph  ->  G  e.  ( C  Func  D ) )   &    |-  I  =  (Inv `  Q )   &    |-  J  =  (Inv `  D )   &    |-  ( ph  ->  U  e.  ( F N G ) )   &    |-  (
 ( ph  /\  x  e.  B )  ->  ( U `  x ) ( ( ( 1st `  F ) `  x ) J ( ( 1st `  G ) `  x ) ) X )   =>    |-  ( ph  ->  U ( F I G ) ( x  e.  B  |->  X ) )
 
28-Jan-2017fucinv 13691 Two natural transformations are inverses of each other iff all the components are inverse. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  Q  =  ( C FuncCat  D )   &    |-  B  =  (
 Base `  C )   &    |-  N  =  ( C Nat  D )   &    |-  ( ph  ->  F  e.  ( C  Func  D ) )   &    |-  ( ph  ->  G  e.  ( C  Func  D ) )   &    |-  I  =  (Inv `  Q )   &    |-  J  =  (Inv `  D )   =>    |-  ( ph  ->  ( U ( F I G ) V  <->  ( U  e.  ( F N G ) 
 /\  V  e.  ( G N F )  /\  A. x  e.  B  ( U `  x ) ( ( ( 1st `  F ) `  x ) J ( ( 1st `  G ) `  x ) ) ( V `
  x ) ) ) )
 
28-Jan-2017fucsect 13690 Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  Q  =  ( C FuncCat  D )   &    |-  B  =  (
 Base `  C )   &    |-  N  =  ( C Nat  D )   &    |-  ( ph  ->  F  e.  ( C  Func  D ) )   &    |-  ( ph  ->  G  e.  ( C  Func  D ) )   &    |-  S  =  (Sect `  Q )   &    |-  T  =  (Sect `  D )   =>    |-  ( ph  ->  ( U ( F S G ) V  <->  ( U  e.  ( F N G ) 
 /\  V  e.  ( G N F )  /\  A. x  e.  B  ( U `  x ) ( ( ( 1st `  F ) `  x ) T ( ( 1st `  G ) `  x ) ) ( V `
  x ) ) ) )
 
28-Jan-2017coffth 13654 The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  ( ph  ->  F  e.  ( ( C Full  D )  i^i  ( C Faith  D ) ) )   &    |-  ( ph  ->  G  e.  (
 ( D Full  E )  i^i  ( D Faith  E ) ) )   =>    |-  ( ph  ->  ( G  o.func 
 F )  e.  (
 ( C Full  E )  i^i  ( C Faith  E ) ) )
 
28-Jan-2017cofth 13653 The composition of two faithful functors is faithful. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  ( ph  ->  F  e.  ( C Faith  D ) )   &    |-  ( ph  ->  G  e.  ( D Faith  E ) )   =>    |-  ( ph  ->  ( G  o.func 
 F )  e.  ( C Faith  E ) )
 
28-Jan-2017cofull 13652 The composition of two full functors is full. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  ( ph  ->  F  e.  ( C Full  D ) )   &    |-  ( ph  ->  G  e.  ( D Full  E ) )   =>    |-  ( ph  ->  ( G  o.func 
 F )  e.  ( C Full  E ) )
 
28-Jan-2017cofu2 13604 Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  B  =  ( Base `  C )   &    |-  ( ph  ->  F  e.  ( C  Func  D ) )   &    |-  ( ph  ->  G  e.  ( D  Func  E ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   &    |-  H  =  (  Hom  `  C )   &    |-  ( ph  ->  R  e.  ( X H Y ) )   =>    |-  ( ph  ->  ( ( X ( 2nd `  ( G  o.func  F )
 ) Y ) `  R )  =  (
 ( ( ( 1st `  F ) `  X ) ( 2nd `  G ) ( ( 1st `  F ) `  Y ) ) `  (
 ( X ( 2nd `  F ) Y ) `
  R ) ) )
 
28-Jan-2017cofu1 13602 Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  B  =  ( Base `  C )   &    |-  ( ph  ->  F  e.  ( C  Func  D ) )   &    |-  ( ph  ->  G  e.  ( D  Func  E ) )   &    |-  ( ph  ->  X  e.  B )   =>    |-  ( ph  ->  ( ( 1st `  ( G  o.func 
 F ) ) `  X )  =  (
 ( 1st `  G ) `  ( ( 1st `  F ) `  X ) ) )
 
28-Jan-2017idfu2 13596 Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.)
 |-  I  =  (idfunc `  C )   &    |-  B  =  ( Base `  C )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  H  =  (  Hom  `  C )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   &    |-  ( ph  ->  F  e.  ( X H Y ) )   =>    |-  ( ph  ->  ( ( X ( 2nd `  I
 ) Y ) `  F )  =  F )
 
27-Jan-2017ffthres2c 13658 Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.)
 |-  A  =  ( Base `  C )   &    |-  E  =  ( Ds  S )   &    |-  ( ph  ->  D  e.  Cat )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  F : A --> S )   =>    |-  ( ph  ->  ( F ( ( C Full 
 D )  i^i  ( C Faith  D ) ) G  <->  F ( ( C Full 
 E )  i^i  ( C Faith  E ) ) G ) )
 
27-Jan-2017ressffth 13656 The inclusion functor from a full subcategory is a full and faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
 |-  D  =  ( Cs  S )   &    |-  I  =  (idfunc `  D )   =>    |-  ( ( C  e.  Cat  /\  S  e.  V ) 
 ->  I  e.  (
 ( D Full  C )  i^i  ( D Faith  C ) ) )
 
27-Jan-2017rescfth 13655 The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
 |-  D  =  ( C  |`cat  J )   &    |-  I  =  (idfunc `  D )   =>    |-  ( J  e.  (Subcat `  C )  ->  I  e.  ( D Faith  C ) )
 
27-Jan-2017idffth 13651 The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.)
 |-  I  =  (idfunc `  C )   =>    |-  ( C  e.  Cat  ->  I  e.  ( ( C Full  C )  i^i  ( C Faith  C ) ) )
 
27-Jan-2017fthres2 13650 A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017.)
 |-  ( R  e.  (Subcat `  D )  ->  ( C Faith  ( D  |`cat  R )
 )  C_  ( C Faith  D ) )
 
27-Jan-2017fthres2b 13648 Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.)
 |-  A  =  ( Base `  C )   &    |-  H  =  ( 
 Hom  `  C )   &    |-  ( ph  ->  R  e.  (Subcat `  D ) )   &    |-  ( ph  ->  R  Fn  ( S  X.  S ) )   &    |-  ( ph  ->  F : A
 --> S )   &    |-  ( ( ph  /\  ( x  e.  A  /\  y  e.  A ) )  ->  ( x G y ) : Y --> ( ( F `
  x ) R ( F `  y
 ) ) )   =>    |-  ( ph  ->  ( F ( C Faith  D ) G  <->  F ( C Faith  ( D  |`cat  R ) ) G ) )
 
27-Jan-2017ffthiso 13647 A fully faithful functor reflects isomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.)
 |-  B  =  ( Base `  C )   &    |-  H  =  ( 
 Hom  `  C )   &    |-  ( ph  ->  F ( C Faith  D ) G )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   &    |-  ( ph  ->  R  e.  ( X H Y ) )   &    |-  ( ph  ->  F ( C Full  D ) G )   &    |-  I  =  (  Iso  `  C )   &    |-  J  =  ( 
 Iso  `  D )   =>    |-  ( ph  ->  ( R  e.  ( X I Y )  <-> 
 ( ( X G Y ) `  R )  e.  ( ( F `  X ) J ( F `  Y ) ) ) )
 
27-Jan-2017fthepi 13646 A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.)
 |-  B  =  ( Base `  C )   &    |-  H  =  ( 
 Hom  `  C )   &    |-  ( ph  ->  F ( C Faith  D ) G )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  Y  e.  B )   &    |-  ( ph  ->  R  e.  ( X H Y ) )   &    |-  E  =  (Epi `  C )   &    |-  P  =  (Epi `  D )   &    |-  ( ph  ->  ( ( X G Y ) `  R )  e.  ( ( F `  X ) P ( F `  Y )