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 φ G Struct X
usgrstrrepe.b φ Base ndx dom G
usgrstrrepe.w φ E W
usgrstrrepe.e φ E : dom E 1-1 x 𝒫 V | x = 2
Assertion usgrstrrepe φ G sSet I E USGraph

Proof

Step Hyp Ref Expression
1 usgrstrrepe.v V = Base G
2 usgrstrrepe.i I = ef ndx
3 usgrstrrepe.s φ G Struct X
4 usgrstrrepe.b φ Base ndx dom G
5 usgrstrrepe.w φ E W
6 usgrstrrepe.e φ E : dom E 1-1 x 𝒫 V | x = 2
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 rabeqdv φ x 𝒫 Vtx G sSet I E | x = 2 = x 𝒫 V | x = 2
11 f1eq3 x 𝒫 Vtx G sSet I E | x = 2 = x 𝒫 V | x = 2 E : dom E 1-1 x 𝒫 Vtx G sSet I E | x = 2 E : dom E 1-1 x 𝒫 V | x = 2
12 10 11 syl φ E : dom E 1-1 x 𝒫 Vtx G sSet I E | x = 2 E : dom E 1-1 x 𝒫 V | x = 2
13 6 12 mpbird φ E : dom E 1-1 x 𝒫 Vtx G sSet I E | x = 2
14 2 3 4 5 setsiedg φ iEdg G sSet I E = E
15 14 dmeqd φ dom iEdg G sSet I E = dom E
16 eqidd φ x 𝒫 Vtx G sSet I E | x = 2 = x 𝒫 Vtx G sSet I E | x = 2
17 14 15 16 f1eq123d φ iEdg G sSet I E : dom iEdg G sSet I E 1-1 x 𝒫 Vtx G sSet I E | x = 2 E : dom E 1-1 x 𝒫 Vtx G sSet I E | x = 2
18 13 17 mpbird φ iEdg G sSet I E : dom iEdg G sSet I E 1-1 x 𝒫 Vtx G sSet I E | x = 2
19 ovex G sSet I 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 V G sSet I E USGraph iEdg G sSet I E : dom iEdg G sSet I E 1-1 x 𝒫 Vtx G sSet I E | x = 2
23 19 22 mp1i φ G sSet I E USGraph iEdg G sSet I E : dom iEdg G sSet I E 1-1 x 𝒫 Vtx G sSet I E | x = 2
24 18 23 mpbird φ G sSet I E USGraph