Metamath Proof Explorer


Theorem usgredgleordALT

Description: Alternate proof for usgredgleord based on usgriedgleord . In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020) (Proof shortened by AV, 5-May-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses usgredgleord.v 𝑉 = ( Vtx ‘ 𝐺 )
usgredgleord.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion usgredgleordALT ( ( 𝐺 ∈ USGraph ∧ 𝑁𝑉 ) → ( ♯ ‘ { 𝑒𝐸𝑁𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) )

Proof

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 ∧ 𝑁𝑉 ) → ( ♯ ‘ { 𝑒𝐸𝑁𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) )