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

Metamath Proof Explorer

Theorem usgrvd0nedg

Description: If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 16-Dec-2020) (Proof shortened by AV, 23-Dec-2020)

Ref Expression
Hypotheses vtxdusgradjvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdusgradjvtx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion usgrvd0nedg ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 vtxdusgradjvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdusgradjvtx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 vtxdusgradjvtx ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) )
4 3 eqeq1d ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 ↔ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) = 0 ) )
5 1 fvexi ⊢ 𝑉 ∈ V
6 5 rabex ⊢ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ∈ V
7 hasheq0 ⊢ ( { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ∈ V → ( ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) = 0 ↔ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } = ∅ ) )
8 6 7 ax-mp ⊢ ( ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) = 0 ↔ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } = ∅ )
9 rabeq0 ⊢ ( { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } = ∅ ↔ ∀ 𝑣 ∈ 𝑉 ¬ { 𝑈 , 𝑣 } ∈ 𝐸 )
10 ralnex ⊢ ( ∀ 𝑣 ∈ 𝑉 ¬ { 𝑈 , 𝑣 } ∈ 𝐸 ↔ ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )
11 10 biimpi ⊢ ( ∀ 𝑣 ∈ 𝑉 ¬ { 𝑈 , 𝑣 } ∈ 𝐸 → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )
12 11 a1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ∀ 𝑣 ∈ 𝑉 ¬ { 𝑈 , 𝑣 } ∈ 𝐸 → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )
13 9 12 biimtrid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } = ∅ → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )
14 8 13 biimtrid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) = 0 → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )
15 4 14 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )