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 ‘ 𝐺 ) 𝐸 = { 𝑌 , 𝑦 } )