Metamath Proof Explorer Most Recent Proofs |
||
Mirrors > Home > MPE Home > Th. List > Recent | Other > MM 100 |
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 | Hilbert Space Explorer | User Mathboxes |
Date | Label | Description | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Theorem | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthm 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 PB and PC 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 . The result is proven by using chordthmlem5 19877 twice to show that PA PB and PC PD both equal BQ^{2} PQ^{2}. 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem5 19877 | If P is on the segment AB and AQ = BQ, then PA PB = BQ^{2} PQ^{2}. This follows from two uses of chordthmlem3 19875 to show that PQ^{2} = QM^{2} PM^{2} and BQ^{2} = QM^{2} BM^{2}, so BQ^{2} PQ^{2} = (QM^{2} BM^{2}) (QM^{2} PM^{2}) = BM^{2} PM^{2}, which equals PA PB by chordthmlem4 19876. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem4 19876 | If P is on the segment AB and M is the midpoint of AB, then PA PB = BM^{2} PM^{2}. If all lengths are reexpressed as fractions of AB, this reduces to the identity ^{2} ^{2}. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem3 19875 | If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then PQ^{2} = QM^{2} PM^{2}. 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem2 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angpieqvd 19872 | The angle ABC is 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angpined 19871 | If the angle at ABC is , then A is not equal to C. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angpieqvdlem2 19870 | Equivalence used in angpieqvd 19872. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angpieqvdlem 19869 | Equivalence used in the proof of angpieqvd 19872. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | affineequiv2 19868 | Equivalence between two ways of expressing as an affine combination of and . (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | affineequiv 19867 | Equivalence between two ways of expressing as an affine combination of and . (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | ssscongptld 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angrtmuld 19850 | Perpendicularity of two vectors does not change under rescaling the second. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | cosangneg2d 19849 | The cosine of the angle between and is the negative of that between and . 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angrteqvd 19848 | Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angcld 19847 | The (signed) angle between two vectors is in . Deduction form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angvald 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | cosarg0d 19795 | The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | cosargd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | logimclad 19762 | The imaginary part of the logarithm is in . Alternate form of logimcld 19761. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | logimcld 19761 | The imaginary part of the logarithm is in . Deduction form of logimcl 19759. Compare logimclad 19762. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | logcld 19760 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 19758. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | negpitopissre 19734 | is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | coseq0negpitopi 19703 | Location of the zeroes of cosine in . (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | coseq00topi 19702 | Location of the zeroes of cosine in . (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | cosneghalfpi 19670 | The cosine of is zero. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | halfpire 19667 | is real. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | abs00bd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | abs00ad 11652 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 11651. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | sq0id 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | unitssre 10659 | is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | xov1plusxeqvd 10658 | A complex number is positive real iff is in . Deduction form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | rehalfcli 9839 | Half a real number is real. Inference form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | div2subd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | diveq1bd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | dmdcan2d 9446 | Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | divne1d 9427 | If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | diveq0ad 9426 | A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 9314. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | diveq1ad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | eqnegad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | eqnegd 9361 | A complex number equals its negative iff it is zero. Deduction form of eqneg 9360. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | mulne0bbd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | mulne0bad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | mulcan2ad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | mulcanad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | lt0ne0d 9218 | Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subeq0bd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subneintr2d 9083 | Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcan2d 9079. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subcan2ad 9082 | Cancellation law for subtraction. Deduction form of subcan2 8952. Generalization of subcan2d 9079. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subneintrd 9081 | Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcand 9078. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subcanad 9080 | Cancellation law for subtraction. Deduction form of subcan 8982. Generalization of subcand 9078. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subne0ad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subeq0ad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | negned 9034 | If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 9049. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | neg11ad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | negcon1ad 9032 | Contraposition law for unary minus. One-way deduction form of negcon1 8979. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | negcon1d 9031 | Contraposition law for unary minus. Deduction form of negcon1 8979. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | addneintr2d 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | addneintrd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | addcan2ad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | addcanad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | rexri 8764 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | pm2.21ddne 2486 | A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | neneqad 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Feb-2017 | ex-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):
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 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Feb-2017 | ex-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):
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 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
18-Feb-2017 | sbidd-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
18-Feb-2017 | sbidd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
18-Feb-2017 | ex-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 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):
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 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, 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
18-Feb-2017 | sbcid 2937 | An identity theorem for substitution. See sbid 1895. (Contributed by Mario Carneiro, 18-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
13-Feb-2017 | 19.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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | resolution 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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):
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 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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):
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 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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:
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 and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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:
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 and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-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:
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 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | a4esbcd 3003 | form of a4sbc 2933. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | a4sbcd 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | sbceq1dd 2927 | Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | sbceq1d 2926 | Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | exlimdd 1933 | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | pm2.21fal 1331 | If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | efald 1330 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | inegd 1329 | Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | dfnot 1328 | Given falsum, we can define the negation of a wff as the statement that a contradiction follows from assuming . (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | falimd 1326 | implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | pm2.18da 432 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | pm2.01da 431 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | exmidd 407 | Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | pm2.21dd 101 | A contradiction implies anything. Deduction from pm2.21 102. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
8-Feb-2017 | notnotrd 107 | Deduction converting double-negation into the original wff, aka the double negation rule. A translation of natural deduction rule -C, => ; 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
5-Feb-2017 | eelT 27238 | An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | 3impdirp1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun2221p2 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun2221p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123p4 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123p3 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123p2 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | 3anidm12p2 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | 3anidm12p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun111 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p5 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p4 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p3 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p2 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT11p2 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT11p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT11 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunTT1p2 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunTT1p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunTT1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun2131p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun2131 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | anabss7p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun132p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun132 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun121p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun121 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT1p1 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT0 27240 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel0cT 27239 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelTT 27236 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel00cT 27235 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel0T1 27180 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT01 27179 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelTT1 27178 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT12 27176 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT11 27173 | A elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelTTT 27171 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT00 27170 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel0TT 27169 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel000cT 27168 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | sbtT 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | natded 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.
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 represents the set of (current) hypotheses. We use wff variable names beginning with to provide a closer representation of the Metamath equivalents (which typically use the antedent to represent the context ). 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
31-Jan-2017 | 2p2ne5 26953 | Prove that . 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 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
31-Jan-2017 | 5m4e1 26952 | Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
30-Jan-2017 | yoniso 13903 | If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat CatCat FuncCat ↾_{s} _{f} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
30-Jan-2017 | fullres2c 13657 | Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
↾_{s} Full Full | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
30-Jan-2017 | fthres2c 13649 | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
↾_{s} Faith Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
30-Jan-2017 | funcres2c 13619 | Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
↾_{s} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonffth 13902 | The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category as a full subcategory of the category of presheaves on . (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat _{f} Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yoneda 13901 | The Yoneda Lemma. There is a natural isomorphism between the functors and , where is the natural transformations from Yon to , and is the evaluation functor. Here we need two universes to state the claim: the smaller universe is used for forming the functor category ^{op} , which itself does not (necessarily) live in but instead is an element of the larger universe . (If is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonffthlem 13900 | Lemma for yonffth 13902. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat Inv Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedainv 13899 | The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat Inv | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem3b 13897 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat Nat comp comp | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem22 13896 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem4c 13895 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem4b 13894 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem4a 13893 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem3a 13892 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | catciso 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
CatCat Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | catcisolem 13782 | Lemma for catciso 13783. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
CatCat Inv Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | ffthf1o 13637 | The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | yonedalem3 13898 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat _{c} Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | yonedalem21 13891 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | yonedalem1 13890 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} _{c} _{c} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | funcsetcres2 13769 | A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | fuciso 13693 | A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
FuncCat Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | invfuc 13692 | If is an inverse to for each , and is a natural transformation, then is also a natural transformation and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
FuncCat Nat Inv Inv | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | fucinv 13691 | Two natural transformations are inverses of each other iff all the components are inverse. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
FuncCat Nat Inv Inv | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | fucsect 13690 | Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
FuncCat Nat Sect Sect | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | coffth 13654 | The composition of two fully faithful functors is fully faithful. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Full Faith Full Faith _{func} Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | cofth 13653 | The composition of two faithful functors is faithful. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Faith Faith _{func} Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | cofull 13652 | The composition of two full functors is full. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Full Full _{func} Full | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | cofu2 13604 | Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
_{func} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | cofu1 13602 | Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
_{func} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Jan-2017 | idfu2 13596 | Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id_{func} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | ffthres2c 13658 | Condition for a fully faithful functor to also be a fully faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
↾_{s} Full Faith Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | ressffth 13656 | The inclusion functor from a full subcategory is a full and faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
↾_{s} id_{func} Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | rescfth 13655 | The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
_{cat} id_{func} Subcat Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | idffth 13651 | The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
id_{func} Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | fthres2 13650 | A functor into a restricted category is also a functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Subcat Faith _{cat} Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | fthres2b 13648 | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Subcat Faith Faith _{cat} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | ffthiso 13647 | A fully faithful functor reflects isomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Faith Full | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | fthepi 13646 | A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Faith Epi Epi | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
27-Jan-2017 | fthmon 13645 | A faithful functor reflects monomorphisms. (Contributed by Mario Carneiro, 27-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Faith Mono Mono |