Theorem nbgr0vtxlem

Description: Lemma for nbgr0vtx and nbgr0edg . (Contributed by AV, 15-Nov-2020)

	Ref	Expression
Hypothesis	nbgr0vtxlem.v	⊢ ( 𝜑 → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 )
Assertion	nbgr0vtxlem	⊢ ( 𝜑 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		nbgr0vtxlem.v	⊢ ( 𝜑 → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 )
2		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4	2 3	nbgrval	⊢ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝐾 ) = { 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 } )
5	4	ad2antrl	⊢ ( ( ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) ∧ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝜑 ) ) → ( 𝐺 NeighbVtx 𝐾 ) = { 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 } )
6	1	ad2antll	⊢ ( ( ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) ∧ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝜑 ) ) → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 )
7		rabeq0	⊢ ( { 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 } = ∅ ↔ ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 )
8	6 7	sylibr	⊢ ( ( ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) ∧ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝜑 ) ) → { 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 } = ∅ )
9	5 8	eqtrd	⊢ ( ( ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) ∧ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝜑 ) ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
10	9	expcom	⊢ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝜑 ) → ( ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) )
11	10	ex	⊢ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( 𝜑 → ( ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) ) )
12	11	com23	⊢ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) → ( 𝜑 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) ) )
13		df-nel	⊢ ( 𝐾 ∉ ( Vtx ‘ 𝐺 ) ↔ ¬ 𝐾 ∈ ( Vtx ‘ 𝐺 ) )
14	2	nbgrnvtx0	⊢ ( 𝐾 ∉ ( Vtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
15	13 14	sylbir	⊢ ( ¬ 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
16	15	a1d	⊢ ( ¬ 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( 𝜑 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) )
17		nbgrprc0	⊢ ( ¬ ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
18	17	a1d	⊢ ( ¬ ( 𝐺 ∈ V ∧ 𝐾 ∈ V ) → ( 𝜑 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) )
19	12 16 18	pm2.61nii	⊢ ( 𝜑 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )