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 )