Metamath Proof Explorer

Theorem subgrprop3

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 . (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses subgrprop3.v 
|- V = ( Vtx ` S )
subgrprop3.a 
|- A = ( Vtx ` G )
subgrprop3.e 
|- E = ( Edg ` S )
subgrprop3.b 
|- B = ( Edg ` G )
Assertion subgrprop3 
|- ( S SubGraph G -> ( V C_ A /\ E C_ B ) )

Proof

Step Hyp Ref Expression
1 subgrprop3.v 
 |-  V = ( Vtx ` S )
2 subgrprop3.a 
 |-  A = ( Vtx ` G )
3 subgrprop3.e 
 |-  E = ( Edg ` S )
4 subgrprop3.b 
 |-  B = ( Edg ` G )
5 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
6 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
7 1 2 5 6 3 subgrprop2 
 |-  ( S SubGraph G -> ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ E C_ ~P V ) )
8 3simpa 
 |-  ( ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ E C_ ~P V ) -> ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) )
9 7 8 syl 
 |-  ( S SubGraph G -> ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) )
10 simprl 
 |-  ( ( S SubGraph G /\ ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) ) -> V C_ A )
11 rnss 
 |-  ( ( iEdg ` S ) C_ ( iEdg ` G ) -> ran ( iEdg ` S ) C_ ran ( iEdg ` G ) )
12 11 ad2antll 
 |-  ( ( S SubGraph G /\ ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) ) -> ran ( iEdg ` S ) C_ ran ( iEdg ` G ) )
13 subgrv 
 |-  ( S SubGraph G -> ( S e. _V /\ G e. _V ) )
14 edgval 
 |-  ( Edg ` S ) = ran ( iEdg ` S )
15 14 a1i 
 |-  ( ( S e. _V /\ G e. _V ) -> ( Edg ` S ) = ran ( iEdg ` S ) )
16 3 15 syl5eq 
 |-  ( ( S e. _V /\ G e. _V ) -> E = ran ( iEdg ` S ) )
17 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
18 17 a1i 
 |-  ( ( S e. _V /\ G e. _V ) -> ( Edg ` G ) = ran ( iEdg ` G ) )
19 4 18 syl5eq 
 |-  ( ( S e. _V /\ G e. _V ) -> B = ran ( iEdg ` G ) )
20 16 19 sseq12d 
 |-  ( ( S e. _V /\ G e. _V ) -> ( E C_ B <-> ran ( iEdg ` S ) C_ ran ( iEdg ` G ) ) )
21 13 20 syl 
 |-  ( S SubGraph G -> ( E C_ B <-> ran ( iEdg ` S ) C_ ran ( iEdg ` G ) ) )
22 21 adantr 
 |-  ( ( S SubGraph G /\ ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) ) -> ( E C_ B <-> ran ( iEdg ` S ) C_ ran ( iEdg ` G ) ) )
23 12 22 mpbird 
 |-  ( ( S SubGraph G /\ ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) ) -> E C_ B )
24 10 23 jca 
 |-  ( ( S SubGraph G /\ ( V C_ A /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) ) -> ( V C_ A /\ E C_ B ) )
25 9 24 mpdan 
 |-  ( S SubGraph G -> ( V C_ A /\ E C_ B ) )