This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subgrprop2

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