This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uspgredgleord

Description: In a simple pseudograph 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, 6-Dec-2020)

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

Proof

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