# Metamath Proof Explorer

## Theorem umgrreslem

Description: Lemma for umgrres and usgrres . (Contributed by AV, 27-Nov-2020) (Revised by AV, 19-Dec-2021)

Ref Expression
Hypotheses upgrres.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
upgrres.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
upgrres.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{E}|{N}\notin {E}\left({i}\right)\right\}$
Assertion umgrreslem ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$

### Proof

Step Hyp Ref Expression
1 upgrres.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 upgrres.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 upgrres.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{E}|{N}\notin {E}\left({i}\right)\right\}$
4 df-ima ${⊢}{E}\left[{F}\right]=\mathrm{ran}\left({{E}↾}_{{F}}\right)$
5 fveq2 ${⊢}{i}={j}\to {E}\left({i}\right)={E}\left({j}\right)$
6 neleq2 ${⊢}{E}\left({i}\right)={E}\left({j}\right)\to \left({N}\notin {E}\left({i}\right)↔{N}\notin {E}\left({j}\right)\right)$
7 5 6 syl ${⊢}{i}={j}\to \left({N}\notin {E}\left({i}\right)↔{N}\notin {E}\left({j}\right)\right)$
8 7 3 elrab2 ${⊢}{j}\in {F}↔\left({j}\in \mathrm{dom}{E}\wedge {N}\notin {E}\left({j}\right)\right)$
9 1 2 umgrf ${⊢}{G}\in \mathrm{UMGraph}\to {E}:\mathrm{dom}{E}⟶\left\{{p}\in 𝒫{V}|\left|{p}\right|=2\right\}$
10 ffvelrn ${⊢}\left({E}:\mathrm{dom}{E}⟶\left\{{p}\in 𝒫{V}|\left|{p}\right|=2\right\}\wedge {j}\in \mathrm{dom}{E}\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫{V}|\left|{p}\right|=2\right\}$
11 fveqeq2 ${⊢}{p}={E}\left({j}\right)\to \left(\left|{p}\right|=2↔\left|{E}\left({j}\right)\right|=2\right)$
12 11 elrab ${⊢}{E}\left({j}\right)\in \left\{{p}\in 𝒫{V}|\left|{p}\right|=2\right\}↔\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)$
13 simpll ${⊢}\left(\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in 𝒫{V}$
14 elpwi ${⊢}{E}\left({j}\right)\in 𝒫{V}\to {E}\left({j}\right)\subseteq {V}$
15 14 adantr ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\to {E}\left({j}\right)\subseteq {V}$
16 15 adantr ${⊢}\left(\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\subseteq {V}$
17 simpr ${⊢}\left(\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {N}\notin {E}\left({j}\right)$
18 elpwdifsn ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge {E}\left({j}\right)\subseteq {V}\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)$
19 13 16 17 18 syl3anc ${⊢}\left(\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)$
20 simpr ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\to \left|{E}\left({j}\right)\right|=2$
21 20 adantr ${⊢}\left(\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to \left|{E}\left({j}\right)\right|=2$
22 11 19 21 elrabd ${⊢}\left(\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
23 22 ex ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
24 23 a1d ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge \left|{E}\left({j}\right)\right|=2\right)\to \left({N}\in {V}\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)\right)$
25 12 24 sylbi ${⊢}{E}\left({j}\right)\in \left\{{p}\in 𝒫{V}|\left|{p}\right|=2\right\}\to \left({N}\in {V}\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)\right)$
26 10 25 syl ${⊢}\left({E}:\mathrm{dom}{E}⟶\left\{{p}\in 𝒫{V}|\left|{p}\right|=2\right\}\wedge {j}\in \mathrm{dom}{E}\right)\to \left({N}\in {V}\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)\right)$
27 26 ex ${⊢}{E}:\mathrm{dom}{E}⟶\left\{{p}\in 𝒫{V}|\left|{p}\right|=2\right\}\to \left({j}\in \mathrm{dom}{E}\to \left({N}\in {V}\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)\right)\right)$
28 27 com23 ${⊢}{E}:\mathrm{dom}{E}⟶\left\{{p}\in 𝒫{V}|\left|{p}\right|=2\right\}\to \left({N}\in {V}\to \left({j}\in \mathrm{dom}{E}\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)\right)\right)$
29 9 28 syl ${⊢}{G}\in \mathrm{UMGraph}\to \left({N}\in {V}\to \left({j}\in \mathrm{dom}{E}\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)\right)\right)$
30 29 imp4b ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \left(\left({j}\in \mathrm{dom}{E}\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
31 8 30 syl5bi ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \left({j}\in {F}\to {E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
32 31 ralrimiv ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \forall {j}\in {F}\phantom{\rule{.4em}{0ex}}{E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
33 umgruhgr ${⊢}{G}\in \mathrm{UMGraph}\to {G}\in \mathrm{UHGraph}$
34 2 uhgrfun ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{Fun}{E}$
35 33 34 syl ${⊢}{G}\in \mathrm{UMGraph}\to \mathrm{Fun}{E}$
36 35 adantr ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \mathrm{Fun}{E}$
37 3 ssrab3 ${⊢}{F}\subseteq \mathrm{dom}{E}$
38 funimass4 ${⊢}\left(\mathrm{Fun}{E}\wedge {F}\subseteq \mathrm{dom}{E}\right)\to \left({E}\left[{F}\right]\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}↔\forall {j}\in {F}\phantom{\rule{.4em}{0ex}}{E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
39 36 37 38 sylancl ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \left({E}\left[{F}\right]\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}↔\forall {j}\in {F}\phantom{\rule{.4em}{0ex}}{E}\left({j}\right)\in \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
40 32 39 mpbird ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to {E}\left[{F}\right]\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
41 4 40 eqsstrrid ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$