Metamath Proof Explorer

Theorem umgrres1lem

Description: Lemma for umgrres1 . (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses upgrres1.v ⊢V=Vtx⁡G
upgrres1.e ⊢E=Edg⁡G
upgrres1.f ⊢F=e∈E|N∉e
Assertion umgrres1lem ⊢G∈UMGraph∧N∈V→ran⁡I↾F⊆p∈𝒫V∖N|p=2

Proof

Step Hyp Ref Expression
1 upgrres1.v ⊢V=Vtx⁡G
2 upgrres1.e ⊢E=Edg⁡G
3 upgrres1.f ⊢F=e∈E|N∉e
4 rnresi ⊢ran⁡I↾F=F
5 simpr ⊢G∈UMGraph∧N∈V∧e∈E→e∈E
6 5 adantr ⊢G∈UMGraph∧N∈V∧e∈E∧N∉e→e∈E
7 umgruhgr ⊢G∈UMGraph→G∈UHGraph
8 2 eleq2i ⊢e∈E↔e∈Edg⁡G
9 8 biimpi ⊢e∈E→e∈Edg⁡G
10 edguhgr ⊢G∈UHGraph∧e∈Edg⁡G→e∈𝒫Vtx⁡G
11 elpwi ⊢e∈𝒫Vtx⁡G→e⊆Vtx⁡G
12 11 1 sseqtrrdi ⊢e∈𝒫Vtx⁡G→e⊆V
13 10 12 syl ⊢G∈UHGraph∧e∈Edg⁡G→e⊆V
14 7 9 13 syl2an ⊢G∈UMGraph∧e∈E→e⊆V
15 14 ad4ant13 ⊢G∈UMGraph∧N∈V∧e∈E∧N∉e→e⊆V
16 simpr ⊢G∈UMGraph∧N∈V∧e∈E∧N∉e→N∉e
17 elpwdifsn ⊢e∈E∧e⊆V∧N∉e→e∈𝒫V∖N
18 6 15 16 17 syl3anc ⊢G∈UMGraph∧N∈V∧e∈E∧N∉e→e∈𝒫V∖N
19 18 ex ⊢G∈UMGraph∧N∈V∧e∈E→N∉e→e∈𝒫V∖N
20 19 ralrimiva ⊢G∈UMGraph∧N∈V→∀e∈EN∉e→e∈𝒫V∖N
21 rabss ⊢e∈E|N∉e⊆𝒫V∖N↔∀e∈EN∉e→e∈𝒫V∖N
22 20 21 sylibr ⊢G∈UMGraph∧N∈V→e∈E|N∉e⊆𝒫V∖N
23 3 22 eqsstrid ⊢G∈UMGraph∧N∈V→F⊆𝒫V∖N
24 elrabi ⊢p∈e∈E|N∉e→p∈E
25 24 2 eleqtrdi ⊢p∈e∈E|N∉e→p∈Edg⁡G
26 edgumgr ⊢G∈UMGraph∧p∈Edg⁡G→p∈𝒫Vtx⁡G∧p=2
27 26 simprd ⊢G∈UMGraph∧p∈Edg⁡G→p=2
28 27 ex ⊢G∈UMGraph→p∈Edg⁡G→p=2
29 28 adantr ⊢G∈UMGraph∧N∈V→p∈Edg⁡G→p=2
30 25 29 syl5com ⊢p∈e∈E|N∉e→G∈UMGraph∧N∈V→p=2
31 30 3 eleq2s ⊢p∈F→G∈UMGraph∧N∈V→p=2
32 31 impcom ⊢G∈UMGraph∧N∈V∧p∈F→p=2
33 23 32 ssrabdv ⊢G∈UMGraph∧N∈V→F⊆p∈𝒫V∖N|p=2
34 4 33 eqsstrid ⊢G∈UMGraph∧N∈V→ran⁡I↾F⊆p∈𝒫V∖N|p=2