Metamath Proof Explorer

Theorem isupgr

Description: The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v 
|- V = ( Vtx ` G )
isupgr.e 
|- E = ( iEdg ` G )
Assertion isupgr 
|- ( G e. U -> ( G e. UPGraph <-> E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )

Proof

Step Hyp Ref Expression
1 isupgr.v 
 |-  V = ( Vtx ` G )
2 isupgr.e 
 |-  E = ( iEdg ` G )
3 df-upgr 
 |-  UPGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }
4 3 eleq2i 
 |-  ( G e. UPGraph <-> G e. { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } } )
5 fveq2 
 |-  ( h = G -> ( iEdg ` h ) = ( iEdg ` G ) )
6 5 2 eqtr4di 
 |-  ( h = G -> ( iEdg ` h ) = E )
7 5 dmeqd 
 |-  ( h = G -> dom ( iEdg ` h ) = dom ( iEdg ` G ) )
8 2 eqcomi 
 |-  ( iEdg ` G ) = E
9 8 dmeqi 
 |-  dom ( iEdg ` G ) = dom E
10 7 9 eqtrdi 
 |-  ( h = G -> dom ( iEdg ` h ) = dom E )
11 fveq2 
 |-  ( h = G -> ( Vtx ` h ) = ( Vtx ` G ) )
12 11 1 eqtr4di 
 |-  ( h = G -> ( Vtx ` h ) = V )
13 12 pweqd 
 |-  ( h = G -> ~P ( Vtx ` h ) = ~P V )
14 13 difeq1d 
 |-  ( h = G -> ( ~P ( Vtx ` h ) \ { (/) } ) = ( ~P V \ { (/) } ) )
15 14 rabeqdv 
 |-  ( h = G -> { x e. ( ~P ( Vtx ` h ) \ { (/) } ) | ( # ` x ) <_ 2 } = { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
16 6 10 15 feq123d 
 |-  ( h = G -> ( ( iEdg ` h ) : dom ( iEdg ` h ) --> { x e. ( ~P ( Vtx ` h ) \ { (/) } ) | ( # ` x ) <_ 2 } <-> E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
17 fvexd 
 |-  ( g = h -> ( Vtx ` g ) e. _V )
18 fveq2 
 |-  ( g = h -> ( Vtx ` g ) = ( Vtx ` h ) )
19 fvexd 
 |-  ( ( g = h /\ v = ( Vtx ` h ) ) -> ( iEdg ` g ) e. _V )
20 fveq2 
 |-  ( g = h -> ( iEdg ` g ) = ( iEdg ` h ) )
21 20 adantr 
 |-  ( ( g = h /\ v = ( Vtx ` h ) ) -> ( iEdg ` g ) = ( iEdg ` h ) )
22 simpr 
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> e = ( iEdg ` h ) )
23 22 dmeqd 
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> dom e = dom ( iEdg ` h ) )
24 pweq 
 |-  ( v = ( Vtx ` h ) -> ~P v = ~P ( Vtx ` h ) )
25 24 ad2antlr 
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> ~P v = ~P ( Vtx ` h ) )
26 25 difeq1d 
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> ( ~P v \ { (/) } ) = ( ~P ( Vtx ` h ) \ { (/) } ) )
27 26 rabeqdv 
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } = { x e. ( ~P ( Vtx ` h ) \ { (/) } ) | ( # ` x ) <_ 2 } )
28 22 23 27 feq123d 
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> ( e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( iEdg ` h ) : dom ( iEdg ` h ) --> { x e. ( ~P ( Vtx ` h ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
29 19 21 28 sbcied2 
 |-  ( ( g = h /\ v = ( Vtx ` h ) ) -> ( [. ( iEdg ` g ) / e ]. e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( iEdg ` h ) : dom ( iEdg ` h ) --> { x e. ( ~P ( Vtx ` h ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
30 17 18 29 sbcied2 
 |-  ( g = h -> ( [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( iEdg ` h ) : dom ( iEdg ` h ) --> { x e. ( ~P ( Vtx ` h ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
31 30 cbvabv 
 |-  { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } } = { h | ( iEdg ` h ) : dom ( iEdg ` h ) --> { x e. ( ~P ( Vtx ` h ) \ { (/) } ) | ( # ` x ) <_ 2 } }
32 16 31 elab2g 
 |-  ( G e. U -> ( G e. { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } } <-> E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
33 4 32 syl5bb 
 |-  ( G e. U -> ( G e. UPGraph <-> E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )