This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgrop

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

Ref Expression
Assertion upgrop 
|- ( G e. UPGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. UPGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 upgrf 
 |-  ( G e. UPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { p e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` p ) <_ 2 } )
4 fvex 
 |-  ( Vtx ` G ) e. _V
5 fvex 
 |-  ( iEdg ` G ) e. _V
6 4 5 pm3.2i 
 |-  ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V )
7 opex 
 |-  <. ( Vtx ` G ) , ( iEdg ` G ) >. e. _V
8 eqid 
 |-  ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. )
9 eqid 
 |-  ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. )
10 8 9 isupgr 
 |-  ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. _V -> ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. UPGraph <-> ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) : dom ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) --> { p e. ( ~P ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
11 7 10 mp1i 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. UPGraph <-> ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) : dom ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) --> { p e. ( ~P ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
12 opiedgfv 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( iEdg ` G ) )
13 12 dmeqd 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> dom ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = dom ( iEdg ` G ) )
14 opvtxfv 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( Vtx ` G ) )
15 14 pweqd 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ~P ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ~P ( Vtx ` G ) )
16 15 difeq1d 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( ~P ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) \ { (/) } ) = ( ~P ( Vtx ` G ) \ { (/) } ) )
17 16 rabeqdv 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> { p e. ( ~P ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) \ { (/) } ) | ( # ` p ) <_ 2 } = { p e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` p ) <_ 2 } )
18 12 13 17 feq123d 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) : dom ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) --> { p e. ( ~P ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) \ { (/) } ) | ( # ` p ) <_ 2 } <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { p e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
19 11 18 bitrd 
 |-  ( ( ( Vtx ` G ) e. _V /\ ( iEdg ` G ) e. _V ) -> ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { p e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
20 6 19 mp1i 
 |-  ( G e. UPGraph -> ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { p e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
21 3 20 mpbird 
 |-  ( G e. UPGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. UPGraph )