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

Metamath Proof Explorer

Theorem edgusgrnbfin

Description: The number of neighbors of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 28-Oct-2020)

Ref Expression
Hypotheses nbusgrf1o.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbusgrf1o.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion edgusgrnbfin ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 nbusgrf1o.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbusgrf1o.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 nbusgrf1o ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )
4 f1ofo ⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )
5 fofi ⊢ ( ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ∧ 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin )
6 5 expcom ⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
7 4 6 syl ⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
8 7 exlimiv ⊢ ( ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
9 3 8 syl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )
10 f1of1 ⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } )
11 f1fi ⊢ ( ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ∧ 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ) → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin )
12 11 expcom ⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
13 10 12 syl ⊢ ( 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
14 13 exlimiv ⊢ ( ∃ 𝑓 𝑓 : ( 𝐺 NeighbVtx 𝑈 ) –1-1-onto→ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
15 3 14 syl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) )
16 9 15 impbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ↔ { 𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒 } ∈ Fin ) )