Metamath Proof Explorer

Theorem edgupgr

Description: Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020)

Ref Expression
Assertion edgupgr ⊢G∈UPGraph∧E∈Edg⁡G→E∈𝒫Vtx⁡G∧E≠∅∧E≤2

Proof

Step Hyp Ref Expression
1 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
2 1 a1i ⊢G∈UPGraph→Edg⁡G=ran⁡iEdg⁡G
3 2 eleq2d ⊢G∈UPGraph→E∈Edg⁡G↔E∈ran⁡iEdg⁡G
4 eqid ⊢Vtx⁡G=Vtx⁡G
5 eqid ⊢iEdg⁡G=iEdg⁡G
6 4 5 upgrf ⊢G∈UPGraph→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
7 6 frnd ⊢G∈UPGraph→ran⁡iEdg⁡G⊆x∈𝒫Vtx⁡G∖∅|x≤2
8 7 sseld ⊢G∈UPGraph→E∈ran⁡iEdg⁡G→E∈x∈𝒫Vtx⁡G∖∅|x≤2
9 fveq2 ⊢x=E→x=E
10 9 breq1d ⊢x=E→x≤2↔E≤2
11 10 elrab ⊢E∈x∈𝒫Vtx⁡G∖∅|x≤2↔E∈𝒫Vtx⁡G∖∅∧E≤2
12 eldifsn ⊢E∈𝒫Vtx⁡G∖∅↔E∈𝒫Vtx⁡G∧E≠∅
13 12 biimpi ⊢E∈𝒫Vtx⁡G∖∅→E∈𝒫Vtx⁡G∧E≠∅
14 13 anim1i ⊢E∈𝒫Vtx⁡G∖∅∧E≤2→E∈𝒫Vtx⁡G∧E≠∅∧E≤2
15 df-3an ⊢E∈𝒫Vtx⁡G∧E≠∅∧E≤2↔E∈𝒫Vtx⁡G∧E≠∅∧E≤2
16 14 15 sylibr ⊢E∈𝒫Vtx⁡G∖∅∧E≤2→E∈𝒫Vtx⁡G∧E≠∅∧E≤2
17 16 a1i ⊢G∈UPGraph→E∈𝒫Vtx⁡G∖∅∧E≤2→E∈𝒫Vtx⁡G∧E≠∅∧E≤2
18 11 17 biimtrid ⊢G∈UPGraph→E∈x∈𝒫Vtx⁡G∖∅|x≤2→E∈𝒫Vtx⁡G∧E≠∅∧E≤2
19 8 18 syld ⊢G∈UPGraph→E∈ran⁡iEdg⁡G→E∈𝒫Vtx⁡G∧E≠∅∧E≤2
20 3 19 sylbid ⊢G∈UPGraph→E∈Edg⁡G→E∈𝒫Vtx⁡G∧E≠∅∧E≤2
21 20 imp ⊢G∈UPGraph∧E∈Edg⁡G→E∈𝒫Vtx⁡G∧E≠∅∧E≤2