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

Metamath Proof Explorer

Theorem usgrstrrepe

Description: Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a simple graph. Instead of requiring ( ph -> G Struct X ) , it would be sufficient to require ( ph -> Fun ( G \ { (/) } ) ) and ( ph -> G e. _V ) . (Contributed by AV, 13-Nov-2021) (Proof shortened by AV, 16-Nov-2021)

Ref Expression
Hypotheses usgrstrrepe.v 
|- V = ( Base ` G )
usgrstrrepe.i 
|- I = ( .ef ` ndx )
usgrstrrepe.s 
|- ( ph -> G Struct X )
usgrstrrepe.b 
|- ( ph -> ( Base ` ndx ) e. dom G )
usgrstrrepe.w 
|- ( ph -> E e. W )
usgrstrrepe.e 
|- ( ph -> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
Assertion usgrstrrepe 
|- ( ph -> ( G sSet <. I , E >. ) e. USGraph )

Proof

Step Hyp Ref Expression
1 usgrstrrepe.v 
 |-  V = ( Base ` G )
2 usgrstrrepe.i 
 |-  I = ( .ef ` ndx )
3 usgrstrrepe.s 
 |-  ( ph -> G Struct X )
4 usgrstrrepe.b 
 |-  ( ph -> ( Base ` ndx ) e. dom G )
5 usgrstrrepe.w 
 |-  ( ph -> E e. W )
6 usgrstrrepe.e 
 |-  ( ph -> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
7 2 3 4 5 setsvtx 
 |-  ( ph -> ( Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` G ) )
8 7 1 eqtr4di 
 |-  ( ph -> ( Vtx ` ( G sSet <. I , E >. ) ) = V )
9 8 pweqd 
 |-  ( ph -> ~P ( Vtx ` ( G sSet <. I , E >. ) ) = ~P V )
10 9 rabeqdv 
 |-  ( ph -> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 } )
11 f1eq3 
 |-  ( { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 } -> ( E : dom E -1-1-> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } <-> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
12 10 11 syl 
 |-  ( ph -> ( E : dom E -1-1-> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } <-> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
13 6 12 mpbird 
 |-  ( ph -> E : dom E -1-1-> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } )
14 2 3 4 5 setsiedg 
 |-  ( ph -> ( iEdg ` ( G sSet <. I , E >. ) ) = E )
15 14 dmeqd 
 |-  ( ph -> dom ( iEdg ` ( G sSet <. I , E >. ) ) = dom E )
16 eqidd 
 |-  ( ph -> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } = { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } )
17 14 15 16 f1eq123d 
 |-  ( ph -> ( ( iEdg ` ( G sSet <. I , E >. ) ) : dom ( iEdg ` ( G sSet <. I , E >. ) ) -1-1-> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } <-> E : dom E -1-1-> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } ) )
18 13 17 mpbird 
 |-  ( ph -> ( iEdg ` ( G sSet <. I , E >. ) ) : dom ( iEdg ` ( G sSet <. I , E >. ) ) -1-1-> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } )
19 ovex 
 |-  ( G sSet <. I , E >. ) e. _V
20 eqid 
 |-  ( Vtx ` ( G sSet <. I , E >. ) ) = ( Vtx ` ( G sSet <. I , E >. ) )
21 eqid 
 |-  ( iEdg ` ( G sSet <. I , E >. ) ) = ( iEdg ` ( G sSet <. I , E >. ) )
22 20 21 isusgrs 
 |-  ( ( G sSet <. I , E >. ) e. _V -> ( ( G sSet <. I , E >. ) e. USGraph <-> ( iEdg ` ( G sSet <. I , E >. ) ) : dom ( iEdg ` ( G sSet <. I , E >. ) ) -1-1-> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } ) )
23 19 22 mp1i 
 |-  ( ph -> ( ( G sSet <. I , E >. ) e. USGraph <-> ( iEdg ` ( G sSet <. I , E >. ) ) : dom ( iEdg ` ( G sSet <. I , E >. ) ) -1-1-> { x e. ~P ( Vtx ` ( G sSet <. I , E >. ) ) | ( # ` x ) = 2 } ) )
24 18 23 mpbird 
 |-  ( ph -> ( G sSet <. I , E >. ) e. USGraph )