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

Metamath Proof Explorer

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 )