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 biimtrid ⊢ ( 𝐺 ∈ 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 ) )