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 ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → 𝑆 SubGraph 𝐺 )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) )
2 eqid ⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
3 eqid ⊢ ( Edg ‘ 𝑆 ) = ( Edg ‘ 𝑆 )
4 2 3 edg0iedg0 ⊢ ( Fun ( iEdg ‘ 𝑆 ) → ( ( Edg ‘ 𝑆 ) = ∅ ↔ ( iEdg ‘ 𝑆 ) = ∅ ) )
5 4 adantl ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ Fun ( iEdg ‘ 𝑆 ) ) → ( ( Edg ‘ 𝑆 ) = ∅ ↔ ( iEdg ‘ 𝑆 ) = ∅ ) )
6 res0 ⊢ ( ( iEdg ‘ 𝐺 ) ↾ ∅ ) = ∅
7 6 eqcomi ⊢ ∅ = ( ( iEdg ‘ 𝐺 ) ↾ ∅ )
8 id ⊢ ( ( iEdg ‘ 𝑆 ) = ∅ → ( iEdg ‘ 𝑆 ) = ∅ )
9 dmeq ⊢ ( ( iEdg ‘ 𝑆 ) = ∅ → dom ( iEdg ‘ 𝑆 ) = dom ∅ )
10 dm0 ⊢ dom ∅ = ∅
11 9 10 eqtrdi ⊢ ( ( iEdg ‘ 𝑆 ) = ∅ → dom ( iEdg ‘ 𝑆 ) = ∅ )
12 11 reseq2d ⊢ ( ( iEdg ‘ 𝑆 ) = ∅ → ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) = ( ( iEdg ‘ 𝐺 ) ↾ ∅ ) )
13 7 8 12 3eqtr4a ⊢ ( ( iEdg ‘ 𝑆 ) = ∅ → ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) )
14 5 13 biimtrdi ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ Fun ( iEdg ‘ 𝑆 ) ) → ( ( Edg ‘ 𝑆 ) = ∅ → ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) ) )
15 14 impr ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) )
16 15 3adant2 ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) )
17 0ss ⊢ ∅ ⊆ 𝒫 ( Vtx ‘ 𝑆 )
18 sseq1 ⊢ ( ( Edg ‘ 𝑆 ) = ∅ → ( ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ↔ ∅ ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) )
19 17 18 mpbiri ⊢ ( ( Edg ‘ 𝑆 ) = ∅ → ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) )
20 19 adantl ⊢ ( ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) → ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) )
21 20 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) )
22 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
23 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
24 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
25 22 23 2 24 3 issubgr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) → ( 𝑆 SubGraph 𝐺 ↔ ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ) )
26 25 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → ( 𝑆 SubGraph 𝐺 ↔ ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ) )
27 1 16 21 26 mpbir3and ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → 𝑆 SubGraph 𝐺 )