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	syl6bi	⊢ ( ( 𝑆 ∈ 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	syl5eq	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → ( Edg ‘ 𝑆 ) = ∅ )
20		egrsubgr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ) ∧ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( Fun ( iEdg ‘ 𝑆 ) ∧ ( Edg ‘ 𝑆 ) = ∅ ) ) → 𝑆 SubGraph 𝐺 )
21	1 5 8 19 20	syl112anc	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ ( Vtx ‘ 𝑆 ) = ∅ ) → 𝑆 SubGraph 𝐺 )