Theorem uhgrstrrepe

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

	Ref	Expression
Hypotheses	uhgrstrrepe.v	|- V = ( Base ` G )
	uhgrstrrepe.i	|- I = ( .ef ` ndx )
	uhgrstrrepe.s	|- ( ph -> G Struct X )
	uhgrstrrepe.b	|- ( ph -> ( Base ` ndx ) e. dom G )
	uhgrstrrepe.w	|- ( ph -> E e. W )
	uhgrstrrepe.e	|- ( ph -> E : dom E --> ( ~P V \ { (/) } ) )
Assertion	uhgrstrrepe	|- ( ph -> ( G sSet <. I , E >. ) e. UHGraph )

Proof

Step	Hyp	Ref	Expression
1		uhgrstrrepe.v	|- V = ( Base ` G )
2		uhgrstrrepe.i	|- I = ( .ef ` ndx )
3		uhgrstrrepe.s	|- ( ph -> G Struct X )
4		uhgrstrrepe.b	|- ( ph -> ( Base ` ndx ) e. dom G )
5		uhgrstrrepe.w	|- ( ph -> E e. W )
6		uhgrstrrepe.e	|- ( ph -> E : dom E --> ( ~P V \ { (/) } ) )
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	difeq1d	|- ( ph -> ( ~P ( Vtx ` ( G sSet <. I , E >. ) ) \ { (/) } ) = ( ~P V \ { (/) } ) )
11	10	feq3d	|- ( ph -> ( E : dom E --> ( ~P ( Vtx ` ( G sSet <. I , E >. ) ) \ { (/) } ) <-> E : dom E --> ( ~P V \ { (/) } ) ) )
12	6 11	mpbird	|- ( ph -> E : dom E --> ( ~P ( Vtx ` ( G sSet <. I , E >. ) ) \ { (/) } ) )
13	2 3 4 5	setsiedg	|- ( ph -> ( iEdg ` ( G sSet <. I , E >. ) ) = E )
14	13	dmeqd	|- ( ph -> dom ( iEdg ` ( G sSet <. I , E >. ) ) = dom E )
15	13 14	feq12d	|- ( ph -> ( ( iEdg ` ( G sSet <. I , E >. ) ) : dom ( iEdg ` ( G sSet <. I , E >. ) ) --> ( ~P ( Vtx ` ( G sSet <. I , E >. ) ) \ { (/) } ) <-> E : dom E --> ( ~P ( Vtx ` ( G sSet <. I , E >. ) ) \ { (/) } ) ) )
16	12 15	mpbird	|- ( ph -> ( iEdg ` ( G sSet <. I , E >. ) ) : dom ( iEdg ` ( G sSet <. I , E >. ) ) --> ( ~P ( Vtx ` ( G sSet <. I , E >. ) ) \ { (/) } ) )
17		ovex	|- ( G sSet <. I , E >. ) e. _V
18		eqid	|- ( Vtx ` ( G sSet <. I , E >. ) ) = ( Vtx ` ( G sSet <. I , E >. ) )
19		eqid	|- ( iEdg ` ( G sSet <. I , E >. ) ) = ( iEdg ` ( G sSet <. I , E >. ) )
20	18 19	isuhgr	|- ( ( G sSet <. I , E >. ) e. _V -> ( ( G sSet <. I , E >. ) e. UHGraph <-> ( iEdg ` ( G sSet <. I , E >. ) ) : dom ( iEdg ` ( G sSet <. I , E >. ) ) --> ( ~P ( Vtx ` ( G sSet <. I , E >. ) ) \ { (/) } ) ) )
21	17 20	mp1i	|- ( ph -> ( ( G sSet <. I , E >. ) e. UHGraph <-> ( iEdg ` ( G sSet <. I , E >. ) ) : dom ( iEdg ` ( G sSet <. I , E >. ) ) --> ( ~P ( Vtx ` ( G sSet <. I , E >. ) ) \ { (/) } ) ) )
22	16 21	mpbird	|- ( ph -> ( G sSet <. I , E >. ) e. UHGraph )