Theorem usgredgreu

Description: For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

	Ref	Expression
Hypotheses	usgredg3.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	usgredg3.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	usgredgreu	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ ( 𝐸 ‘ 𝑋 ) ) → ∃! 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		usgredg3.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		usgredg3.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3	1 2	usgredg4	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ ( 𝐸 ‘ 𝑋 ) ) → ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } )
4		eqtr2	⊢ ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } ∧ ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑥 } ) → { 𝑌 , 𝑦 } = { 𝑌 , 𝑥 } )
5		vex	⊢ 𝑦 ∈ V
6		vex	⊢ 𝑥 ∈ V
7	5 6	preqr2	⊢ ( { 𝑌 , 𝑦 } = { 𝑌 , 𝑥 } → 𝑦 = 𝑥 )
8	4 7	syl	⊢ ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } ∧ ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑥 } ) → 𝑦 = 𝑥 )
9	8	a1i	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ ( 𝐸 ‘ 𝑋 ) ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } ∧ ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑥 } ) → 𝑦 = 𝑥 ) )
10	9	ralrimivva	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ ( 𝐸 ‘ 𝑋 ) ) → ∀ 𝑦 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } ∧ ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑥 } ) → 𝑦 = 𝑥 ) )
11		preq2	⊢ ( 𝑦 = 𝑥 → { 𝑌 , 𝑦 } = { 𝑌 , 𝑥 } )
12	11	eqeq2d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } ↔ ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑥 } ) )
13	12	reu4	⊢ ( ∃! 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } ↔ ( ∃ 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } ∧ ∀ 𝑦 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } ∧ ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑥 } ) → 𝑦 = 𝑥 ) ) )
14	3 10 13	sylanbrc	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ∧ 𝑌 ∈ ( 𝐸 ‘ 𝑋 ) ) → ∃! 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } )