Step |
Hyp |
Ref |
Expression |
1 |
|
uspgrupgr |
⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph ) |
2 |
|
uspgrushgr |
⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph ) |
3 |
1 2
|
jca |
⊢ ( 𝐺 ∈ USPGraph → ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) ) |
4 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
5 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
6 |
4 5
|
ushgrf |
⊢ ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) |
7 |
|
edgval |
⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) |
8 |
|
upgredgss |
⊢ ( 𝐺 ∈ UPGraph → ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
9 |
7 8
|
eqsstrrid |
⊢ ( 𝐺 ∈ UPGraph → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
10 |
|
f1ssr |
⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
11 |
6 9 10
|
syl2anr |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
12 |
4 5
|
isuspgr |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐺 ∈ USPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) → ( 𝐺 ∈ USPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
14 |
11 13
|
mpbird |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) → 𝐺 ∈ USPGraph ) |
15 |
3 14
|
impbii |
⊢ ( 𝐺 ∈ USPGraph ↔ ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) ) |