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	biimtrdi	|- ( ( 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	eqtrid	|- ( ( 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 )