Step |
Hyp |
Ref |
Expression |
1 |
|
usgredgffibi.I |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
2 |
|
usgredgffibi.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
edgval |
⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) |
4 |
1
|
eqcomi |
⊢ ( iEdg ‘ 𝐺 ) = 𝐼 |
5 |
4
|
rneqi |
⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼 |
6 |
2 3 5
|
3eqtri |
⊢ 𝐸 = ran 𝐼 |
7 |
6
|
eleq1i |
⊢ ( 𝐸 ∈ Fin ↔ ran 𝐼 ∈ Fin ) |
8 |
1
|
fvexi |
⊢ 𝐼 ∈ V |
9 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
10 |
9 1
|
usgrfs |
⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
11 |
|
f1vrnfibi |
⊢ ( ( 𝐼 ∈ V ∧ 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) → ( 𝐼 ∈ Fin ↔ ran 𝐼 ∈ Fin ) ) |
12 |
8 10 11
|
sylancr |
⊢ ( 𝐺 ∈ USGraph → ( 𝐼 ∈ Fin ↔ ran 𝐼 ∈ Fin ) ) |
13 |
7 12
|
bitr4id |
⊢ ( 𝐺 ∈ USGraph → ( 𝐸 ∈ Fin ↔ 𝐼 ∈ Fin ) ) |