Metamath Proof Explorer

Theorem egrsubgr

Description: An empty graph consisting of a subset of vertices of a graph (and having no edges) is a subgraph of the graph. (Contributed by AV, 17-Nov-2020) (Proof shortened by AV, 17-Dec-2020)

Ref Expression
Assertion egrsubgr 
|- ( ( ( G e. W /\ S e. U ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> S SubGraph G )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( ( G e. W /\ S e. U ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> ( Vtx ` S ) C_ ( Vtx ` G ) )
2 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
3 eqid 
 |-  ( Edg ` S ) = ( Edg ` S )
4 2 3 edg0iedg0 
 |-  ( Fun ( iEdg ` S ) -> ( ( Edg ` S ) = (/) <-> ( iEdg ` S ) = (/) ) )
5 4 adantl 
 |-  ( ( ( G e. W /\ S e. U ) /\ Fun ( iEdg ` S ) ) -> ( ( Edg ` S ) = (/) <-> ( iEdg ` S ) = (/) ) )
6 res0 
 |-  ( ( iEdg ` G ) |` (/) ) = (/)
7 6 eqcomi 
 |-  (/) = ( ( iEdg ` G ) |` (/) )
8 id 
 |-  ( ( iEdg ` S ) = (/) -> ( iEdg ` S ) = (/) )
9 dmeq 
 |-  ( ( iEdg ` S ) = (/) -> dom ( iEdg ` S ) = dom (/) )
10 dm0 
 |-  dom (/) = (/)
11 9 10 eqtrdi 
 |-  ( ( iEdg ` S ) = (/) -> dom ( iEdg ` S ) = (/) )
12 11 reseq2d 
 |-  ( ( iEdg ` S ) = (/) -> ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) = ( ( iEdg ` G ) |` (/) ) )
13 7 8 12 3eqtr4a 
 |-  ( ( iEdg ` S ) = (/) -> ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) )
14 5 13 biimtrdi 
 |-  ( ( ( G e. W /\ S e. U ) /\ Fun ( iEdg ` S ) ) -> ( ( Edg ` S ) = (/) -> ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) ) )
15 14 impr 
 |-  ( ( ( G e. W /\ S e. U ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) )
16 15 3adant2 
 |-  ( ( ( G e. W /\ S e. U ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) )
17 0ss 
 |-  (/) C_ ~P ( Vtx ` S )
18 sseq1 
 |-  ( ( Edg ` S ) = (/) -> ( ( Edg ` S ) C_ ~P ( Vtx ` S ) <-> (/) C_ ~P ( Vtx ` S ) ) )
19 17 18 mpbiri 
 |-  ( ( Edg ` S ) = (/) -> ( Edg ` S ) C_ ~P ( Vtx ` S ) )
20 19 adantl 
 |-  ( ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) -> ( Edg ` S ) C_ ~P ( Vtx ` S ) )
21 20 3ad2ant3 
 |-  ( ( ( G e. W /\ S e. U ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> ( Edg ` S ) C_ ~P ( Vtx ` S ) )
22 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
23 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
24 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
25 22 23 2 24 3 issubgr 
 |-  ( ( G e. W /\ S e. U ) -> ( S SubGraph G <-> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) )
26 25 3ad2ant1 
 |-  ( ( ( G e. W /\ S e. U ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> ( S SubGraph G <-> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) )
27 1 16 21 26 mpbir3and 
 |-  ( ( ( G e. W /\ S e. U ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> S SubGraph G )