Metamath Proof Explorer


Theorem edgupgr

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

Ref Expression
Assertion edgupgr ( ( 𝐺 ∈ UPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) )

Proof

Step Hyp Ref Expression
1 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
2 1 a1i ( 𝐺 ∈ UPGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
3 2 eleq2d ( 𝐺 ∈ UPGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ 𝐸 ∈ ran ( iEdg ‘ 𝐺 ) ) )
4 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 4 5 upgrf ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
7 6 frnd ( 𝐺 ∈ UPGraph → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
8 7 sseld ( 𝐺 ∈ UPGraph → ( 𝐸 ∈ ran ( iEdg ‘ 𝐺 ) → 𝐸 ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
9 fveq2 ( 𝑥 = 𝐸 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐸 ) )
10 9 breq1d ( 𝑥 = 𝐸 → ( ( ♯ ‘ 𝑥 ) ≤ 2 ↔ ( ♯ ‘ 𝐸 ) ≤ 2 ) )
11 10 elrab ( 𝐸 ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ ( 𝐸 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) )
12 eldifsn ( 𝐸 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ) )
13 12 biimpi ( 𝐸 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ) )
14 13 anim1i ( ( 𝐸 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) → ( ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ) ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) )
15 df-3an ( ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) ↔ ( ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ) ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) )
16 14 15 sylibr ( ( 𝐸 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) → ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) )
17 16 a1i ( 𝐺 ∈ UPGraph → ( ( 𝐸 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) → ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) ) )
18 11 17 syl5bi ( 𝐺 ∈ UPGraph → ( 𝐸 ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) ) )
19 8 18 syld ( 𝐺 ∈ UPGraph → ( 𝐸 ∈ ran ( iEdg ‘ 𝐺 ) → ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) ) )
20 3 19 sylbid ( 𝐺 ∈ UPGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) → ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) ) )
21 20 imp ( ( 𝐺 ∈ UPGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐸 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝐸 ≠ ∅ ∧ ( ♯ ‘ 𝐸 ) ≤ 2 ) )