Step |
Hyp |
Ref |
Expression |
1 |
|
ausgr.1 |
⊢ 𝐺 = { 〈 𝑣 , 𝑒 〉 ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } } |
2 |
|
usgredgss |
⊢ ( 𝐻 ∈ USGraph → ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
3 |
|
fvex |
⊢ ( Vtx ‘ 𝐻 ) ∈ V |
4 |
|
fvex |
⊢ ( Edg ‘ 𝐻 ) ∈ V |
5 |
1
|
isausgr |
⊢ ( ( ( Vtx ‘ 𝐻 ) ∈ V ∧ ( Edg ‘ 𝐻 ) ∈ V ) → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
6 |
3 4 5
|
mp2an |
⊢ ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
7 |
2 6
|
sylibr |
⊢ ( 𝐻 ∈ USGraph → ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ) |