Database
GRAPH THEORY
Undirected graphs
Subgraphs
subgrprop2
Metamath Proof Explorer
Description: The properties of a subgraph: If S is a subgraph of G , its
vertices are also vertices of G , and its edges are also edges of
G , connecting vertices of the subgraph only. (Contributed by AV , 19-Nov-2020)
Ref
Expression
Hypotheses
issubgr.v
|- V = ( Vtx ` S )
issubgr.a
|- A = ( Vtx ` G )
issubgr.i
|- I = ( iEdg ` S )
issubgr.b
|- B = ( iEdg ` G )
issubgr.e
|- E = ( Edg ` S )
Assertion
subgrprop2
|- ( S SubGraph G -> ( V C_ A /\ I C_ B /\ E C_ ~P V ) )
Proof
Step
Hyp
Ref
Expression
1
issubgr.v
|- V = ( Vtx ` S )
2
issubgr.a
|- A = ( Vtx ` G )
3
issubgr.i
|- I = ( iEdg ` S )
4
issubgr.b
|- B = ( iEdg ` G )
5
issubgr.e
|- E = ( Edg ` S )
6
1 2 3 4 5
subgrprop
|- ( S SubGraph G -> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) )
7
resss
|- ( B |` dom I ) C_ B
8
sseq1
|- ( I = ( B |` dom I ) -> ( I C_ B <-> ( B |` dom I ) C_ B ) )
9
7 8
mpbiri
|- ( I = ( B |` dom I ) -> I C_ B )
10
9
3anim2i
|- ( ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) -> ( V C_ A /\ I C_ B /\ E C_ ~P V ) )
11
6 10
syl
|- ( S SubGraph G -> ( V C_ A /\ I C_ B /\ E C_ ~P V ) )