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=ABC
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=ABC
6 prex ⊢BC∈V
7 6 snid ⊢BC∈BC
8 f1sng ⊢A∈X∧BC∈BC→ABC:A⟶1-1BC
9 2 7 8 sylancl ⊢φ→ABC:A⟶1-1BC
10 3 4 prssd ⊢φ→BC⊆V
11 10 1 sseqtrdi ⊢φ→BC⊆Vtx⁡G
12 6 elpw ⊢BC∈𝒫Vtx⁡G↔BC⊆Vtx⁡G
13 11 12 sylibr ⊢φ→BC∈𝒫Vtx⁡G
14 13 3 upgr1elem ⊢φ→BC⊆x∈𝒫Vtx⁡G∖∅|x≤2
15 f1ss ⊢ABC:A⟶1-1BC∧BC⊆x∈𝒫Vtx⁡G∖∅|x≤2→ABC:A⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
16 9 14 15 syl2anc ⊢φ→ABC:A⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
17 6 a1i ⊢φ→BC∈V
18 17 3 upgr1elem ⊢φ→BC⊆x∈V∖∅|x≤2
19 f1ss ⊢ABC:A⟶1-1BC∧BC⊆x∈V∖∅|x≤2→ABC:A⟶1-1x∈V∖∅|x≤2
20 9 18 19 syl2anc ⊢φ→ABC:A⟶1-1x∈V∖∅|x≤2
21 f1dm ⊢ABC:A⟶1-1x∈V∖∅|x≤2→dom⁡ABC=A
22 f1eq2 ⊢dom⁡ABC=A→ABC:dom⁡ABC⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2↔ABC:A⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
23 20 21 22 3syl ⊢φ→ABC:dom⁡ABC⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2↔ABC:A⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
24 16 23 mpbird ⊢φ→ABC:dom⁡ABC⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
25 5 dmeqd ⊢φ→dom⁡iEdg⁡G=dom⁡ABC
26 eqidd ⊢φ→x∈𝒫Vtx⁡G∖∅|x≤2=x∈𝒫Vtx⁡G∖∅|x≤2
27 5 25 26 f1eq123d ⊢φ→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2↔ABC:dom⁡ABC⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
28 24 27 mpbird ⊢φ→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫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-1x∈𝒫Vtx⁡G∖∅|x≤2
33 3 29 32 3syl ⊢φ→G∈USHGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
34 28 33 mpbird ⊢φ→G∈USHGraph