# Metamath Proof Explorer

## Theorem upgrreslem

Description: Lemma for upgrres . (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 upgrreslem ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {N}\in {V}\right)\to \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 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 upgrf ${⊢}{G}\in \mathrm{UPGraph}\to {E}:\mathrm{dom}{E}⟶\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$
10 ffvelrn ${⊢}\left({E}:\mathrm{dom}{E}⟶\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\wedge {j}\in \mathrm{dom}{E}\right)\to {E}\left({j}\right)\in \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$
11 fveq2 ${⊢}{p}={E}\left({j}\right)\to \left|{p}\right|=\left|{E}\left({j}\right)\right|$
12 11 breq1d ${⊢}{p}={E}\left({j}\right)\to \left(\left|{p}\right|\le 2↔\left|{E}\left({j}\right)\right|\le 2\right)$
13 12 elrab ${⊢}{E}\left({j}\right)\in \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}↔\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)$
14 eldifsn ${⊢}{E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)↔\left({E}\left({j}\right)\in 𝒫{V}\wedge {E}\left({j}\right)\ne \varnothing \right)$
15 simpl ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in 𝒫{V}$
16 elpwi ${⊢}{E}\left({j}\right)\in 𝒫{V}\to {E}\left({j}\right)\subseteq {V}$
17 16 adantr ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\subseteq {V}$
18 simpr ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge {N}\notin {E}\left({j}\right)\right)\to {N}\notin {E}\left({j}\right)$
19 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)$
20 15 17 18 19 syl3anc ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)$
21 20 ex ${⊢}{E}\left({j}\right)\in 𝒫{V}\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
22 21 adantr ${⊢}\left({E}\left({j}\right)\in 𝒫{V}\wedge {E}\left({j}\right)\ne \varnothing \right)\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
23 14 22 sylbi ${⊢}{E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
24 23 adantr ${⊢}\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\right)$
25 24 imp ${⊢}\left(\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)$
26 eldifsni ${⊢}{E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\to {E}\left({j}\right)\ne \varnothing$
27 26 adantr ${⊢}\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\to {E}\left({j}\right)\ne \varnothing$
28 27 adantr ${⊢}\left(\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\ne \varnothing$
29 eldifsn ${⊢}{E}\left({j}\right)\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)↔\left({E}\left({j}\right)\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)\wedge {E}\left({j}\right)\ne \varnothing \right)$
30 25 28 29 sylanbrc ${⊢}\left(\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)$
31 simpr ${⊢}\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\to \left|{E}\left({j}\right)\right|\le 2$
32 31 adantr ${⊢}\left(\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to \left|{E}\left({j}\right)\right|\le 2$
33 12 30 32 elrabd ${⊢}\left(\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\wedge {N}\notin {E}\left({j}\right)\right)\to {E}\left({j}\right)\in \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$
34 33 ex ${⊢}\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 2\right)\to \left({N}\notin {E}\left({j}\right)\to {E}\left({j}\right)\in \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
35 34 a1d ${⊢}\left({E}\left({j}\right)\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)\wedge \left|{E}\left({j}\right)\right|\le 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(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)\right)$
36 13 35 sylbi ${⊢}{E}\left({j}\right)\in \left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 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(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)\right)$
37 10 36 syl ${⊢}\left({E}:\mathrm{dom}{E}⟶\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 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(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)\right)$
38 37 ex ${⊢}{E}:\mathrm{dom}{E}⟶\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 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(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)\right)\right)$
39 38 com23 ${⊢}{E}:\mathrm{dom}{E}⟶\left\{{p}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 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(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)\right)\right)$
40 9 39 syl ${⊢}{G}\in \mathrm{UPGraph}\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(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)\right)\right)$
41 40 imp4b ${⊢}\left({G}\in \mathrm{UPGraph}\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(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
42 8 41 syl5bi ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {N}\in {V}\right)\to \left({j}\in {F}\to {E}\left({j}\right)\in \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
43 42 ralrimiv ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {N}\in {V}\right)\to \forall {j}\in {F}\phantom{\rule{.4em}{0ex}}{E}\left({j}\right)\in \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$
44 upgruhgr ${⊢}{G}\in \mathrm{UPGraph}\to {G}\in \mathrm{UHGraph}$
45 2 uhgrfun ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{Fun}{E}$
46 44 45 syl ${⊢}{G}\in \mathrm{UPGraph}\to \mathrm{Fun}{E}$
47 46 adantr ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {N}\in {V}\right)\to \mathrm{Fun}{E}$
48 3 ssrab3 ${⊢}{F}\subseteq \mathrm{dom}{E}$
49 funimass4 ${⊢}\left(\mathrm{Fun}{E}\wedge {F}\subseteq \mathrm{dom}{E}\right)\to \left({E}\left[{F}\right]\subseteq \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}↔\forall {j}\in {F}\phantom{\rule{.4em}{0ex}}{E}\left({j}\right)\in \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
50 47 48 49 sylancl ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {N}\in {V}\right)\to \left({E}\left[{F}\right]\subseteq \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}↔\forall {j}\in {F}\phantom{\rule{.4em}{0ex}}{E}\left({j}\right)\in \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}\right)$
51 43 50 mpbird ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {N}\in {V}\right)\to {E}\left[{F}\right]\subseteq \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$
52 4 51 eqsstrrid ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {N}\in {V}\right)\to \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in \left(𝒫\left({V}\setminus \left\{{N}\right\}\right)\setminus \left\{\varnothing \right\}\right)|\left|{p}\right|\le 2\right\}$