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=∅→SSubGraphG

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 eqtrid ⊢G∈W∧S∈UHGraph∧Vtx⁡S=∅→Edg⁡S=∅
20 egrsubgr ⊢G∈W∧S∈UHGraph∧Vtx⁡S⊆Vtx⁡G∧Fun⁡iEdg⁡S∧Edg⁡S=∅→SSubGraphG
21 1 5 8 19 20 syl112anc ⊢G∈W∧S∈UHGraph∧Vtx⁡S=∅→SSubGraphG