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