Theorem usgriedgleord

Description: Alternate version of usgredgleord , not using the notation ( EdgG ) . 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)

	Ref	Expression
Hypotheses	usgredg2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	usgredg2v.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	usgriedgleord	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ) ≤ ( ♯ ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		usgredg2v.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		usgredg2v.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3	1	fvexi	⊢ 𝑉 ∈ V
4		eqid	⊢ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } = { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) }
5		eqid	⊢ ( 𝑦 ∈ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ↦ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) ) = ( 𝑦 ∈ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ↦ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) )
6	1 2 4 5	usgredg2v	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑦 ∈ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ↦ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) ) : { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } –1-1→ 𝑉 )
7		f1domg	⊢ ( 𝑉 ∈ V → ( ( 𝑦 ∈ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ↦ ( ℩ 𝑧 ∈ 𝑉 ( 𝐸 ‘ 𝑦 ) = { 𝑧 , 𝑁 } ) ) : { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } –1-1→ 𝑉 → { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ≼ 𝑉 ) )
8	3 6 7	mpsyl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ≼ 𝑉 )
9		hashdomi	⊢ ( { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ≼ 𝑉 → ( ♯ ‘ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ) ≤ ( ♯ ‘ 𝑉 ) )
10	8 9	syl	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑥 ) } ) ≤ ( ♯ ‘ 𝑉 ) )