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 φ G Struct X
uhgrstrrepe.b φ Base ndx dom G
uhgrstrrepe.w φ E W
uhgrstrrepe.e φ E : dom E 𝒫 V
Assertion uhgrstrrepe φ G sSet I E UHGraph

Proof

Step Hyp Ref Expression
1 uhgrstrrepe.v V = Base G
2 uhgrstrrepe.i I = ef ndx
3 uhgrstrrepe.s φ G Struct X
4 uhgrstrrepe.b φ Base ndx dom G
5 uhgrstrrepe.w φ E W
6 uhgrstrrepe.e φ E : dom E 𝒫 V
7 2 3 4 5 setsvtx φ Vtx G sSet I E = Base G
8 7 1 eqtr4di φ Vtx G sSet I E = V
9 8 pweqd φ 𝒫 Vtx G sSet I E = 𝒫 V
10 9 difeq1d φ 𝒫 Vtx G sSet I E = 𝒫 V
11 10 feq3d φ E : dom E 𝒫 Vtx G sSet I E E : dom E 𝒫 V
12 6 11 mpbird φ E : dom E 𝒫 Vtx G sSet I E
13 2 3 4 5 setsiedg φ iEdg G sSet I E = E
14 13 dmeqd φ dom iEdg G sSet I E = dom E
15 13 14 feq12d φ iEdg G sSet I E : dom iEdg G sSet I E 𝒫 Vtx G sSet I E E : dom E 𝒫 Vtx G sSet I E
16 12 15 mpbird φ iEdg G sSet I E : dom iEdg G sSet I E 𝒫 Vtx G sSet I E
17 ovex G sSet I 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 V G sSet I E UHGraph iEdg G sSet I E : dom iEdg G sSet I E 𝒫 Vtx G sSet I E
21 17 20 mp1i φ G sSet I E UHGraph iEdg G sSet I E : dom iEdg G sSet I E 𝒫 Vtx G sSet I E
22 16 21 mpbird φ G sSet I E UHGraph