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