Step |
Hyp |
Ref |
Expression |
1 |
|
upgruhgr |
⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph ) |
2 |
1
|
anim1ci |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph ) → ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) ) |
3 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
4 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
5 |
3 4
|
acycgrislfgr |
⊢ ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) |
6 |
2 5
|
syl |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) |
7 |
3 4
|
umgrislfupgr |
⊢ ( 𝐺 ∈ UMGraph ↔ ( 𝐺 ∈ UPGraph ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ) |
8 |
7
|
biimpri |
⊢ ( ( 𝐺 ∈ UPGraph ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐺 ∈ UMGraph ) |
9 |
6 8
|
syldan |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph ) → 𝐺 ∈ UMGraph ) |