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∈W∧S∈U∧Vtx⁡S⊆Vtx⁡G∧Fun⁡iEdg⁡S∧Edg⁡S=∅→SSubGraphG

Proof

Step Hyp Ref Expression
1 simp2 ⊢G∈W∧S∈U∧Vtx⁡S⊆Vtx⁡G∧Fun⁡iEdg⁡S∧Edg⁡S=∅→Vtx⁡S⊆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∈W∧S∈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 syl6bi ⊢G∈W∧S∈U∧Fun⁡iEdg⁡S→Edg⁡S=∅→iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S
15 14 impr ⊢G∈W∧S∈U∧Fun⁡iEdg⁡S∧Edg⁡S=∅→iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S
16 15 3adant2 ⊢G∈W∧S∈U∧Vtx⁡S⊆Vtx⁡G∧Fun⁡iEdg⁡S∧Edg⁡S=∅→iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S
17 0ss ⊢∅⊆𝒫Vtx⁡S
18 sseq1 ⊢Edg⁡S=∅→Edg⁡S⊆𝒫Vtx⁡S↔∅⊆𝒫Vtx⁡S
19 17 18 mpbiri ⊢Edg⁡S=∅→Edg⁡S⊆𝒫Vtx⁡S
20 19 adantl ⊢Fun⁡iEdg⁡S∧Edg⁡S=∅→Edg⁡S⊆𝒫Vtx⁡S
21 20 3ad2ant3 ⊢G∈W∧S∈U∧Vtx⁡S⊆Vtx⁡G∧Fun⁡iEdg⁡S∧Edg⁡S=∅→Edg⁡S⊆𝒫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∈W∧S∈U→SSubGraphG↔Vtx⁡S⊆Vtx⁡G∧iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S∧Edg⁡S⊆𝒫Vtx⁡S
26 25 3ad2ant1 ⊢G∈W∧S∈U∧Vtx⁡S⊆Vtx⁡G∧Fun⁡iEdg⁡S∧Edg⁡S=∅→SSubGraphG↔Vtx⁡S⊆Vtx⁡G∧iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S∧Edg⁡S⊆𝒫Vtx⁡S
27 1 16 21 26 mpbir3and ⊢G∈W∧S∈U∧Vtx⁡S⊆Vtx⁡G∧Fun⁡iEdg⁡S∧Edg⁡S=∅→SSubGraphG