Step |
Hyp |
Ref |
Expression |
1 |
|
usgredgleord.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
usgredgleord.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
fvex |
⊢ ( iEdg ‘ 𝐺 ) ∈ V |
4 |
3
|
dmex |
⊢ dom ( iEdg ‘ 𝐺 ) ∈ V |
5 |
4
|
rabex |
⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ V |
6 |
5
|
a1i |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ V ) |
7 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
8 |
|
eqid |
⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } |
9 |
|
eleq2w |
⊢ ( 𝑒 = 𝑓 → ( 𝑁 ∈ 𝑒 ↔ 𝑁 ∈ 𝑓 ) ) |
10 |
9
|
cbvrabv |
⊢ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } = { 𝑓 ∈ 𝐸 ∣ 𝑁 ∈ 𝑓 } |
11 |
|
eqid |
⊢ ( 𝑦 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ) |
12 |
2 7 1 8 10 11
|
usgredgedg |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑦 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ↦ ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) |
13 |
6 12
|
hasheqf1od |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ) |
14 |
1 7
|
usgriedgleord |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) ≤ ( ♯ ‘ 𝑉 ) ) |
15 |
13 14
|
eqbrtrrd |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) ) |