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

Metamath Proof Explorer

Theorem usgredg3

Description: The value of the "edge function" of a simple graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 17-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 usgredg3.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgredg3.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 usgrfun ⊢ ( 𝐺 ∈ USGraph → Fun ( iEdg ‘ 𝐺 ) )
4 2 funeqi ⊢ ( Fun 𝐸 ↔ Fun ( iEdg ‘ 𝐺 ) )
5 3 4 sylibr ⊢ ( 𝐺 ∈ USGraph → Fun 𝐸 )
6 fvelrn ⊢ ( ( Fun 𝐸 ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ∈ ran 𝐸 )
7 5 6 sylan ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ∈ ran 𝐸 )
8 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
9 8 a1i ⊢ ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
10 2 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐸
11 10 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐸
12 9 11 eqtrdi ⊢ ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ran 𝐸 )
13 12 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( Edg ‘ 𝐺 ) = ran 𝐸 )
14 7 13 eleqtrrd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ∈ ( Edg ‘ 𝐺 ) )
15 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
16 1 15 usgredg ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ ( 𝐸 ‘ 𝑋 ) = { 𝑥 , 𝑦 } ) )
17 14 16 syldan ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ ( 𝐸 ‘ 𝑋 ) = { 𝑥 , 𝑦 } ) )