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 e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> S SubGraph G )

Proof

Step Hyp Ref Expression
1 3simpa 
 |-  ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( G e. W /\ S e. UHGraph ) )
2 0ss 
 |-  (/) C_ ( Vtx ` G )
3 sseq1 
 |-  ( ( Vtx ` S ) = (/) -> ( ( Vtx ` S ) C_ ( Vtx ` G ) <-> (/) C_ ( Vtx ` G ) ) )
4 2 3 mpbiri 
 |-  ( ( Vtx ` S ) = (/) -> ( Vtx ` S ) C_ ( Vtx ` G ) )
5 4 3ad2ant3 
 |-  ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( Vtx ` S ) C_ ( Vtx ` G ) )
6 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
7 6 uhgrfun 
 |-  ( S e. UHGraph -> Fun ( iEdg ` S ) )
8 7 3ad2ant2 
 |-  ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> Fun ( iEdg ` S ) )
9 edgval 
 |-  ( Edg ` S ) = ran ( iEdg ` S )
10 uhgr0vb 
 |-  ( ( S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( S e. 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 e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( S e. UHGraph -> ran ( iEdg ` S ) = (/) ) )
15 14 ex 
 |-  ( S e. UHGraph -> ( ( Vtx ` S ) = (/) -> ( S e. UHGraph -> ran ( iEdg ` S ) = (/) ) ) )
16 15 pm2.43a 
 |-  ( S e. UHGraph -> ( ( Vtx ` S ) = (/) -> ran ( iEdg ` S ) = (/) ) )
17 16 a1i 
 |-  ( G e. W -> ( S e. UHGraph -> ( ( Vtx ` S ) = (/) -> ran ( iEdg ` S ) = (/) ) ) )
18 17 3imp 
 |-  ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ran ( iEdg ` S ) = (/) )
19 9 18 syl5eq 
 |-  ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> ( Edg ` S ) = (/) )
20 egrsubgr 
 |-  ( ( ( G e. W /\ S e. UHGraph ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( Fun ( iEdg ` S ) /\ ( Edg ` S ) = (/) ) ) -> S SubGraph G )
21 1 5 8 19 20 syl112anc 
 |-  ( ( G e. W /\ S e. UHGraph /\ ( Vtx ` S ) = (/) ) -> S SubGraph G )