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

Metamath Proof Explorer

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 𝐸 ∧ 𝑌 ∈ ( 𝐸 ‘ 𝑋 ) ) → ∃! 𝑦 ∈ 𝑉 ( 𝐸 ‘ 𝑋 ) = { 𝑌 , 𝑦 } )