Metamath Proof Explorer

Theorem 1hevtxdg1

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

Ref Expression
Hypotheses 1hevtxdg0.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
1hevtxdg0.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
1hevtxdg0.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
1hevtxdg0.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
1hevtxdg1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
1hevtxdg1.n ⊢ ( 𝜑 → 𝐷 ∈ 𝐸 )
1hevtxdg1.l ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐸 ) )
Assertion 1hevtxdg1 ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 1 )

Proof

Step Hyp Ref Expression
1 1hevtxdg0.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
2 1hevtxdg0.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
3 1hevtxdg0.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
4 1hevtxdg0.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5 1hevtxdg1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
6 1hevtxdg1.n ⊢ ( 𝜑 → 𝐷 ∈ 𝐸 )
7 1hevtxdg1.l ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐸 ) )
8 1 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , 𝐸 ⟩ } )
9 dmsnopg ⊢ ( 𝐸 ∈ 𝒫 𝑉 → dom { ⟨ 𝐴 , 𝐸 ⟩ } = { 𝐴 } )
10 5 9 syl ⊢ ( 𝜑 → dom { ⟨ 𝐴 , 𝐸 ⟩ } = { 𝐴 } )
11 8 10 eqtrd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } )
12 fveq2 ⊢ ( 𝑥 = 𝐸 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐸 ) )
13 12 breq2d ⊢ ( 𝑥 = 𝐸 → ( 2 ≤ ( ♯ ‘ 𝑥 ) ↔ 2 ≤ ( ♯ ‘ 𝐸 ) ) )
14 2 pweqd ⊢ ( 𝜑 → 𝒫 ( Vtx ‘ 𝐺 ) = 𝒫 𝑉 )
15 5 14 eleqtrrd ⊢ ( 𝜑 → 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
16 13 15 7 elrabd ⊢ ( 𝜑 → 𝐸 ∈ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
17 3 16 fsnd ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
18 17 adantr ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
19 1 adantr ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
20 simpr ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } )
21 19 20 feq12d ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ↔ { ⟨ 𝐴 , 𝐸 ⟩ } : { 𝐴 } ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
22 18 21 mpbird ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
23 4 2 eleqtrrd ⊢ ( 𝜑 → 𝐷 ∈ ( Vtx ‘ 𝐺 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → 𝐷 ∈ ( Vtx ‘ 𝐺 ) )
25 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
26 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
27 eqid ⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
28 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
29 25 26 27 28 vtxdlfgrval ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
30 22 24 29 syl2anc ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
31 rabeq ⊢ ( dom ( iEdg ‘ 𝐺 ) = { 𝐴 } → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑥 ∈ { 𝐴 } ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } )
32 31 adantl ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑥 ∈ { 𝐴 } ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } )
33 32 fveq2d ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
34 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) )
35 34 eleq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
36 35 rabsnif ⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) , { 𝐴 } , ∅ )
37 1 fveq1d ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) )
38 fvsng ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝒫 𝑉 ) → ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐸 )
39 3 5 38 syl2anc ⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐸 )
40 37 39 eqtrd ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) = 𝐸 )
41 6 40 eleqtrrd ⊢ ( 𝜑 → 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) )
42 41 iftrued ⊢ ( 𝜑 → if ( 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) , { 𝐴 } , ∅ ) = { 𝐴 } )
43 36 42 syl5eq ⊢ ( 𝜑 → { 𝑥 ∈ { 𝐴 } ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝐴 } )
44 43 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝐴 } ) )
45 hashsng ⊢ ( 𝐴 ∈ 𝑋 → ( ♯ ‘ { 𝐴 } ) = 1 )
46 3 45 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝐴 } ) = 1 )
47 44 46 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 )
48 47 adantr ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 )
49 30 33 48 3eqtrd ⊢ ( ( 𝜑 ∧ dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 1 )
50 11 49 mpdan ⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 1 )