Step |
Hyp |
Ref |
Expression |
1 |
|
usgruhgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph ) |
2 |
|
uhgr0vb |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) ) |
3 |
1 2
|
syl5ib |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) = ∅ ) ) |
4 |
|
simpl |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ 𝑊 ) |
5 |
|
simpr |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ ) |
6 |
4 5
|
usgr0e |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph ) |
7 |
6
|
ex |
⊢ ( 𝐺 ∈ 𝑊 → ( ( iEdg ‘ 𝐺 ) = ∅ → 𝐺 ∈ USGraph ) ) |
8 |
7
|
adantr |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( iEdg ‘ 𝐺 ) = ∅ → 𝐺 ∈ USGraph ) ) |
9 |
3 8
|
impbid |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) ) |