Metamath Proof Explorer

Theorem 1hevtxdg0

Description: The vertex degree of vertex D in a graph G with only one hyperedge E is 0 if D is not incident with the edge E . (Contributed by AV, 2-Mar-2021)

Ref Expression
Hypotheses 1hevtxdg0.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
1hevtxdg0.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
1hevtxdg0.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
1hevtxdg0.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
1hevtxdg0.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑌 )
1hevtxdg0.n ⊢ ( 𝜑 → 𝐷 ∉ 𝐸 )
Assertion 1hevtxdg0 ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 )

Proof

Step Hyp Ref Expression
1 1hevtxdg0.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
2 1hevtxdg0.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
3 1hevtxdg0.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
4 1hevtxdg0.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5 1hevtxdg0.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑌 )
6 1hevtxdg0.n ⊢ ( 𝜑 → 𝐷 ∉ 𝐸 )
7 df-nel ⊢ ( 𝐷 ∉ 𝐸 ↔ ¬ 𝐷 ∈ 𝐸 )
8 6 7 sylib ⊢ ( 𝜑 → ¬ 𝐷 ∈ 𝐸 )
9 1 fveq1d ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) )
10 fvsng ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐸 )
11 3 5 10 syl2anc ⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐸 )
12 9 11 eqtrd ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) = 𝐸 )
13 8 12 neleqtrrd ⊢ ( 𝜑 → ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) )
14 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) )
15 14 eleq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
16 15 notbid ⊢ ( 𝑥 = 𝐴 → ( ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
17 16 ralsng ⊢ ( 𝐴 ∈ 𝑋 → ( ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
18 3 17 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
19 13 18 mpbird ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
20 1 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , 𝐸 ⟩ } )
21 dmsnopg ⊢ ( 𝐸 ∈ 𝑌 → dom { ⟨ 𝐴 , 𝐸 ⟩ } = { 𝐴 } )
22 5 21 syl ⊢ ( 𝜑 → dom { ⟨ 𝐴 , 𝐸 ⟩ } = { 𝐴 } )
23 20 22 eqtrd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } )
24 23 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
25 19 24 mpbird ⊢ ( 𝜑 → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
26 ralnex ⊢ ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
27 25 26 sylib ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
28 2 eleq2d ⊢ ( 𝜑 → ( 𝐷 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐷 ∈ 𝑉 ) )
29 4 28 mpbird ⊢ ( 𝜑 → 𝐷 ∈ ( Vtx ‘ 𝐺 ) )
30 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
31 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
32 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
33 30 31 32 vtxd0nedgb ⊢ ( 𝐷 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
34 29 33 syl ⊢ ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
35 27 34 mpbird ⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 )