P. 217 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Type

Label

Description

Statement

Theorem

constr3cycl 21601

Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.)

|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> ( F ( V Cycles E ) P /\ ( # ` F ) = 3 ) )

Theorem

constr3cyclp 21602

Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.)

|- F = { <. 0 , ( `' E ` { A , B } ) >. , <. 1 , ( `' E ` { B , C } ) >. , <. 2 , ( `' E ` { C , A } ) >. }   &    |- P = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , A >. } )   =>    |- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> ( F ( V Cycles E ) P /\ ( # ` F ) = 3 /\ ( P ` 0 ) = A ) )

Theorem

constr3cyclpe 21603*

If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.)

|- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E /\ { C , A } e. ran E ) ) -> E. f E. p ( f ( V Cycles E ) p /\ ( # ` f ) = 3 /\ ( p ` 0 ) = A ) )

Theorem

3v3e3cycl2 21604*

If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph. (Contributed by Alexander van der Vekens, 14-Nov-2017.)

|- ( V USGrph E -> ( E. a e. V E. b e. V E. c e. V ( { a , b } e. ran E /\ { b , c } e. ran E /\ { c , a } e. ran E ) -> E. f E. p ( f ( V Cycles E ) p /\ ( # ` f ) = 3 ) ) )

Theorem

3v3e3cycl 21605*

If and only if there is a 3-cycle in a graph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.)

|- ( V USGrph E -> ( E. f E. p ( f ( V Cycles E ) p /\ ( # ` f ) = 3 ) <-> E. a e. V E. b e. V E. c e. V ( { a , b } e. ran E /\ { b , c } e. ran E /\ { c , a } e. ran E ) ) )

Theorem

4cycl4v4e 21606*

If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)

|- ( ( Fun E /\ F ( V Cycles E ) P /\ ( # ` F ) = 4 ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( { a , b } e. ran E /\ { b , c } e. ran E ) /\ ( { c , d } e. ran E /\ { d , a } e. ran E ) ) )

Theorem

4cycl4dv 21607

In a simple graph, the vertices of a 4-cycle are mutually different. (Contributed by Alexander van der Vekens, 18-Nov-2017.)

|- ( ( V USGrph E /\ ( F e. Word dom E /\ Fun `' F /\ ( # ` F ) = 4 ) ) -> ( ( ( ( E ` ( F ` 0 ) ) = { A , B } /\ ( E ` ( F ` 1 ) ) = { B , C } ) /\ ( ( E ` ( F ` 2 ) ) = { C , D } /\ ( E ` ( F ` 3 ) ) = { D , A } ) ) -> ( ( ( { A , B } e. ran E /\ { B , C } e. ran E ) /\ ( { C , D } e. ran E /\ { D , A } e. ran E ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) ) )

Theorem

4cycl4dv4e 21608*

If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)

|- ( ( V USGrph E /\ F ( V Cycles E ) P /\ ( # ` F ) = 4 ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. ran E /\ { b , c } e. ran E ) /\ ( { c , d } e. ran E /\ { d , a } e. ran E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )

14.1.5.4  Connected graphs

Syntax

cconngra 21609

Extend class notation with connected graphs.

class ConnGrph

Definition

df-conngra 21610*

Define the class of all connected graphs. A graph (or, more generally, any pair representing a structure consisting of "vertices" and "edges") is called connected if there is a path between every pair of (distinct) vertices. The distinctness of the vertices is not necessary for the definition, because there is always a path (of length 0) from a vertex to itself, see 0pthonv 21534 and dfconngra1 21611. (Contributed by Alexander van der Vekens, 2-Dec-2017.)

|- ConnGrph = { <. v , e >. | A. k e. v A. n e. v E. f E. p f ( k ( v PathOn e ) n ) p }

Theorem

dfconngra1 21611*

Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017.)

|- ConnGrph = { <. v , e >. | A. k e. v A. n e. ( v \ { k } ) E. f E. p f ( k ( v PathOn e ) n ) p }

Theorem

isconngra 21612*

The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.)

|- ( ( V e. X /\ E e. Y ) -> ( V ConnGrph E <-> A. k e. V A. n e. V E. f E. p f ( k ( V PathOn E ) n ) p ) )

Theorem

isconngra1 21613*

The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.)

|- ( ( V e. X /\ E e. Y ) -> ( V ConnGrph E <-> A. k e. V A. n e. ( V \ { k } ) E. f E. p f ( k ( V PathOn E ) n ) p ) )

Theorem

0conngra 21614

A class/graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.)

|- ( E e. V -> (/) ConnGrph E )

Theorem

1conngra 21615

A class/graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.)

|- ( E e. V -> { A } ConnGrph E )

Theorem

cusconngra 21616

A complete (undirected simple) graph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.)

|- ( V ComplUSGrph E -> V ConnGrph E )

14.1.6  Vertex Degree

Syntax

cvdg 21617

Extend class notation with the vertex degree function.

class VDeg

Definition

df-vdgr 21618*

Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, we have to double-count those edges that contain u "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition + e is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)

|- VDeg = ( v e. _V , e e. _V |-> ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) + e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )

Theorem

vdgrfval 21619*

The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)

|- ( ( V e. W /\ E Fn A /\ A e. X ) -> ( V VDeg E ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( E ` x ) } ) + e ( # ` { x e. A | ( E ` x ) = { u } } ) ) ) )

Theorem

vdgrval 21620*

The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)

|- ( ( ( V e. W /\ E Fn A /\ A e. X ) /\ U e. V ) -> ( ( V VDeg E ) ` U ) = ( ( # ` { x e. A | U e. ( E ` x ) } ) + e ( # ` { x e. A | ( E ` x ) = { U } } ) ) )

Theorem

vdgrfival 21621*

The value of the vertex degree function (for graphs of finite size). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.)

|- ( ( ( V e. W /\ E Fn A /\ A e. Fin ) /\ U e. V ) -> ( ( V VDeg E ) ` U ) = ( ( # ` { x e. A | U e. ( E ` x ) } ) + ( # ` { x e. A | ( E ` x ) = { U } } ) ) )

Theorem

vdgrf 21622

The vertex degree function is a function from vertices to nonnegative integers or plus infinity. (Contributed by Alexander van der Vekens, 20-Dec-2017.)

|- ( ( V e. W /\ E Fn A /\ A e. X ) -> ( V VDeg E ) : V --> ( NN0 u. { +oo } ) )

Theorem

vdgrfif 21623

The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)

|- ( ( V e. W /\ E Fn A /\ A e. Fin ) -> ( V VDeg E ) : V --> NN0 )

Theorem

vdgr0 21624

The degree of a vertex in an empty graph is zero, because there are no edges. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)

|- ( ( V e. W /\ U e. V ) -> ( ( V VDeg (/) ) ` U ) = 0 )

Theorem

vdgrun 21625

The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.)

|- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> V UMGrph E )   &    |- ( ph -> V UMGrph F )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( ( V VDeg ( E u. F ) ) ` U ) = ( ( ( V VDeg E ) ` U ) + e ( ( V VDeg F ) ` U ) ) )

Theorem

vdgrfiun 21626

The degree of a vertex in the union of two graphs (of finite size) on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.)

|- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> V UMGrph E )   &    |- ( ph -> V UMGrph F )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( ( V VDeg ( E u. F ) ) ` U ) = ( ( ( V VDeg E ) ` U ) + ( ( V VDeg F ) ` U ) ) )

Theorem

vdgr1d 21627

The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.)

|- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( ( V VDeg { <. A , { U } >. } ) ` U ) = 2 )

Theorem

vdgr1b 21628

The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.)

|- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> U e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> B =/= U )   =>    |- ( ph -> ( ( V VDeg { <. A , { U , B } >. } ) ` U ) = 1 )

Theorem

vdgr1c 21629

The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.)

|- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> U e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> B =/= U )   =>    |- ( ph -> ( ( V VDeg { <. A , { B , U } >. } ) ` U ) = 1 )

Theorem

vdgr1a 21630

The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.)

|- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> U e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> B =/= U )   &    |- ( ph -> C e. V )   &    |- ( ph -> C =/= U )   =>    |- ( ph -> ( ( V VDeg { <. A , { B , C } >. } ) ` U ) = 0 )

Theorem

vdusgraval 21631*

The value of the vertex degree function for simple undirected graphs. (Contributed by Alexander van der Vekens, 20-Dec-2017.)

|- ( ( V USGrph E /\ U e. V ) -> ( ( V VDeg E ) ` U ) = ( # ` { x e. dom E | U e. ( E ` x ) } ) )

Theorem

vdusgra0nedg 21632*

If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.)

|- ( ( V USGrph E /\ U e. V /\ E e. Fin ) -> ( ( ( V VDeg E ) ` U ) = 0 -> -. E. v e. V { U , v } e. ran E ) )

Theorem

vdgrnn0pnf 21633

The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.)

|- ( ( V USGrph E /\ X e. V ) -> ( ( V VDeg E ) ` X ) e. ( NN0 u. { +oo } ) )

Theorem

hashnbgravd 21634

The size of the set of the neighbors of a vertex is the vertex degree of this vertex. (Contributed by Alexander van der Vekens, 17-Dec-2017.)

|- ( ( V USGrph E /\ U e. V /\ E e. Fin ) -> ( # ` ( <. V , E >. Neighbors U ) ) = ( ( V VDeg E ) ` U ) )

Theorem

hashnbgravdg 21635

The size of the set of the neighbors of a vertex is the vertex degree of this vertex, analogous to hashnbgravd 21634. (Contributed by Alexander van der Vekens, 20-Dec-2017.)

|- ( ( V USGrph E /\ U e. V ) -> ( # ` ( <. V , E >. Neighbors U ) ) = ( ( V VDeg E ) ` U ) )

Theorem

usgravd0nedg 21636*

If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge, analogous to vdusgra0nedg 21632. (Contributed by Alexander van der Vekens, 20-Dec-2017.)

|- ( ( V USGrph E /\ U e. V ) -> ( ( ( V VDeg E ) ` U ) = 0 -> -. E. v e. V { U , v } e. ran E ) )

14.2  Eulerian paths and the Konigsberg Bridge problem

14.2.1  Eulerian paths

Syntax

ceup 21637

Extend class notation with Eulerian paths.

class EulPaths

Definition

df-eupa 21638*

Define the set of all Eulerian paths on an undirected multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.)

|- EulPaths = ( v e. _V , e e. _V |-> { <. f , p >. | ( v UMGrph e /\ E. n e. NN0 ( f : ( 1 ... n ) -1-1-onto-> dom e /\ p : ( 0 ... n ) --> v /\ A. k e. ( 1 ... n ) ( e ` ( f ` k ) ) = { ( p ` ( k - 1 ) ) , ( p ` k ) } ) ) } )

Theorem

releupa 21639

The set ( V EulPaths E ) of all Eulerian paths on <. V , E >. is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.)

|- Rel ( V EulPaths E )

Theorem

iseupa 21640*

The property " <. F , P >. is an Eulerian path on the graph <. V , E >.". An Eulerian path is defined as bijection F from the edges to a set 1 ... N a function P : ( 0 ... N ) --> V into the vertices such that for each 1 <_ k <_ N, F ( k ) is an edge from P ( k - 1 ) to P ( k ). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.)

|- ( dom E = A -> ( F ( V EulPaths E ) P <-> ( V UMGrph E /\ E. n e. NN0 ( F : ( 1 ... n ) -1-1-onto-> A /\ P : ( 0 ... n ) --> V /\ A. k e. ( 1 ... n ) ( E ` ( F ` k ) ) = { ( P ` ( k - 1 ) ) , ( P ` k ) } ) ) ) )

Theorem

eupagra 21641

If an eulerian path exists, then <. V , E >. is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)

|- ( F ( V EulPaths E ) P -> V UMGrph E )

Theorem

eupai 21642*

Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.)

|- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> ( ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) -1-1-onto-> A /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 1 ... ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` ( k - 1 ) ) , ( P ` k ) } ) )

Theorem

eupatrl 21643*

An Eulerian path is a trail.

Unfortunately, the edge function F of an Eulerian path has the domain ( 1 ... ( # ` F ) ), whereas the edge functions of all kinds of walks defined here have the domain ( 0..^ ( # ` F ) ) (i.e. the edge functions are "words of edge indices", see discussion and proposal of Mario Carneiro at https://groups.google.com/d/msg/metamath/KdVXdL3IH3k/2-BYcS_ACQAJ). Therefore, the arguments of the edge function of an Eulerian path must be shifted by 1 to obtain an edge function of a trail in this theorem, using the auxiliary theorems above (fargshiftlem 21574, fargshiftfv 21575, etc.). TODO: The definition of an Eulerian path and all related theorems should be modified to fit to the general definition of a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017.)

|- G = ( x e. ( 0..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )   =>    |- ( F ( V EulPaths E ) P -> G ( V Trails E ) P )

Theorem

eupacl 21644

An Eulerian path has length # ( F ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.)

|- ( F ( V EulPaths E ) P -> ( # ` F ) e. NN0 )

Theorem

eupaf1o 21645

The F function in an Eulerian path is a bijection from a one-based sequence to the set of edges. (Contributed by Mario Carneiro, 12-Mar-2015.)

|- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )

Theorem

eupafi 21646

Any graph with an Eulerian path is finite. (Contributed by Mario Carneiro, 7-Apr-2015.)

|- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> A e. Fin )

Theorem

eupapf 21647

The P function in an Eulerian path is a function from a zero-based finite sequence to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015.)

|- ( F ( V EulPaths E ) P -> P : ( 0 ... ( # ` F ) ) --> V )

Theorem

eupaseg 21648

The N-th edge in an eulerian path is the edge from P ( N - 1 ) to P ( N ). (Contributed by Mario Carneiro, 12-Mar-2015.)

|- ( ( F ( V EulPaths E ) P /\ N e. ( 1 ... ( # ` F ) ) ) -> ( E ` ( F ` N ) ) = { ( P ` ( N - 1 ) ) , ( P ` N ) } )

Theorem

eupa0 21649

There is an Eulerian path on the empty graph. (Contributed by Mario Carneiro, 7-Apr-2015.)

|- ( ( V e. W /\ A e. V ) -> (/) ( V EulPaths (/) ) { <. 0 , A >. } )

Theorem

eupares 21650

The restriction of an Eulerian path to an initial segment of the path forms an Eulerian path on the subgraph consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.)

|- ( ph -> G ( V EulPaths E ) P )   &    |- ( ph -> N e. ( 0 ... ( # ` G ) ) )   &    |- F = ( E |` ( G " ( 1 ... N ) ) )   &    |- H = ( G |` ( 1 ... N ) )   &    |- Q = ( P |` ( 0 ... N ) )   =>    |- ( ph -> H ( V EulPaths F ) Q )

Theorem

eupap1 21651

Append one path segment to an Eulerian path (enlarging the graph to add the new edge). (Contributed by Mario Carneiro, 7-Apr-2015.)

|- ( ph -> E Fn A )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ph -> G ( V EulPaths E ) P )   &    |- ( ph -> N = ( # ` G ) )   &    |- F = ( E u. { <. B , { ( P ` N ) , C } >. } )   &    |- H = ( G u. { <. ( N + 1 ) , B >. } )   &    |- Q = ( P u. { <. ( N + 1 ) , C >. } )   =>    |- ( ph -> H ( V EulPaths F ) Q )

Theorem

eupath2lem1 21652

Lemma for eupath2 21655. (Contributed by Mario Carneiro, 8-Apr-2015.)

|- ( U e. V -> ( U e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )

Theorem

eupath2lem2 21653

Lemma for eupath2 21655. (Contributed by Mario Carneiro, 8-Apr-2015.)

|- B e. _V   =>    |- ( ( B =/= C /\ B = U ) -> ( -. U e. if ( A = B , (/) , { A , B } ) <-> U e. if ( A = C , (/) , { A , C } ) ) )

Theorem

eupath2lem3 21654*

Lemma for eupath2 21655. (Contributed by Mario Carneiro, 8-Apr-2015.)

|- ( ph -> E Fn A )   &    |- ( ph -> F ( V EulPaths E ) P )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> ( N + 1 ) <_ ( # ` F ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> { x e. V | -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )   =>    |- ( ph -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )

Theorem

eupath2 21655*

The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (Contributed by Mario Carneiro, 8-Apr-2015.)

|- ( ph -> E Fn A )   &    |- ( ph -> F ( V EulPaths E ) P )   =>    |- ( ph -> { x e. V | -. 2 || ( ( V VDeg E ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) )

Theorem

eupath 21656*

A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.)

|- ( ( V EulPaths E ) =/= (/) -> ( # ` { x e. V | -. 2 || ( ( V VDeg E ) ` x ) } ) e. { 0 , 2 } )

14.2.2  The Konigsberg Bridge problem

Theorem

vdeg0i 21657

The base case for the induction for calculating the degree of a vertex. The degree of U in the empty graph is 0. (Contributed by Mario Carneiro, 12-Mar-2015.)

|- V e. _V   &    |- U e. V   =>    |- ( ( V VDeg (/) ) ` U ) = 0

Theorem

umgrabi 21658*

Show that an unordered pair is a valid edge in a graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)

|- V e. _V   &    |- X e. V   &    |- Y e. V   =>    |- ( ph -> { X , Y } e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )

Theorem

vdegp1ai 21659*

The induction step for a vertex degree calculation. If the degree of U in the edge set E is P, then adding { X , Y } to the edge set, where X =/= U =/= Y, yields degree P as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)

|- V e. _V   &    |- ( T. -> E e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )   &    |- U e. V   &    |- ( ( V VDeg E ) ` U ) = P   &    |- X e. V   &    |- X =/= U   &    |- Y e. V   &    |- Y =/= U   &    |- F = ( E concat <" { X , Y } "> )   =>    |- ( ( V VDeg F ) ` U ) = P

Theorem

vdegp1bi 21660*

The induction step for a vertex degree calculation. If the degree of U in the edge set E is P, then adding { U , X } to the edge set, where X =/= U, yields degree P + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)

|- V e. _V   &    |- ( T. -> E e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )   &    |- U e. V   &    |- ( ( V VDeg E ) ` U ) = P   &    |- Q = ( P + 1 )   &    |- X e. V   &    |- X =/= U   &    |- F = ( E concat <" { U , X } "> )   =>    |- ( ( V VDeg F ) ` U ) = Q

Theorem

vdegp1ci 21661*

The induction step for a vertex degree calculation. If the degree of U in the edge set E is P, then adding { X , U } to the edge set, where X =/= U, yields degree P + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)

|- V e. _V   &    |- ( T. -> E e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )   &    |- U e. V   &    |- ( ( V VDeg E ) ` U ) = P   &    |- Q = ( P + 1 )   &    |- X e. V   &    |- X =/= U   &    |- F = ( E concat <" { X , U } "> )   =>    |- ( ( V VDeg F ) ` U ) = Q

Theorem

konigsberg 21662

The Konigsberg Bridge problem. If <. V , E >. is the graph on four vertices 0 , 1 , 2 , 3, with edges { 0 , 1 } , { 0 , 2 } , { 0 , 3 } , { 1 , 2 } , { 1 , 2 } , { 2 , 3 } , { 2 , 3 }, then vertices 0 , 1 , 3 each have degree three, and 2 has degree five, so there are four vertices of odd degree and thus by eupath 21656 the graph cannot have an Eulerian path. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)

|- V = ( 0 ... 3 )   &    |- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">   =>    |- ( V EulPaths E ) = (/)

PART 15  GUIDES AND MISCELLANEA

15.1  Guides (conventions, explanations, and examples)

15.1.1  Conventions

This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. Logic and set theory provide a foundation for all of mathematics. To learn about them, you should study one or more of the references listed below. We indicate references using square brackets. The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:

• Axioms of propositional calculus - [Margaris].
• Axioms of predicate calculus - [Megill] (System S3' in the article referenced).
• Theorems of propositional calculus - [WhiteheadRussell].
• Theorems of pure predicate calculus - [Margaris].
• Theorems of equality and substitution - [Monk2], [Tarski], [Megill].
• Axioms of set theory - [BellMachover].
• Development of set theory - [TakeutiZaring]. (The first part of [Quine] has a good explanation of the powerful device of "virtual" or class abstractions, which is essential to our development.)
• Construction of real and complex numbers - [Gleason]
• Theorems about real numbers - [Apostol]

Theorem

conventions 21663

Here are some of the conventions we use in the Metamath Proof Explorer (aka "set.mm"), and how they correspond to typical textbook language (skipping the many cases where they're identical):

• Notation. Where possible, the notation attempts to conform to modern conventions, with variations due to our choice of the axiom system or to make proofs shorter. However, our notation is strictly sequential (left-to-right). For example, summation is written in the form sum_ k e. A B (df-sum 12435) which denotes that index variable k ranges over A when evaluating B. Thus, sum_ k e. NN ( 1 / ( 2 ^ k ) ) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 12614). Also, the method of definition, the axioms for predicate calculus, and the development of substitution are somewhat different from those found in standard texts. For example, the expressions for the axioms were designed for direct derivation of standard results without excessive use of metatheorems. (See Theorem 9.7 of [Megill] p. 448 for a rigorous justification.) The notation is usually explained in more detail when first introduced.
• Axiomatic assertions ($a). All axiomatic assertions ($a statements) starting with " |-" have labels starting with "ax-" (axioms) or "df-" (definitions). A statement with a label starting with "ax-" corresponds to what is traditionally called an axiom. A statement with a label starting with "df-" introduces new symbols or a new relationship among symbols that can be eliminated; they always extend the definition of a wff or class. Metamath blindly treats $a statements as new given facts but does not try to justify them. The mmj2 program will justify the definitions as sound, except for 4 (df-bi, df-cleq, df-clel, df-clab) that require a more complex metalogical justification by hand.
• Proven axioms. In some cases we wish to treat an expression as an axiom in later theorems, even though it can be proved. For example, we derive the postulates or axioms of complex arithmetic as theorems of ZFC set theory. For convenience, after deriving the postulates we re-introduce them as new axioms on top of set theory. This lets us easily identify which axioms are needed for a particular complex number proof, without the obfuscation of the set theory used to derive them. For more, see http://us.metamath.org/mpeuni/mmcomplex.html. When we wish to use a previously-proven assertion as an axiom, our convention is that we use the regular "ax-NAME" label naming convention to define the axiom, but we precede it with a proof of the same statement with the label "axNAME" . An example is complex arithmetic axiom ax-1cn 9004, proven by the preceding theorem ax1cn 8980. The metamath.exe program will warn if an axiom does not match the preceding theorem that justifies it if the names match in this way.
• Definitions (df-...). We encourage definitions to include hypertext links to proven examples.
• Statements with hypotheses. Many theorems and some axioms, such as ax-mp 8, have hypotheses that must be satisfied in order for the conclusion to hold, in this case min and maj. When presented in summarized form such as in the Theorem List (click on "Nearby theorems" on the ax-mp 8 page), the hypotheses are connected with an ampersand and separated from the conclusion with a big arrow, such as in " |- ph & |- ( ph -> ps ) => |- ps". These symbols are not part of the Metamath language but are just informal notation meaning "and" and "implies".
• Discouraged use and modification. If something should only be used in limited ways, it is marked with "(New usage is discouraged.)". This is used, for example, when something can be constructed in more than one way, and we do not want later theorems to depend on that specific construction. This marking is also used if we want later proofs to use proven axioms. For example, we want later proofs to use ax-1cn 9004 (not ax1cn 8980) and ax-1ne0 9015 (not ax1ne0 8991), as these are proven axioms for complex arithmetic. Thus, both ax1cn 8980 and ax1ne0 8991 are marked as "(New usage is discouraged.)". In some cases a proof should not normally be changed, e.g., when it demonstrates some specific technique. These are marked with "(Proof modification is discouraged.)".
• New definitions infrequent. Typically, we are minimalist when introducing new definitions; they are introduced only when a clear advantage becomes apparent for reducing the number of symbols, shortening proofs, etc. We generally avoid the introduction of gratuitous definitions because each one requires associated theorems and additional elimination steps in proofs. For example, we use < and <_ for inequality expressions, and use ( ( sin ` ( _i x. A ) ) / _i ) instead of (sinh ` A ) for the hyperbolic sine.
• Axiom of choice. The axiom of choice (df-ac 7953) is widely accepted, and ZFC is the most commonly-accepted fundamental set of axioms for mathematics. However, there have been and still are some lingering controversies about the Axiom of Choice. Therefore, where a proof does not require the axiom of choice, we prefer that proof instead. E.g., our proof of the Schroeder-Bernstein Theorem (sbth 7186) does not use the axiom of choice. In some cases, the weaker axiom of countable choice (ax-cc 8271) or axiom of dependent choice (ax-dc 8282) can be used instead.
• Variables. Typically, Greek letters ( ph = phi, ps = psi, ch = chi, etc.),... are used for propositional (wff) variables; x, y, z,... for individual (set) variables; and A, B, C,... for class variables.
• Turnstile. " |-", meaning "It is provable that," is the first token of all assertions and hypotheses that aren't syntax constructions. This is a standard convention in logic. For us, it also prevents any ambiguity with statements that are syntax constructions, such as "wff -. ph".
• Biconditional ( <->). There are basically two ways to maximize the effectiveness of biconditionals ( <->): you can either have one-directional simplifications of all theorems that produce biconditionals, or you can have one-directional simplifications of theorems that consume biconditionals. Some tools (like Lean) follow the first approach, but set.mm follows the second approach. Practically, this means that in set.mm, for every theorem that uses an implication in the hypothesis, like ax-mp 8, there is a corresponding version with a biconditional or a reversed biconditional, like mpbi 200 or mpbir 201. We prefer this second approach because the number of duplications in the second approach is bounded by the size of the propositional calculus section, which is much smaller than the number of possible theorems in all later sections that produce biconditionals. So although theorems like biimpi 187 are available, in most cases there is already a theorem that combines it with your theorem of choice, like mpbir2an 887, sylbir 205, or 3imtr4i 258.
• Substitution. " [ y / x ] ph" should be read "the wff that results from the proper substitution of y for x in wff ph." See df-sb 1656 and the related df-sbc 3122 and df-csb 3212.
• Is-a set. " A e. _V" should be read "Class A is a set (i.e. exists)." This is a convenient convention based on Definition 2.9 of [Quine] p. 19. See df-v 2918 and isset 2920.
• Converse. " `' R" should be read "converse of (relation) R" and is the same as the more standard notation R^{-1} (the standard notation is ambiguous). See df-cnv 4845. This can be used to define a subset, e.g., df-tan 12629 notates "the set of values whose cosine is a nonzero complex number" as ( `' cos " ( CC \ { 0 } ) ).
• Function application. "( F ` x)" should be read "the value of function F at x" and has the same meaning as the more familiar but ambiguous notation F(x). For example, ( cos ` 0 ) = 1 (see cos0 12706). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. See df-fv 5421. In the ASCII (input) representation there are spaces around the grave accent; there is a single accent when it is used directly, and it is doubled within comments.
• Infix and parentheses. When a function that takes two classes and produces a class is applied as part of an infix expression, the expression is always surrounded by parentheses (see df-ov 6043). For example, the + in ( 2 + 2 ); see 2p2e4 10054. Function application is itself an example of this. Similarly, predicate expressions in infix form that take two or three wffs and produce a wff are also always surrounded by parentheses, such as ( ph -> ps ), ( ph \/ ps ), ( ph /\ ps ), and ( ph <-> ps ) (see wi 4, df-or 360, df-an 361, and df-bi 178 respectively). In contrast, a binary relation (which compares two classes and produces a wff) applied in an infix expression is not surrounded by parentheses. This includes set membership A e. B (see wel 1722), equality A = B (see df-cleq 2397), subset A C_ B (see df-ss 3294), and less-than A < B (see df-lt 8959). For the general definition of a binary relation in the form A R B, see df-br 4173. For example, 0 < 1 ( see 0lt1 9506) does not use parentheses.
• Unary minus. The symbol -u is used to indicate a unary minus, e.g., -u 1. It is specially defined because it is so commonly used. See cneg 9248.
• Function definition. Functions are typically defined by first defining the constant symbol (using $c) and declaring that its symbol is a class with the label cNAME (e.g., ccos 12622). The function is then defined labelled df-NAME; definitions are typically given using the maps-to notation (e.g., df-cos 12628). Typically, there are other proofs such as its closure labelled NAMEcl (e.g., coscl 12683), its function application form labelled NAMEval (e.g., cosval 12679), and at least one simple value (e.g., cos0 12706).
• Factorial. The factorial function is traditionally a postfix operation, but we treat it as a normal function applied in prefix form, e.g., ( ! ` 4 ) = ; 2 4 (df-fac 11522 and fac4 11529).
• Unambiguous symbols. A given symbol has a single unambiguous meaning in general. Thus, where the literature might use the same symbol with different meanings, here we use different (variant) symbols for different meanings. These variant symbols often have suffixes, subscripts, or underlines to distinguish them. For example, here " 0" always means the value zero (df-0 8953), while " 0g" is the group identity element (df-0g 13682), " 0." is the poset zero (df-p0 14423), " 0 p" is the zero polynomial (df-0p 19515), " 0vec" is the zero vector in a normed complex vector space (df-0v 22030), and " .0." is a class variable for use as a connective symbol (this is used, for example, in p0val 14425). There are other class variables used as connective symbols where traditional notation would use ambiguous symbols, including " .1.", " .+", " .*", and " .||". These symbols are very similar to traditional notation, but because they are different symbols they eliminate ambiguity.
• Natural numbers. There are different definitions of "natural" numbers in the literature. We use NN (df-nn 9957) for the integer numbers starting from 1, and NN0 (df-n0 10178) for the set of nonnegative integers starting at zero.
• Decimal numbers. Numbers larger than ten are often expressed in base 10 using the decimal constructor df-dec 10339, e.g., ;;; 4 0 0 1 (see 4001prm 13419 for a proof that 4001 is prime).
• Theorem forms. We often call a theorem a "deduction" whenever the conclusion and all hypotheses are each prefixed with the same antecedent ph ->. Deductions are often the preferred form for theorems because they allow us to easily use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used. See, for example, a1d 23. A deduction hypothesis can have an indirect antecedent via definitions, e.g., see lhop 19853. Deductions have a label suffix of "d" if there are other forms of the same theorem. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 11. Finally, a "tautology" would be the form with no hypotheses, and its label would have no suffix. For example, see pm2.43 49, pm2.43i 45, and pm2.43d 46.
• Deduction theorem. The Deduction Theorem is a metalogical theorem that provides an algorithm for constructing a proof of a theorem from the proof of its corresponding deduction. In ordinary mathematics, no one actually carries out the algorithm, because (in its most basic form) it involves an exponential explosion of the number of proof steps as more hypotheses are eliminated. Instead, in ordinary mathematics the Deduction Theorem is invoked simply to claim that something can be done in principle, without actually doing it. For more details, see http://us.metamath.org/mpeuni/mmdeduction.html. The Deduction Theorem is a metalogical theorem that cannot be applied directly in metamath, and the explosion of steps would be a problem anyway, so alternatives are used. One alternative we use sometimes is the "weak deduction theorem" dedth 3740, which works in certain cases in set theory. We also sometimes use dedhb 3064. However, the primary mechanism we use today for emulating the deduction theorem is to write proofs in the deduction theorem form (aka "deduction style") described earlier; the prefixed ph -> mimics the context in a deduction proof system. In practice this mechanism works very well. This approach is described in the deduction form and natural deduction page; a list of translations for common natural deduction rules is given in natded 21664.
• Recursion. We define recursive functions using various "recursion constructors". These allow us to define, with compact direct definitions, functions that are usually defined in textbooks with indirect self-referencing recursive definitions. This produces compact definition and much simpler proofs, and greatly reduces the risk of creating unsound definitions. Examples of recursion constructors include recs ( F ) in df-recs 6592, rec ( F , I ) in df-rdg 6627, seq_𝜔 ( F , I ) in df-seqom 6664, and seq M ( .+ , F ) in df-seq 11279. These have characteristic function F and initial value I. ( gsum_g in df-gsum 13683 isn't really designed for arbitrary recursion, but you could do it with the right magma.) The logically primary one is df-recs 6592, but for the "average user" the most useful one is probably df-seq 11279- provided that a countable sequence is sufficient for the recursion.
• Extensible structures. Mathematics includes many structures such as ring, group, poset, etc. We define an "extensible structure" which is then used to define group, ring, poset, etc. This allows theorems from more general structures (groups) to be reused for more specialized structures (rings) without having to reprove them. See df-struct 13426.
• Organizing proofs. Humans have trouble understanding long proofs. It is often preferable to break longer proofs into smaller parts (just as with traditional proofs). In Metamath this is done by creating separate proofs of the separate parts. A proof with the sole purpose of supporting a final proof is a lemma; the naming convention for a lemma is the final proof's name followed by "lem", and a number if there is more than one. E.g., sbthlem1 7176 is the first lemma for sbth 7186. Also, consider proving reusable results separately, so that others will be able to easily reuse that part of your work.
• Hypertext links. We strongly encourage comments to have many links to related material, with accompanying text that explains the relationship. These can help readers understand the context. Links to other statements, or to HTTP/HTTPS URLs, can be inserted in ASCII source text by prepending a space-separated tilde. When metamath.exe is used to generate HTML it automatically inserts hypertext links for syntax used (e.g., every symbol used), every axiom and definition depended on, the justification for each step in a proof, and to both the next and previous assertion.
• Bibliography references. Please include a bibliographic reference to any external material used. A name in square brackets in a comment indicates a bibliographic reference. The full reference must be of the form KEYWORD IDENTIFIER? NOISEWORD(S)* [AUTHOR(S)] p. NUMBER - note that this is a very specific form that requires a page number. There should be no comma between the author reference and the "p." (a constant indicator). Whitespace, comma, period, or semicolon should follow NUMBER. An example is Theorem 3.1 of [Monk1] p. 22, The KEYWORD, which is not case-sensitive, must be one of the following: Axiom, Chapter, Compare, Condition, Corollary, Definition, Equation, Example, Exercise, Figure, Item, Lemma, Lemmas, Line, Lines, Notation, Part, Postulate, Problem, Property, Proposition, Remark, Rule, Scheme, Section, or Theorem. The IDENTIFIER is optional, as in for example "Remark in [Monk1] p. 22". The NOISEWORDS(S) are zero or more from the list: from, in, of, on. The AUTHOR(S) must be present in the file identified with the htmlbibliography assignment (e.g. mmset.html) as a named anchor (NAME=). If there is more than one document by the same author(s), add a numeric suffix (as shown here). The NUMBER is a page number, and may be any alphanumeric string such as an integer or Roman numeral. Note that we require page numbers in comments for individual $a or $p statements. We allow names in square brackets without page numbers (a reference to an entire document) in heading comments. If this is a new reference, please also add it to the "Bibliography" section of mmset.html. (The file mmbiblio.html is automatically rebuilt, e.g., using the metamath.exe "write bibliography" command.)
• Input format. The input is in ASCII with two-space indents. Tab characters are not allowed. Use embedded math comments or HTML entities for non-ASCII characters (e.g., "&eacute;" for "é").
• Information on syntax, axioms, and definitions. For a hyperlinked list of syntax, axioms, and definitions, see http://us.metamath.org/mpeuni/mmdefinitions.html. If you have questions about a specific symbol or axiom, it is best to go directly to its definition to learn more about it. The generated HTML for each theorem and axiom includes hypertext links to each symbol's definition.

Naming conventions

Every statement has a unique identifying label. We use various label naming conventions to provide easy-to-remember hints about their contents. Labels are not a 1-to-1 mapping, because that would create long names that would be difficult to remember and tedious to type. Instead, label names are relatively short while suggesting their purpose. Names are occasionally changed to make them more consistent or as we find better ways to name them. Here are a few of the label naming conventions:

• Axioms, definitions, and wff syntax. As noted earlier, axioms are named "ax-NAME", proofs of proven axioms are named "axNAME", and definitions are named "df-NAME". Wff syntax declarations have labels beginning with "w" followed by short fragment suggesting its purpose.
• Hypotheses. Hypotheses have the name of the final axiom or theorem, followed by ".", followed by a unique id.
• Common names. If a theorem has a well-known name, that name (or a short version of it) is sometimes used directly. Examples include barbara 2351 and stirling 27705.
• Syntax label fragments. Most theorems are named using syntax label fragments. Almost every syntactic construct has a definition labelled "df-NAME", and NAME normally is the syntax label fragment. For example, the difference construct ( A \ B ) is defined in df-dif 3283, and thus its syntax label fragment is "dif". Similarly, the singleton construct { A } has syntax label fragment "sn" (because it is defined in df-sn 3780), the subclass (subset) relation A C_ B has "ss" (because it is defined in df-ss 3294), and the pair construct { A , B } has "pr" (df-pr 3781). Theorem names are often a concatenation of the syntax label fragments (omitting variables). For example, a theorem about ( A \ B ) C_ A involves a difference ("dif") of a subset ("ss"), and thus is named difss 3434. Digits are used to represent themselves. Suffixes (e.g., with numbers) are sometimes used to distinguish multiple theorems that would otherwise produce the same label.
• Phantom definitions. In some cases there are common label fragments for something that could be in a definition, but for technical reasons is not. The is-element-of (is member of) construct A e. B does not have a df-NAME definition; in this case its syntax label fragment is "el". Thus, because the theorem beginning with ( A e. ( B \ { C } ) uses is-element-of ("el") of a difference ("dif") of a singleton ("sn"), it is named eldifsn 3887. An "n" is often used for negation ( -.), e.g., nan 564.
• Exceptions. Sometimes there is a definition df-NAME but the label fragment is not the NAME part. The table below attempts to list all such cases and marks them in bold. For example, label fragment "cn" represents complex numbers CC (even though its definition is in df-c 8952) and "re" represents real numbers RR. The empty set (/) often uses fragment 0, even though it is defined in df-nul 3589. Syntax construct ( A + B ) usually uses the fragment "add" (which is consistent with df-add 8957), but "p" is used as the fragment for constant theorems. Equality ( A = B ) often uses "e" as the fragment. As a result, "two plus two equals four" is named 2p2e4 10054.
• Other markings. In labels we sometimes use "com" for "commutative", "ass" for "associative", "rot" for "rotation", and "di" for "distributive".
• Principia Mathematica. Proofs of theorems from Principia Mathematica often use a different naming convention. They are instead often named "pm" followed by its identifier. For example, Theorem *2.27 of [WhiteheadRussell] p. 104 is named pm2.27 37.
• Closures and values. As noted above, if a function df-NAME is defined, there is typically a proof of its value named "NAMEval" and its closure named "NAMEcl". E.g., for cosine (df-cos 12628) we have value cosval 12679 and closure coscl 12683.
• Special cases. Sometimes syntax and related markings are insufficient to distinguish different theorems. For example, there are over 100 different implication-exclusive theorems. These are then grouped in a more ad-hoc way that attempts to make their distinctions clearer. These often use abbreviations such as "mp" for "modus ponens", "syl" for syllogism, and "id" for "identity". It's especially hard to give good names in the propositional calculus section because there are so few primitives. However, in most cases this is not a serious problem. There are a few very common theorems like ax-mp 8 and syl 16 that you will have no trouble remembering, a few theorem series like syl*anc and simp* that you can use parametrically, and a few other useful glue things for destructuring 'and's and 'or's (see natded 21664 for a list), and that's about all you need for most things. As for the rest, you can just assume that if it involves three or less connectives we probably already have a proof, and searching for it will give you the name.
• Suffixes. We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as F/ x ph in 19.21 1810 via the use of distinct variable conditions combined with nfv 1626. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 2260 derived from df-eu 2258. The "f" stands for "not free in" which is less restrictive than "does not occur in." We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 16) -type inference in a proof. When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for "more general") as in uniex 4664 vs. uniexg 4665. A theorem name is suffixed with "ALT" if it's an alternative less-preferred proof of a theorem.
• Reuse. When creating a new theorem or axiom, try to reuse abbreviations used elsewhere. A comment should explain the first use of an abbreviation.

The following table shows some commonly-used abbreviations in labels, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME. This is not a complete list of abbreviations, though we do want this to eventually be a complete list of exceptions.

Abbreviation	Mnenomic	Source	Expression	Syntax?	Example(s)
add	add (see "p")	df-add 8957	( A + B )	Yes	addcl 9028, addcom 9208, addass 9033
ALT	alternative/less preferred (suffix)			No
an	and	df-an 361	( ph /\ ps )	Yes	anor 476, iman 414, imnan 412
ass	associative			No	biass 349, orass 511, mulass 9034
bi	biconditional	df-bi 178	( ph <-> ps )	Yes	impbid 184
cn	complex numbers	df-c 8952	CC	Yes	nnsscn 9961, nncn 9964
com	commutative			No	orcom 377, bicomi 194, eqcomi 2408
d	deduction form			No	idd 22, impbid 184
di, distr	distributive			No	andi 838, imdi 353, ordi 835, difindi 3555, ndmovdistr 6195
dif	difference	df-dif 3283	( A \ B )	Yes	difss 3434, difindi 3555
div	division	df-div 9634	( A / B )	Yes	divcl 9640, divval 9636, divmul 9637
e, eq	equals	df-cleq 2397	A = B	Yes	2p2e4 10054, uneqri 3449
el	element of		A e. B	Yes	eldif 3290, eldifsn 3887, elssuni 4003
f	"not free in" (suffix)			No
g	more general (suffix); eliminates "is a set" hypothsis			No	uniexg 4665
id	identity			No
idm	idempotent			No	anidm 626, tpidm13 3866
im, imp	implication (label often omitted)	df-im 11861	( A -> B )	Yes	iman 414, imnan 412, impbidd 182
in	intersection	df-in 3287	( A i^i B )	Yes	elin 3490, incom 3493
is...	is (something a) ...?			No	isrng 15623
mp	modus ponens	ax-mp 8		No	mpd 15, mpi 17
mul	multiplication (see "t")	df-mul 8958	( A x. B )	Yes	mulcl 9030, divmul 9637, mulcom 9032, mulass 9034
n, not	not		-. ph	Yes	nan 564, notnot2 106
ne0	not equal to zero (see n0)		=/= 0	No	negne0d 9365, ine0 9425, gt0ne0 9449
nn	natural numbers	df-nn 9957	NN	Yes	nnsscn 9961, nncn 9964
n0	not the empty set (see ne0)		=/= (/)	No	n0i 3593, vn0 3595, ssn0 3620
or	or	df-or 360	( ph \/ ps )	Yes	orcom 377, anor 476
p	plus (see "add"), for all-constant theorems	df-add 8957	( 3 + 2 ) = 5	Yes	3p2e5 10067
pm	Principia Mathematica			No	pm2.27 37
pr	pair	df-pr 3781	{ A , B }	Yes	elpr 3792, prcom 3842, prid1g 3870, prnz 3883
q	QQ (quotients)	df-q 10531	QQ	Yes	elq 10532
re	real numbers	df-r 8956	RR	Yes	recn 9036, 0re 9047
rng	ring	df-rng 15618	Ring	Yes	rngidval 15621, isrng 15623, rnggrp 15624
rot	rotation			No	3anrot 941, 3orrot 942
s	eliminates need for syllogism (suffix)			No
sn	singleton	df-sn 3780	{ A }	Yes	eldifsn 3887
ss	subset	df-ss 3294	A C_ B	Yes	difss 3434
sub	subtract	df-sub 9249	( A - B )	Yes	subval 9253, subaddi 9343
syl	syllogism	syl 16		No	3syl 19
t	times (see "mul"), for all-constant theorems	df-mul 8958	( 3 x. 2 ) = 6	Yes	3t2e6 10084
tp	triple	df-tp 3782	{ A , B , C }	Yes	eltpi 3812, tpeq1 3852
un	union	df-un 3285	( A u. B )	Yes	uneqri 3449, uncom 3451
v	distinct variable conditions used when a not-free hypothesis (suffix)			No	spimv 1961
xr	eXtended reals	df-xr 9080	RR*	Yes	ressxr 9085, rexr 9086, 0xr 9087
z	ZZ (integers, from German Zahlen)	df-z 10239	ZZ	Yes	elz 10240, zcn 10243
0, z	slashed zero (empty set) (see n0)	df-nul 3589	(/)	Yes	n0i 3593, vn0 3595; snnz 3882, prnz 3883

Distinctness or freeness

Here are some conventions that address distinctness or freeness of a variable:

• F/ x ph is read " x is not free in (wff) ph"; see df-nf 1551 (whose description has some important technical details). Similarly, F/_ x A is read x is not free in (class) A, see df-nfc 2529.
• "$d x y $." should be read "Assume x and y are distinct variables."
• "$d x ph $." should be read "Assume x does not occur in phi $." Sometimes a theorem is proved using F/ x ph (df-nf 1551) in place of "$d x ph $." when a more general result is desired; ax-17 1623 can be used to derive the $d version. For an example of how to get from the $d version back to the $e version, see the proof of euf 2260 from df-eu 2258.
• "$d x A $." should be read "Assume x is not a variable occurring in class A."
• "$d x A $. $d x ps $. $e |- ( x = A -> ( ph <-> ps ) ) $." is an idiom often used instead of explicit substitution, meaning "Assume psi results from the proper substitution of A for x in phi."
• " |- ( -. A. x x = y -> ..." occurs early in some cases, and should be read "If x and y are distinct variables, then..." This antecedent provides us with a technical device (called a "distinctor" in Section 7 of [Megill] p. 444) to avoid the need for the $d statement early in our development of predicate calculus, permitting unrestricted substitutions as conceptually simple as those in propositional calculus. However, the $d eventually becomes a requirement, and after that this device is rarely used.

Here is more information about our processes for checking and contributing to this work:

• Multiple verifiers. This entire file is verified by multiple independently-implemented verifiers when it is checked in, giving us extremely high confidence that all proofs follow from the assumptions. The checkers also check for various other problems such as overly long lines.
• Rewrapped line length. The input file routinely has its text wrapped using metamath 'read set.mm' 'save proof */c/f' 'write source set.mm/rewrap' (so please do the same).
• Discouraged information. A separate file named "discouraged" lists all discouraged statements and uses of them, and this file is checked. If you change the use of discouraged things, you will need to change this file. This makes it obvious when there is a change to anything discouraged (triggering further review).
• Proposing specific changes. Please propose specific changes as pull requests (PRs) against the "develop" branch of set.mm, at: https://github.com/metamath/set.mm/tree/develop
• Community. We encourage anyone interested in Metamath to join our mailing list: https://groups.google.com/forum/#!forum/metamath.

(Contributed by DAW, 27-Dec-2016.)

|- ph   =>    |- ph

15.1.2  Natural deduction

Theorem

natded 21664

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.

Name	Natural Deduction Rule	Translation	Recommendation	Comments
IT	_G |- ps => _G |- ps	idi 2	nothing	Reiteration is always redundant in Metamath. Definition "new rule" in [Pfenning] p. 18, definition IT in [Clemente] p. 10.
/\I	_G |- ps & _G |- ch => _G |- ps /\ ch	jca 519	jca 519, pm3.2i 442	Definition /\I in [Pfenning] p. 18, definition I /\m,n in [Clemente] 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 446	simpld 446, adantr 452	Definition /\EL in [Pfenning] p. 18, definition E /\(1) in [Clemente] 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 450	simpr 448, adantl 453	Definition /\ER in [Pfenning] p. 18, definition E /\(2) in [Clemente] 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 424	ex 424	Definition ->I in [Pfenning] p. 18, definition I=>m,n in [Clemente] p. 11, and definition ->I in [Indrzejczak] p. 33.
->E	_G |- ps -> ch & _G |- ps => _G |- ch	mpd 15	ax-mp 8, mpd 15, mpdan 650, imp 419	Definition ->E in [Pfenning] p. 18, definition E=>m,n in [Clemente] p. 11, and definition ->E in [Indrzejczak] p. 33.
\/IL	_G |- ps => _G |- ps \/ ch	olcd 383	olc 374, olci 381, olcd 383	Definition \/I in [Pfenning] p. 18, definition I \/n(1) in [Clemente] p. 12
\/IR	_G |- ch => _G |- ps \/ ch	orcd 382	orc 375, orci 380, orcd 382	Definition \/IR in [Pfenning] p. 18, definition I \/n(2) in [Clemente] p. 12.
\/E	_G |- ps \/ ch & _G , ps |- th & _G , ch |- th => _G |- th	mpjaodan 762	mpjaodan 762, jaodan 761, jaod 370	Definition \/E in [Pfenning] p. 18, definition E \/m,n,p in [Clemente] p. 12.
-.I	_G , ps |- F. => _G |- -. ps	inegd 1339	pm2.01d 163
-.I	_G , ps |- th & _G |- -. th => _G |- -. ps	mtand 641	mtand 641	definition I -.m,n,p in [Clemente] p. 13.
-.I	_G , ps |- ch & _G , ps |- -. ch => _G |- -. ps	pm2.65da 560	pm2.65da 560	Contradiction.
-.I	_G , ps |- -. ps => _G |- -. ps	pm2.01da 430	pm2.01d 163, pm2.65da 560, pm2.65d 168	For an alternative falsum-free natural deduction ruleset
-.E	_G |- ps & _G |- -. ps => _G |- F.	pm2.21fal 1341	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 1336	tru 1327, a1tru 1336, trud 1329	Definition T.I in [Pfenning] p. 18.
F.E	_G , F. |- th	falimd 1335	falim 1334	Definition F.E in [Pfenning] p. 18.
A.I	_G |- [ a / x ] ps => _G |- A. x ps	alrimiv 1638	alrimiv 1638, ralrimiva 2749	Definition A.Ia in [Pfenning] p. 18, definition I A.n in [Clemente] p. 32.
A.E	_G |- A. x ps => _G |- [ t / x ] ps	spsbcd 3134	spcv 3002, rspcv 3008	Definition A.E in [Pfenning] p. 18, definition E A.n,t in [Clemente] p. 32.
E.I	_G |- [ t / x ] ps => _G |- E. x ps	spesbcd 3203	spcev 3003, rspcev 3012	Definition E.I in [Pfenning] p. 18, definition I E.n,t in [Clemente] p. 32.
E.E	_G |- E. x ps & _G , [ a / x ] ps |- th => _G |- th	exlimddv 1645	exlimddv 1645, exlimdd 1908, exlimdv 1643, rexlimdva 2790	Definition E.Ea,u in [Pfenning] p. 18, definition E E.m,n,p,a in [Clemente] p. 32.
F.C	_G , -. ps |- F. => _G |- ps	efald 1340	efald 1340	Proof by contradiction (classical logic), definition F.C in [Pfenning] p. 17.
F.C	_G , -. ps |- ps => _G |- ps	pm2.18da 431	pm2.18da 431, 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 [Clemente] p. 14.
EM	_G |- ps \/ -. ps	exmidd 406	exmid 405	Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Clemente] p. 14.
=I	_G |- A = A	eqidd 2405	eqid 2404, eqidd 2405	Introduce equality, definition =I in [Pfenning] p. 127.
=E	_G |- A = B & _G [. A / x ]. ps => _G |- [. B / x ]. ps	sbceq1dd 3127	sbceq1d 3126, 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 21665, ex-natded5.3 21668, ex-natded5.5 21671, ex-natded5.7 21672, ex-natded5.8 21674, ex-natded5.13 21676, ex-natded9.20 21678, and ex-natded9.26 21680.

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

|- ph   =>    |- ph

15.1.3  Natural deduction examples

These are examples of how natural deduction rules can be applied in metamath (both as line-for-line translations of ND rules, and as a way to apply deduction forms without being limited to applying ND rules). For more information, see natded 21664 and http://us.metamath.org/mpeuni/mmnatded.html.

Theorem

ex-natded5.2 21665

Theorem 5.2 of [Clemente] 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 Translation	ND Rationale	MPE Rationale
1	5	( ( ps /\ ch ) -> th )	( ph -> ( ( ps /\ ch ) -> th ) )	Given	$e.
2	2	( ch -> ps )	( ph -> ( ch -> ps ) )	Given	$e.
3	1	ch	( ph -> ch )	Given	$e.
4	3	ps	( ph -> ps )	->E 2,3	mpd 15, the MPE equivalent of ->E, 1,2
5	4	( ps /\ ch )	( ph -> ( ps /\ ch ) )	/\I 4,3	jca 519, the MPE equivalent of /\I, 3,1
6	6	th	( ph -> th )	->E 1,5	mpd 15, 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 21666. A proof without context is shown in ex-natded5.2i 21667. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ph -> ( ( ps /\ ch ) -> th ) )   &    |- ( ph -> ( ch -> ps ) )   &    |- ( ph -> ch )   =>    |- ( ph -> th )

Theorem

ex-natded5.2-2 21666

A more efficient proof of Theorem 5.2 of [Clemente] p. 15. Compare with ex-natded5.2 21665 and ex-natded5.2i 21667. (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ph -> ( ( ps /\ ch ) -> th ) )   &    |- ( ph -> ( ch -> ps ) )   &    |- ( ph -> ch )   =>    |- ( ph -> th )

Theorem

ex-natded5.2i 21667

The same as ex-natded5.2 21665 and ex-natded5.2-2 21666 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ( ps /\ ch ) -> th )   &    |- ( ch -> ps )   &    |- ch   =>    |- th

Theorem

ex-natded5.3 21668

Theorem 5.3 of [Clemente] 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 21669. A proof without context is shown in ex-natded5.3i 21670. 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 Translation	ND Rationale	MPE Rationale
1	2;3	( ps -> ch )	( ph -> ( ps -> ch ) )	Given	$e; adantr 452 to move it into the ND hypothesis
2	5;6	( ch -> th )	( ph -> ( ch -> th ) )	Given	$e; adantr 452 to move it into the ND hypothesis
3	1	...| ps	( ( ph /\ ps ) -> ps )	ND hypothesis assumption	simpr 448, to access the new assumption
4	4	... ch	( ( ph /\ ps ) -> ch )	->E 1,3	mpd 15, the MPE equivalent of ->E, 1.3. adantr 452 was used to transform its dependency (we could also use imp 419 to get this directly from 1)
5	7	... th	( ( ph /\ ps ) -> th )	->E 2,4	mpd 15, the MPE equivalent of ->E, 4,6. adantr 452 was used to transform its dependency
6	8	... ( ch /\ th )	( ( ph /\ ps ) -> ( ch /\ th ) )	/\I 4,5	jca 519, the MPE equivalent of /\I, 4,7
7	9	( ps -> ( ch /\ th ) )	( ph -> ( ps -> ( ch /\ th ) ) )	->I 3,6	ex 424, 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 ) ) )

Theorem

ex-natded5.3-2 21669

A more efficient proof of Theorem 5.3 of [Clemente] p. 16. Compare with ex-natded5.3 21668 and ex-natded5.3i 21670. (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ch -> th ) )   =>    |- ( ph -> ( ps -> ( ch /\ th ) ) )

Theorem

ex-natded5.3i 21670

The same as ex-natded5.3 21668 and ex-natded5.3-2 21669 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ps -> ch )   &    |- ( ch -> th )   =>    |- ( ps -> ( ch /\ th ) )

Theorem

ex-natded5.5 21671

Theorem 5.5 of [Clemente] 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 Translation	ND Rationale	MPE Rationale
1	2;3	( ps -> ch )	( ph -> ( ps -> ch ) )	Given	$e; adantr 452 to move it into the ND hypothesis
2	5	-. ch	( ph -> -. ch )	Given	$e; we'll use adantr 452 to move it into the ND hypothesis
3	1	...| ps	( ph -> ps )	ND hypothesis assumption	simpr 448
4	4	... ch	( ( ph /\ ps ) -> ch )	->E 1,3	mpd 15 1,3
5	6	... -. ch	( ( ph /\ ps ) -> -. ch )	IT 2	adantr 452 5
6	7	-. ps	( ph -> -. ps )	/\I 3,4,5	pm2.65da 560 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 452; simpr 448 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 )

Theorem

ex-natded5.7 21672

Theorem 5.7 of [Clemente] 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 21673. 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 Translation	ND Rationale	MPE Rationale
1	6	( ps \/ ( ch /\ th ) )	( ph -> ( ps \/ ( ch /\ th ) ) )	Given	$e. No need for adantr 452 because we do not move this into an ND hypothesis
2	1	...| ps	( ( ph /\ ps ) -> ps )	ND hypothesis assumption (new scope)	simpr 448
3	2	... ( ps \/ ch )	( ( ph /\ ps ) -> ( ps \/ ch ) )	\/IL 2	orcd 382, the MPE equivalent of \/IL, 1
4	3	...| ( ch /\ th )	( ( ph /\ ( ch /\ th ) ) -> ( ch /\ th ) )	ND hypothesis assumption (new scope)	simpr 448
5	4	... ch	( ( ph /\ ( ch /\ th ) ) -> ch )	/\EL 4	simpld 446, the MPE equivalent of /\EL, 3
6	6	... ( ps \/ ch )	( ( ph /\ ( ch /\ th ) ) -> ( ps \/ ch ) )	\/IR 5	olcd 383, the MPE equivalent of \/IR, 4
7	7	( ps \/ ch )	( ph -> ( ps \/ ch ) )	\/E 1,3,6	mpjaodan 762, 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 ) )

Theorem

ex-natded5.7-2 21673

A more efficient proof of Theorem 5.7 of [Clemente] p. 19. Compare with ex-natded5.7 21672. (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ph -> ( ps \/ ( ch /\ th ) ) )   =>    |- ( ph -> ( ps \/ ch ) )

Theorem

ex-natded5.8 21674

Theorem 5.8 of [Clemente] 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 Translation	ND Rationale	MPE Rationale
1	10;11	( ( ps /\ ch ) -> -. th )	( ph -> ( ( ps /\ ch ) -> -. th ) )	Given	$e; adantr 452 to move it into the ND hypothesis
2	3;4	( ta -> th )	( ph -> ( ta -> th ) )	Given	$e; adantr 452 to move it into the ND hypothesis
3	7;8	ch	( ph -> ch )	Given	$e; adantr 452 to move it into the ND hypothesis
4	1;2	ta	( ph -> ta )	Given	$e. adantr 452 to move it into the ND hypothesis
5	6	...| ps	( ( ph /\ ps ) -> ps )	ND Hypothesis/Assumption	simpr 448. New ND hypothesis scope, each reference outside the scope must change antedent ph to ( ph /\ ps ).
6	9	... ( ps /\ ch )	( ( ph /\ ps ) -> ( ps /\ ch ) )	/\I 5,3	jca 519 ( /\I), 6,8 (adantr 452 to bring in scope)
7	5	... -. th	( ( ph /\ ps ) -> -. th )	->E 1,6	mpd 15 ( ->E), 2,4
8	12	... th	( ( ph /\ ps ) -> th )	->E 2,4	mpd 15 ( ->E), 9,11; note the contradiction with ND line 7 (MPE line 5)
9	13	-. ps	( ph -> -. ps )	-.I 5,7,8	pm2.65da 560 ( -.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 452; simpr 448 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 21675.

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

|- ( ph -> ( ( ps /\ ch ) -> -. th ) )   &    |- ( ph -> ( ta -> th ) )   &    |- ( ph -> ch )   &    |- ( ph -> ta )   =>    |- ( ph -> -. ps )

Theorem

ex-natded5.8-2 21675

A more efficient proof of Theorem 5.8 of [Clemente] p. 20. For a longer line-by-line translation, see ex-natded5.8 21674. (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ph -> ( ( ps /\ ch ) -> -. th ) )   &    |- ( ph -> ( ta -> th ) )   &    |- ( ph -> ch )   &    |- ( ph -> ta )   =>    |- ( ph -> -. ps )

Theorem

ex-natded5.13 21676

Theorem 5.13 of [Clemente] 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 21677. 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 Translation	ND Rationale	MPE Rationale
1	15	( ps \/ ch )	( ph -> ( ps \/ ch ) )	Given	$e.
2;3	2	( ps -> th )	( ph -> ( ps -> th ) )	Given	$e. adantr 452 to move it into the ND hypothesis
3	9	( -. ta -> -. ch )	( ph -> ( -. ta -> -. ch ) )	Given	$e. ad2antrr 707 to move it into the ND sub-hypothesis
4	1	...| ps	( ( ph /\ ps ) -> ps )	ND hypothesis assumption	simpr 448
5	4	... th	( ( ph /\ ps ) -> th )	->E 2,4	mpd 15 1,3
6	5	... ( th \/ ta )	( ( ph /\ ps ) -> ( th \/ ta ) )	\/I 5	orcd 382 4
7	6	...| ch	( ( ph /\ ch ) -> ch )	ND hypothesis assumption	simpr 448
8	8	... ...| -. ta	( ( ( ph /\ ch ) /\ -. ta ) -> -. ta )	(sub) ND hypothesis assumption	simpr 448
9	11	... ... -. ch	( ( ( ph /\ ch ) /\ -. ta ) -> -. ch )	->E 3,8	mpd 15 8,10
10	7	... ... ch	( ( ( ph /\ ch ) /\ -. ta ) -> ch )	IT 7	adantr 452 6
11	12	... -. -. ta	( ( ph /\ ch ) -> -. -. ta )	-.I 8,9,10	pm2.65da 560 7,11
12	13	... ta	( ( ph /\ ch ) -> ta )	-.E 11	notnotrd 107 12
13	14	... ( th \/ ta )	( ( ph /\ ch ) -> ( th \/ ta ) )	\/I 12	olcd 383 13
14	16	( th \/ ta )	( ph -> ( th \/ ta ) )	\/E 1,6,13	mpjaodan 762 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 452; simpr 448 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 ) )

Theorem

ex-natded5.13-2 21677

A more efficient proof of Theorem 5.13 of [Clemente] p. 20. Compare with ex-natded5.13 21676. (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ph -> ( ps \/ ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ( ph -> ( -. ta -> -. ch ) )   =>    |- ( ph -> ( th \/ ta ) )

Theorem

ex-natded9.20 21678

Theorem 9.20 of [Clemente] 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 Translation	ND Rationale	MPE Rationale
1	1	( ps /\ ( ch \/ th ) )	( ph -> ( ps /\ ( ch \/ th ) ) )	Given	$e
2	2	ps	( ph -> ps )	/\EL 1	simpld 446 1
3	11	( ch \/ th )	( ph -> ( ch \/ th ) )	/\ER 1	simprd 450 1
4	4	...| ch	( ( ph /\ ch ) -> ch )	ND hypothesis assumption	simpr 448
5	5	... ( ps /\ ch )	( ( ph /\ ch ) -> ( ps /\ ch ) )	/\I 2,4	jca 519 3,4
6	6	... ( ( ps /\ ch ) \/ ( ps /\ th ) )	( ( ph /\ ch ) -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )	\/IR 5	orcd 382 5
7	8	...| th	( ( ph /\ th ) -> th )	ND hypothesis assumption	simpr 448
8	9	... ( ps /\ th )	( ( ph /\ th ) -> ( ps /\ th ) )	/\I 2,7	jca 519 7,8
9	10	... ( ( ps /\ ch ) \/ ( ps /\ th ) )	( ( ph /\ th ) -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )	\/IL 8	olcd 383 9
10	12	( ( ps /\ ch ) \/ ( ps /\ th ) )	( ph -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )	\/E 3,6,9	mpjaodan 762 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 452; simpr 448 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 21679. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.)

|- ( ph -> ( ps /\ ( ch \/ th ) ) )   =>    |- ( ph -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )

Theorem

ex-natded9.20-2 21679

A more efficient proof of Theorem 9.20 of [Clemente] p. 45. Compare with ex-natded9.20 21678. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.)

|- ( ph -> ( ps /\ ( ch \/ th ) ) )   =>    |- ( ph -> ( ( ps /\ ch ) \/ ( ps /\ th ) ) )

Theorem

ex-natded9.26 21680*

Theorem 9.26 of [Clemente] 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 Translation	ND Rationale	MPE Rationale
1	3	E. x A. y ps ( x , y )	( ph -> E. x A. y ps )	Given	$e.
2	6	...| A. y ps ( x , y )	( ( ph /\ A. y ps ) -> A. y ps )	ND hypothesis assumption	simpr 448. Later statements will have this scope.
3	7;5,4	... ps ( x , y )	( ( ph /\ A. y ps ) -> ps )	A.E 2,y	spsbcd 3134 ( A.E), 5,6. To use it we need a1i 11 and vex 2919. This could be immediately done with 19.21bi 1770, but we want to show the general approach for substitution.
4	12;8,9,10,11	... E. x ps ( x , y )	( ( ph /\ A. y ps ) -> E. x ps )	E.I 3,a	spesbcd 3203 ( E.I), 11. To use it we need sylibr 204, which in turn requires sylib 189 and two uses of sbcid 3137. This could be more immediately done using 19.8a 1758, but we want to show the general approach for substitution.
5	13;1,2	E. x ps ( x , y )	( ph -> E. x ps )	E.E 1,2,4,a	exlimdd 1908 ( E.E), 1,2,3,12. We'll need supporting assertions that the variable is free (not bound), as provided in nfv 1626 and nfe1 1743 (MPE# 1,2)
6	14	A. y E. x ps ( x , y )	( ph -> A. y E. x ps )	A.I 5	alrimiv 1638 ( 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 21681.

(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 )

Theorem

ex-natded9.26-2 21681*

A more efficient proof of Theorem 9.26 of [Clemente] p. 45. Compare with ex-natded9.26 21680. (Contributed by Mario Carneiro, 9-Feb-2017.)

|- ( ph -> E. x A. y ps )   =>    |- ( ph -> A. y E. x ps )

15.1.4  Definitional examples

Theorem

ex-or 21682

Example for df-or 360. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)

|- ( 2 = 3 \/ 4 = 4 )

Theorem

ex-an 21683

Example for df-an 361. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)

|- ( 2 = 2 /\ 3 = 3 )

Theorem

ex-dif 21684

Example for df-dif 3283. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

|- ( { 1 , 3 } \ { 1 , 8 } ) = { 3 }

Theorem

ex-un 21685

Example for df-un 3285. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

|- ( { 1 , 3 } u. { 1 , 8 } ) = { 1 , 3 , 8 }

Theorem

ex-in 21686

Example for df-in 3287. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

|- ( { 1 , 3 } i^i { 1 , 8 } ) = { 1 }

Theorem

ex-uni 21687

Example for df-uni 3976. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.)

|- U. { { 1 , 3 } , { 1 , 8 } } = { 1 , 3 , 8 }

Theorem

ex-ss 21688

Example for df-ss 3294. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

|- { 1 , 2 } C_ { 1 , 2 , 3 }

Theorem

ex-pss 21689

Example for df-pss 3296. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

|- { 1 , 2 } C. { 1 , 2 , 3 }

Theorem

ex-pw 21690

Example for df-pw 3761. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.)

|- ( A = { 3 , 5 , 7 } -> ~P A = ( ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) u. ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) ) )

Theorem

ex-pr 21691

Example for df-pr 3781. (Contributed by Mario Carneiro, 7-May-2015.)

|- ( A e. { 1 , -u 1 } -> ( A ^ 2 ) = 1 )

Theorem

ex-br 21692

Example for df-br 4173. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

|- ( R = { <. 2 , 6 >. , <. 3 , 9 >. } -> 3 R 9 )

Theorem

ex-opab 21693*

Example for df-opab 4227. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

|- ( R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 )

Theorem

ex-eprel 21694

Example for df-eprel 4454. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

|- 5 _E { 1 , 5 }

Theorem

ex-id 21695

Example for df-id 4458. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

|- ( 5 _I 5 /\ -. 4 _I 5 )

Theorem

ex-po 21696

Example for df-po 4463. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

|- ( < Po RR /\ -. <_ Po RR )

Theorem

ex-xp 21697

Example for df-xp 4843. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

|- ( { 1 , 5 } X. { 2 , 7 } ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } )

Theorem

ex-cnv 21698

Example for df-cnv 4845. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

|- `' { <. 2 , 6 >. , <. 3 , 9 >. } = { <. 6 , 2 >. , <. 9 , 3 >. }

Theorem

ex-co 21699

Example for df-co 4846. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

|- ( ( exp o. cos ) ` 0 ) = _e

Theorem

ex-dm 21700

Example for df-dm 4847. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

|- ( F = { <. 2 , 6 >. , <. 3 , 9 >. } -> dom F = { 2 , 3 } )