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

Metamath Proof Explorer

Theorem uspgredg2vtxeu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 6-Dec-2020)

Ref Expression
Assertion uspgredg2vtxeu ( ( 𝐺 ∈ USPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )

Proof

Step Hyp Ref Expression
1 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4 2 3 upgredg2vtx ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃ 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )
5 1 4 syl3an1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃ 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )
6 eqtr2 ⊢ ( ( 𝐸 = { 𝑌 , 𝑦 } ∧ 𝐸 = { 𝑌 , 𝑥 } ) → { 𝑌 , 𝑦 } = { 𝑌 , 𝑥 } )
7 vex ⊢ 𝑦 ∈ V
8 vex ⊢ 𝑥 ∈ V
9 7 8 preqr2 ⊢ ( { 𝑌 , 𝑦 } = { 𝑌 , 𝑥 } → 𝑦 = 𝑥 )
10 6 9 syl ⊢ ( ( 𝐸 = { 𝑌 , 𝑦 } ∧ 𝐸 = { 𝑌 , 𝑥 } ) → 𝑦 = 𝑥 )
11 10 a1i ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) ∧ ( 𝑦 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐸 = { 𝑌 , 𝑦 } ∧ 𝐸 = { 𝑌 , 𝑥 } ) → 𝑦 = 𝑥 ) )
12 11 ralrimivva ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∀ 𝑦 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ( ( 𝐸 = { 𝑌 , 𝑦 } ∧ 𝐸 = { 𝑌 , 𝑥 } ) → 𝑦 = 𝑥 ) )
13 preq2 ⊢ ( 𝑦 = 𝑥 → { 𝑌 , 𝑦 } = { 𝑌 , 𝑥 } )
14 13 eqeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐸 = { 𝑌 , 𝑦 } ↔ 𝐸 = { 𝑌 , 𝑥 } ) )
15 14 reu4 ⊢ ( ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ↔ ( ∃ 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } ∧ ∀ 𝑦 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑥 ∈ ( Vtx ‘ 𝐺 ) ( ( 𝐸 = { 𝑌 , 𝑦 } ∧ 𝐸 = { 𝑌 , 𝑥 } ) → 𝑦 = 𝑥 ) ) )
16 5 12 15 sylanbrc ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐸 ) → ∃! 𝑦 ∈ ( Vtx ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )