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

Metamath Proof Explorer

Theorem vtxdusgr0edgnelALT

Description: Alternate proof of vtxdusgr0edgnel , not based on vtxduhgr0edgnel . A vertex in a simple graph has degree 0 if there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdushgrfvedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
vtxdushgrfvedg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion vtxdusgr0edgnelALT ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdushgrfvedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 vtxdushgrfvedg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4 1 2 3 vtxdusgrfvedg ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) )
5 4 eqeq1d ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) = 0 ) )
6 fvex ⊢ ( Edg ‘ 𝐺 ) ∈ V
7 2 6 eqeltri ⊢ 𝐸 ∈ V
8 7 rabex ⊢ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ V
9 hasheq0 ⊢ ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ V → ( ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) = 0 ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } = ∅ ) )
10 8 9 mp1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) = 0 ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } = ∅ ) )
11 rabeq0 ⊢ ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } = ∅ ↔ ∀ 𝑒 ∈ 𝐸 ¬ 𝑈 ∈ 𝑒 )
12 ralnex ⊢ ( ∀ 𝑒 ∈ 𝐸 ¬ 𝑈 ∈ 𝑒 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 )
13 12 a1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ∀ 𝑒 ∈ 𝐸 ¬ 𝑈 ∈ 𝑒 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )
14 11 13 bitrid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } = ∅ ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )
15 5 10 14 3bitrd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )