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	syl5bi	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } = ∅ → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )
14	8 13	syl5bi	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ { 𝑈 , 𝑣 } ∈ 𝐸 } ) = 0 → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )
15	4 14	sylbid	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = 0 → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )