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