Metamath Proof Explorer


Theorem uspgr1e

Description: A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

Ref Expression
Hypotheses uspgr1e.v V = Vtx G
uspgr1e.a φ A X
uspgr1e.b φ B V
uspgr1e.c φ C V
uspgr1e.e φ iEdg G = A B C
Assertion uspgr1e φ G USHGraph

Proof

Step Hyp Ref Expression
1 uspgr1e.v V = Vtx G
2 uspgr1e.a φ A X
3 uspgr1e.b φ B V
4 uspgr1e.c φ C V
5 uspgr1e.e φ iEdg G = A B C
6 prex B C V
7 6 snid B C B C
8 f1sng A X B C B C A B C : A 1-1 B C
9 2 7 8 sylancl φ A B C : A 1-1 B C
10 3 4 prssd φ B C V
11 10 1 sseqtrdi φ B C Vtx G
12 6 elpw B C 𝒫 Vtx G B C Vtx G
13 11 12 sylibr φ B C 𝒫 Vtx G
14 13 3 upgr1elem φ B C x 𝒫 Vtx G | x 2
15 f1ss A B C : A 1-1 B C B C x 𝒫 Vtx G | x 2 A B C : A 1-1 x 𝒫 Vtx G | x 2
16 9 14 15 syl2anc φ A B C : A 1-1 x 𝒫 Vtx G | x 2
17 6 a1i φ B C V
18 17 3 upgr1elem φ B C x V | x 2
19 f1ss A B C : A 1-1 B C B C x V | x 2 A B C : A 1-1 x V | x 2
20 9 18 19 syl2anc φ A B C : A 1-1 x V | x 2
21 f1dm A B C : A 1-1 x V | x 2 dom A B C = A
22 f1eq2 dom A B C = A A B C : dom A B C 1-1 x 𝒫 Vtx G | x 2 A B C : A 1-1 x 𝒫 Vtx G | x 2
23 20 21 22 3syl φ A B C : dom A B C 1-1 x 𝒫 Vtx G | x 2 A B C : A 1-1 x 𝒫 Vtx G | x 2
24 16 23 mpbird φ A B C : dom A B C 1-1 x 𝒫 Vtx G | x 2
25 5 dmeqd φ dom iEdg G = dom A B C
26 eqidd φ x 𝒫 Vtx G | x 2 = x 𝒫 Vtx G | x 2
27 5 25 26 f1eq123d φ iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2 A B C : dom A B C 1-1 x 𝒫 Vtx G | x 2
28 24 27 mpbird φ iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2
29 1 1vgrex B V G V
30 eqid Vtx G = Vtx G
31 eqid iEdg G = iEdg G
32 30 31 isuspgr G V G USHGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2
33 3 29 32 3syl φ G USHGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2
34 28 33 mpbird φ G USHGraph