This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( 𝑆 ∈ 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 𝐺 )