Metamath Proof Explorer


Theorem 0uhgrsubgr

Description: The null graph (as hypergraph) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020) (Proof shortened by AV, 28-Nov-2020)

Ref Expression
Assertion 0uhgrsubgr ( ( 𝐺𝑊𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → 𝑆 SubGraph 𝐺 )

Proof

Step Hyp Ref Expression
1 3simpa ( ( 𝐺𝑊𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( 𝐺𝑊𝑆 ∈ UHGraph ) )
2 0ss ∅ ⊆ ( Vtx ‘ 𝐺 )
3 sseq1 ( ( Vtx ‘ 𝑆 ) = ∅ → ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ↔ ∅ ⊆ ( Vtx ‘ 𝐺 ) ) )
4 2 3 mpbiri ( ( Vtx ‘ 𝑆 ) = ∅ → ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) )
5 4 3ad2ant3 ( ( 𝐺𝑊𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) )
6 eqid ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
7 6 uhgrfun ( 𝑆 ∈ UHGraph → Fun ( iEdg ‘ 𝑆 ) )
8 7 3ad2ant2 ( ( 𝐺𝑊𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → Fun ( iEdg ‘ 𝑆 ) )
9 edgval ( Edg ‘ 𝑆 ) = ran ( iEdg ‘ 𝑆 )
10 uhgr0vb ( ( 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( 𝑆 ∈ UHGraph ↔ ( iEdg ‘ 𝑆 ) = ∅ ) )
11 rneq ( ( iEdg ‘ 𝑆 ) = ∅ → ran ( iEdg ‘ 𝑆 ) = ran ∅ )
12 rn0 ran ∅ = ∅
13 11 12 eqtrdi ( ( iEdg ‘ 𝑆 ) = ∅ → ran ( iEdg ‘ 𝑆 ) = ∅ )
14 10 13 syl6bi ( ( 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( 𝑆 ∈ UHGraph → ran ( iEdg ‘ 𝑆 ) = ∅ ) )
15 14 ex ( 𝑆 ∈ UHGraph → ( ( Vtx ‘ 𝑆 ) = ∅ → ( 𝑆 ∈ UHGraph → ran ( iEdg ‘ 𝑆 ) = ∅ ) ) )
16 15 pm2.43a ( 𝑆 ∈ UHGraph → ( ( Vtx ‘ 𝑆 ) = ∅ → ran ( iEdg ‘ 𝑆 ) = ∅ ) )
17 16 a1i ( 𝐺𝑊 → ( 𝑆 ∈ UHGraph → ( ( Vtx ‘ 𝑆 ) = ∅ → ran ( iEdg ‘ 𝑆 ) = ∅ ) ) )
18 17 3imp ( ( 𝐺𝑊𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ran ( iEdg ‘ 𝑆 ) = ∅ )
19 9 18 eqtrid ( ( 𝐺𝑊𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( Edg ‘ 𝑆 ) = ∅ )
20 egrsubgr ( ( ( 𝐺𝑊𝑆 ∈ UHGraph ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → 𝑆 SubGraph 𝐺 )
21 1 5 8 19 20 syl112anc ( ( 𝐺𝑊𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → 𝑆 SubGraph 𝐺 )