Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdushgrfvedg.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
vtxdushgrfvedg.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
vtxdushgrfvedg.d |
⊢ 𝐷 = ( VtxDeg ‘ 𝐺 ) |
4 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
5 |
1 4 3
|
vtxd0nedgb |
⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) |
6 |
5
|
adantl |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) |
7 |
4 2
|
uhgrvtxedgiedgb |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) ) |
8 |
7
|
notbid |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) ) |
9 |
6 8
|
bitrd |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) ) |