This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nbgr0edglem

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

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

Proof

Step Hyp Ref Expression
1 nbgr0edglem.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 𝐾 ) = ∅ )