# 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}=\mathrm{Vtx}\left({G}\right)$
upgr1e.a ${⊢}{\phi }\to {A}\in {X}$
upgr1e.b ${⊢}{\phi }\to {B}\in {V}$
upgr1e.c ${⊢}{\phi }\to {C}\in {V}$
upgr1e.e ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\right)=\left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}$
Assertion upgr1e ${⊢}{\phi }\to {G}\in \mathrm{UPGraph}$

### Proof

Step Hyp Ref Expression
1 upgr1e.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 upgr1e.a ${⊢}{\phi }\to {A}\in {X}$
3 upgr1e.b ${⊢}{\phi }\to {B}\in {V}$
4 upgr1e.c ${⊢}{\phi }\to {C}\in {V}$
5 upgr1e.e ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\right)=\left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}$
6 prex ${⊢}\left\{{B},{C}\right\}\in \mathrm{V}$
7 6 snid ${⊢}\left\{{B},{C}\right\}\in \left\{\left\{{B},{C}\right\}\right\}$
8 7 a1i ${⊢}{\phi }\to \left\{{B},{C}\right\}\in \left\{\left\{{B},{C}\right\}\right\}$
9 2 8 fsnd ${⊢}{\phi }\to \left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}:\left\{{A}\right\}⟶\left\{\left\{{B},{C}\right\}\right\}$
10 3 4 prssd ${⊢}{\phi }\to \left\{{B},{C}\right\}\subseteq {V}$
11 10 1 sseqtrdi ${⊢}{\phi }\to \left\{{B},{C}\right\}\subseteq \mathrm{Vtx}\left({G}\right)$
12 6 elpw ${⊢}\left\{{B},{C}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)↔\left\{{B},{C}\right\}\subseteq \mathrm{Vtx}\left({G}\right)$
13 11 12 sylibr ${⊢}{\phi }\to \left\{{B},{C}\right\}\in 𝒫\mathrm{Vtx}\left({G}\right)$
14 13 3 upgr1elem ${⊢}{\phi }\to \left\{\left\{{B},{C}\right\}\right\}\subseteq \left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
15 9 14 fssd ${⊢}{\phi }\to \left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}:\left\{{A}\right\}⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
16 15 ffdmd ${⊢}{\phi }\to \left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}:\mathrm{dom}\left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
17 5 dmeqd ${⊢}{\phi }\to \mathrm{dom}\mathrm{iEdg}\left({G}\right)=\mathrm{dom}\left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}$
18 5 17 feq12d ${⊢}{\phi }\to \left(\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}↔\left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}:\mathrm{dom}\left\{⟨{A},\left\{{B},{C}\right\}⟩\right\}⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\right)$
19 16 18 mpbird ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
20 1 1vgrex ${⊢}{B}\in {V}\to {G}\in \mathrm{V}$
21 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
22 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
23 21 22 isupgr ${⊢}{G}\in \mathrm{V}\to \left({G}\in \mathrm{UPGraph}↔\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\right)$
24 3 20 23 3syl ${⊢}{\phi }\to \left({G}\in \mathrm{UPGraph}↔\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\right)$
25 19 24 mpbird ${⊢}{\phi }\to {G}\in \mathrm{UPGraph}$