Theorem nbgr0vtx

Description: In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020)

	Ref	Expression
Assertion	nbgr0vtx	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ral0	⊢ ∀ 𝑛 ∈ ∅ ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒
2		difeq1	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) = ( ∅ ∖ { 𝐾 } ) )
3		0dif	⊢ ( ∅ ∖ { 𝐾 } ) = ∅
4	2 3	eqtrdi	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) = ∅ )
5	4	raleqdv	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 ↔ ∀ 𝑛 ∈ ∅ ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 ) )
6	1 5	mpbiri	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 )
7	6	nbgr0vtxlem	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )