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 ⊢ V = Vtx ⁡ G
usgredg3.e ⊢ E = iEdg ⁡ G
Assertion usgredg3 ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → ∃ x ∈ V ∃ y ∈ V x ≠ y ∧ E ⁡ X = x y

Proof

Step Hyp Ref Expression
1 usgredg3.v ⊢ V = Vtx ⁡ G
2 usgredg3.e ⊢ E = iEdg ⁡ G
3 usgrfun ⊢ G ∈ USGraph → Fun ⁡ iEdg ⁡ G
4 2 funeqi ⊢ Fun ⁡ E ↔ Fun ⁡ iEdg ⁡ G
5 3 4 sylibr ⊢ G ∈ USGraph → Fun ⁡ E
6 fvelrn ⊢ Fun ⁡ E ∧ X ∈ dom ⁡ E → E ⁡ X ∈ ran ⁡ E
7 5 6 sylan ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X ∈ ran ⁡ E
8 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
9 8 a1i ⊢ G ∈ USGraph → Edg ⁡ G = ran ⁡ iEdg ⁡ G
10 2 eqcomi ⊢ iEdg ⁡ G = E
11 10 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ E
12 9 11 eqtrdi ⊢ G ∈ USGraph → Edg ⁡ G = ran ⁡ E
13 12 adantr ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → Edg ⁡ G = ran ⁡ E
14 7 13 eleqtrrd ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X ∈ Edg ⁡ G
15 eqid ⊢ Edg ⁡ G = Edg ⁡ G
16 1 15 usgredg ⊢ G ∈ USGraph ∧ E ⁡ X ∈ Edg ⁡ G → ∃ x ∈ V ∃ y ∈ V x ≠ y ∧ E ⁡ X = x y
17 14 16 syldan ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → ∃ x ∈ V ∃ y ∈ V x ≠ y ∧ E ⁡ X = x y