Metamath Proof Explorer

Theorem upgr1e

Description: A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 16-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

Ref Expression
Hypotheses upgr1e.v ⊢V=Vtx⁡G
upgr1e.a ⊢φ→A∈X
upgr1e.b ⊢φ→B∈V
upgr1e.c ⊢φ→C∈V
upgr1e.e ⊢φ→iEdg⁡G=ABC
Assertion upgr1e ⊢φ→G∈UPGraph

Proof

Step Hyp Ref Expression
1 upgr1e.v ⊢V=Vtx⁡G
2 upgr1e.a ⊢φ→A∈X
3 upgr1e.b ⊢φ→B∈V
4 upgr1e.c ⊢φ→C∈V
5 upgr1e.e ⊢φ→iEdg⁡G=ABC
6 prex ⊢BC∈V
7 6 snid ⊢BC∈BC
8 7 a1i ⊢φ→BC∈BC
9 2 8 fsnd ⊢φ→ABC:A⟶BC
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 9 14 fssd ⊢φ→ABC:A⟶x∈𝒫Vtx⁡G∖∅|x≤2
16 15 ffdmd ⊢φ→ABC:dom⁡ABC⟶x∈𝒫Vtx⁡G∖∅|x≤2
17 5 dmeqd ⊢φ→dom⁡iEdg⁡G=dom⁡ABC
18 5 17 feq12d ⊢φ→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2↔ABC:dom⁡ABC⟶x∈𝒫Vtx⁡G∖∅|x≤2
19 16 18 mpbird ⊢φ→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
20 1 1vgrex ⊢B∈V→G∈V
21 eqid ⊢Vtx⁡G=Vtx⁡G
22 eqid ⊢iEdg⁡G=iEdg⁡G
23 21 22 isupgr ⊢G∈V→G∈UPGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
24 3 20 23 3syl ⊢φ→G∈UPGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
25 19 24 mpbird ⊢φ→G∈UPGraph