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 ⊢ G ∈ W ∧ S ∈ UHGraph ∧ Vtx ⁡ S = ∅ → S SubGraph G

Proof

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