Metamath Proof Explorer

Theorem upgrop

Description: A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021)

Ref Expression
Assertion upgrop ⊢G∈UPGraph→Vtx⁡GiEdg⁡G∈UPGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢iEdg⁡G=iEdg⁡G
3 1 2 upgrf ⊢G∈UPGraph→iEdg⁡G:dom⁡iEdg⁡G⟶p∈𝒫Vtx⁡G∖∅|p≤2
4 fvex ⊢Vtx⁡G∈V
5 fvex ⊢iEdg⁡G∈V
6 4 5 pm3.2i ⊢Vtx⁡G∈V∧iEdg⁡G∈V
7 opex ⊢Vtx⁡GiEdg⁡G∈V
8 eqid ⊢Vtx⁡Vtx⁡GiEdg⁡G=Vtx⁡Vtx⁡GiEdg⁡G
9 eqid ⊢iEdg⁡Vtx⁡GiEdg⁡G=iEdg⁡Vtx⁡GiEdg⁡G
10 8 9 isupgr ⊢Vtx⁡GiEdg⁡G∈V→Vtx⁡GiEdg⁡G∈UPGraph↔iEdg⁡Vtx⁡GiEdg⁡G:dom⁡iEdg⁡Vtx⁡GiEdg⁡G⟶p∈𝒫Vtx⁡Vtx⁡GiEdg⁡G∖∅|p≤2
11 7 10 mp1i ⊢Vtx⁡G∈V∧iEdg⁡G∈V→Vtx⁡GiEdg⁡G∈UPGraph↔iEdg⁡Vtx⁡GiEdg⁡G:dom⁡iEdg⁡Vtx⁡GiEdg⁡G⟶p∈𝒫Vtx⁡Vtx⁡GiEdg⁡G∖∅|p≤2
12 opiedgfv ⊢Vtx⁡G∈V∧iEdg⁡G∈V→iEdg⁡Vtx⁡GiEdg⁡G=iEdg⁡G
13 12 dmeqd ⊢Vtx⁡G∈V∧iEdg⁡G∈V→dom⁡iEdg⁡Vtx⁡GiEdg⁡G=dom⁡iEdg⁡G
14 opvtxfv ⊢Vtx⁡G∈V∧iEdg⁡G∈V→Vtx⁡Vtx⁡GiEdg⁡G=Vtx⁡G
15 14 pweqd ⊢Vtx⁡G∈V∧iEdg⁡G∈V→𝒫Vtx⁡Vtx⁡GiEdg⁡G=𝒫Vtx⁡G
16 15 difeq1d ⊢Vtx⁡G∈V∧iEdg⁡G∈V→𝒫Vtx⁡Vtx⁡GiEdg⁡G∖∅=𝒫Vtx⁡G∖∅
17 16 rabeqdv ⊢Vtx⁡G∈V∧iEdg⁡G∈V→p∈𝒫Vtx⁡Vtx⁡GiEdg⁡G∖∅|p≤2=p∈𝒫Vtx⁡G∖∅|p≤2
18 12 13 17 feq123d ⊢Vtx⁡G∈V∧iEdg⁡G∈V→iEdg⁡Vtx⁡GiEdg⁡G:dom⁡iEdg⁡Vtx⁡GiEdg⁡G⟶p∈𝒫Vtx⁡Vtx⁡GiEdg⁡G∖∅|p≤2↔iEdg⁡G:dom⁡iEdg⁡G⟶p∈𝒫Vtx⁡G∖∅|p≤2
19 11 18 bitrd ⊢Vtx⁡G∈V∧iEdg⁡G∈V→Vtx⁡GiEdg⁡G∈UPGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶p∈𝒫Vtx⁡G∖∅|p≤2
20 6 19 mp1i ⊢G∈UPGraph→Vtx⁡GiEdg⁡G∈UPGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶p∈𝒫Vtx⁡G∖∅|p≤2
21 3 20 mpbird ⊢G∈UPGraph→Vtx⁡GiEdg⁡G∈UPGraph