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 eqtrid ⊢ ( 𝑈 ∈ 𝑉 → ( 𝐷 ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑖 ∈ 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 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) )