Metamath Proof Explorer


Theorem vtxd0nedgb

Description: A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypotheses vtxd0nedgb.v 𝑉 = ( Vtx ‘ 𝐺 )
vtxd0nedgb.i 𝐼 = ( iEdg ‘ 𝐺 )
vtxd0nedgb.d 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion vtxd0nedgb ( 𝑈𝑉 → ( ( 𝐷𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼𝑖 ) ) )

Proof

Step Hyp Ref Expression
1 vtxd0nedgb.v 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxd0nedgb.i 𝐼 = ( iEdg ‘ 𝐺 )
3 vtxd0nedgb.d 𝐷 = ( VtxDeg ‘ 𝐺 )
4 3 fveq1i ( 𝐷𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 )
5 eqid dom 𝐼 = dom 𝐼
6 1 2 5 vtxdgval ( 𝑈𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ) )
7 4 6 syl5eq ( 𝑈𝑉 → ( 𝐷𝑈 ) = ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ) )
8 7 eqeq1d ( 𝑈𝑉 → ( ( 𝐷𝑈 ) = 0 ↔ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ) = 0 ) )
9 2 fvexi 𝐼 ∈ V
10 9 dmex dom 𝐼 ∈ V
11 10 rabex { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ∈ V
12 hashxnn0 ( { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ∈ V → ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) ∈ ℕ0* )
13 11 12 ax-mp ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) ∈ ℕ0*
14 10 rabex { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ∈ V
15 hashxnn0 ( { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ∈ V → ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ∈ ℕ0* )
16 14 15 ax-mp ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ∈ ℕ0*
17 13 16 pm3.2i ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) ∈ ℕ0* ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ∈ ℕ0* )
18 xnn0xadd0 ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) ∈ ℕ0* ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ∈ ℕ0* ) → ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ) = 0 ↔ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) = 0 ) ) )
19 17 18 mp1i ( 𝑈𝑉 → ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) ) = 0 ↔ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) = 0 ) ) )
20 hasheq0 ( { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ∈ V → ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) = 0 ↔ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } = ∅ ) )
21 11 20 ax-mp ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) = 0 ↔ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } = ∅ )
22 hasheq0 ( { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ∈ V → ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) = 0 ↔ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } = ∅ ) )
23 14 22 ax-mp ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) = 0 ↔ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } = ∅ )
24 21 23 anbi12i ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) = 0 ) ↔ ( { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } = ∅ ∧ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } = ∅ ) )
25 rabeq0 ( { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } = ∅ ↔ ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼𝑖 ) )
26 rabeq0 ( { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } = ∅ ↔ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼𝑖 ) = { 𝑈 } )
27 25 26 anbi12i ( ( { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } = ∅ ∧ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } = ∅ ) ↔ ( ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼𝑖 ) ∧ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼𝑖 ) = { 𝑈 } ) )
28 ralnex ( ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) )
29 28 bicomi ( ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) )
30 ioran ( ¬ ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ( ¬ 𝑈 ∈ ( 𝐼𝑖 ) ∧ ¬ ( 𝐼𝑖 ) = { 𝑈 } ) )
31 30 ralbii ( ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ∀ 𝑖 ∈ dom 𝐼 ( ¬ 𝑈 ∈ ( 𝐼𝑖 ) ∧ ¬ ( 𝐼𝑖 ) = { 𝑈 } ) )
32 r19.26 ( ∀ 𝑖 ∈ dom 𝐼 ( ¬ 𝑈 ∈ ( 𝐼𝑖 ) ∧ ¬ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ( ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼𝑖 ) ∧ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼𝑖 ) = { 𝑈 } ) )
33 29 31 32 3bitri ( ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ( ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼𝑖 ) ∧ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼𝑖 ) = { 𝑈 } ) )
34 33 bicomi ( ( ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼𝑖 ) ∧ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) )
35 24 27 34 3bitri ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) = 0 ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) )
36 orcom ( ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ( ( 𝐼𝑖 ) = { 𝑈 } ∨ 𝑈 ∈ ( 𝐼𝑖 ) ) )
37 snidg ( 𝑈𝑉𝑈 ∈ { 𝑈 } )
38 eleq2 ( ( 𝐼𝑖 ) = { 𝑈 } → ( 𝑈 ∈ ( 𝐼𝑖 ) ↔ 𝑈 ∈ { 𝑈 } ) )
39 37 38 syl5ibrcom ( 𝑈𝑉 → ( ( 𝐼𝑖 ) = { 𝑈 } → 𝑈 ∈ ( 𝐼𝑖 ) ) )
40 pm4.72 ( ( ( 𝐼𝑖 ) = { 𝑈 } → 𝑈 ∈ ( 𝐼𝑖 ) ) ↔ ( 𝑈 ∈ ( 𝐼𝑖 ) ↔ ( ( 𝐼𝑖 ) = { 𝑈 } ∨ 𝑈 ∈ ( 𝐼𝑖 ) ) ) )
41 39 40 sylib ( 𝑈𝑉 → ( 𝑈 ∈ ( 𝐼𝑖 ) ↔ ( ( 𝐼𝑖 ) = { 𝑈 } ∨ 𝑈 ∈ ( 𝐼𝑖 ) ) ) )
42 36 41 bitr4id ( 𝑈𝑉 → ( ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ 𝑈 ∈ ( 𝐼𝑖 ) ) )
43 42 rexbidv ( 𝑈𝑉 → ( ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼𝑖 ) ) )
44 43 notbid ( 𝑈𝑉 → ( ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼𝑖 ) ∨ ( 𝐼𝑖 ) = { 𝑈 } ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼𝑖 ) ) )
45 35 44 syl5bb ( 𝑈𝑉 → ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼𝑈 ∈ ( 𝐼𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼𝑖 ) = { 𝑈 } } ) = 0 ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼𝑖 ) ) )
46 8 19 45 3bitrd ( 𝑈𝑉 → ( ( 𝐷𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼𝑖 ) ) )