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 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )