Metamath Proof Explorer

Theorem upgredg

Description: For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020) (Proof shortened by AV, 26-Nov-2021)

Ref Expression
Hypotheses upgredg.v ⊢V=Vtx⁡G
upgredg.e ⊢E=Edg⁡G
Assertion upgredg ⊢G∈UPGraph∧C∈E→∃a∈V∃b∈VC=ab

Proof

Step Hyp Ref Expression
1 upgredg.v ⊢V=Vtx⁡G
2 upgredg.e ⊢E=Edg⁡G
3 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
4 3 a1i ⊢G∈UPGraph→Edg⁡G=ran⁡iEdg⁡G
5 2 4 eqtrid ⊢G∈UPGraph→E=ran⁡iEdg⁡G
6 5 eleq2d ⊢G∈UPGraph→C∈E↔C∈ran⁡iEdg⁡G
7 eqid ⊢iEdg⁡G=iEdg⁡G
8 1 7 upgrf ⊢G∈UPGraph→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫V∖∅|x≤2
9 8 frnd ⊢G∈UPGraph→ran⁡iEdg⁡G⊆x∈𝒫V∖∅|x≤2
10 9 sseld ⊢G∈UPGraph→C∈ran⁡iEdg⁡G→C∈x∈𝒫V∖∅|x≤2
11 6 10 sylbid ⊢G∈UPGraph→C∈E→C∈x∈𝒫V∖∅|x≤2
12 11 imp ⊢G∈UPGraph∧C∈E→C∈x∈𝒫V∖∅|x≤2
13 fveq2 ⊢x=C→x=C
14 13 breq1d ⊢x=C→x≤2↔C≤2
15 14 elrab ⊢C∈x∈𝒫V∖∅|x≤2↔C∈𝒫V∖∅∧C≤2
16 hashle2prv ⊢C∈𝒫V∖∅→C≤2↔∃a∈V∃b∈VC=ab
17 16 biimpa ⊢C∈𝒫V∖∅∧C≤2→∃a∈V∃b∈VC=ab
18 15 17 sylbi ⊢C∈x∈𝒫V∖∅|x≤2→∃a∈V∃b∈VC=ab
19 12 18 syl ⊢G∈UPGraph∧C∈E→∃a∈V∃b∈VC=ab