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=Vtx⁡G
upgrres.e ⊢E=iEdg⁡G
upgrres.f ⊢F=i∈dom⁡E|N∉E⁡i
Assertion umgrreslem ⊢G∈UMGraph∧N∈V→ran⁡E↾F⊆p∈𝒫V∖N|p=2

Proof

Step Hyp Ref Expression
1 upgrres.v ⊢V=Vtx⁡G
2 upgrres.e ⊢E=iEdg⁡G
3 upgrres.f ⊢F=i∈dom⁡E|N∉E⁡i
4 df-ima ⊢EF=ran⁡E↾F
5 fveq2 ⊢i=j→E⁡i=E⁡j
6 neleq2 ⊢E⁡i=E⁡j→N∉E⁡i↔N∉E⁡j
7 5 6 syl ⊢i=j→N∉E⁡i↔N∉E⁡j
8 7 3 elrab2 ⊢j∈F↔j∈dom⁡E∧N∉E⁡j
9 1 2 umgrf ⊢G∈UMGraph→E:dom⁡E⟶p∈𝒫V|p=2
10 ffvelcdm ⊢E:dom⁡E⟶p∈𝒫V|p=2∧j∈dom⁡E→E⁡j∈p∈𝒫V|p=2
11 fveqeq2 ⊢p=E⁡j→p=2↔E⁡j=2
12 11 elrab ⊢E⁡j∈p∈𝒫V|p=2↔E⁡j∈𝒫V∧E⁡j=2
13 simpll ⊢E⁡j∈𝒫V∧E⁡j=2∧N∉E⁡j→E⁡j∈𝒫V
14 elpwi ⊢E⁡j∈𝒫V→E⁡j⊆V
15 14 adantr ⊢E⁡j∈𝒫V∧E⁡j=2→E⁡j⊆V
16 15 adantr ⊢E⁡j∈𝒫V∧E⁡j=2∧N∉E⁡j→E⁡j⊆V
17 simpr ⊢E⁡j∈𝒫V∧E⁡j=2∧N∉E⁡j→N∉E⁡j
18 elpwdifsn ⊢E⁡j∈𝒫V∧E⁡j⊆V∧N∉E⁡j→E⁡j∈𝒫V∖N
19 13 16 17 18 syl3anc ⊢E⁡j∈𝒫V∧E⁡j=2∧N∉E⁡j→E⁡j∈𝒫V∖N
20 simpr ⊢E⁡j∈𝒫V∧E⁡j=2→E⁡j=2
21 20 adantr ⊢E⁡j∈𝒫V∧E⁡j=2∧N∉E⁡j→E⁡j=2
22 11 19 21 elrabd ⊢E⁡j∈𝒫V∧E⁡j=2∧N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
23 22 ex ⊢E⁡j∈𝒫V∧E⁡j=2→N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
24 23 a1d ⊢E⁡j∈𝒫V∧E⁡j=2→N∈V→N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
25 12 24 sylbi ⊢E⁡j∈p∈𝒫V|p=2→N∈V→N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
26 10 25 syl ⊢E:dom⁡E⟶p∈𝒫V|p=2∧j∈dom⁡E→N∈V→N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
27 26 ex ⊢E:dom⁡E⟶p∈𝒫V|p=2→j∈dom⁡E→N∈V→N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
28 27 com23 ⊢E:dom⁡E⟶p∈𝒫V|p=2→N∈V→j∈dom⁡E→N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
29 9 28 syl ⊢G∈UMGraph→N∈V→j∈dom⁡E→N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
30 29 imp4b ⊢G∈UMGraph∧N∈V→j∈dom⁡E∧N∉E⁡j→E⁡j∈p∈𝒫V∖N|p=2
31 8 30 biimtrid ⊢G∈UMGraph∧N∈V→j∈F→E⁡j∈p∈𝒫V∖N|p=2
32 31 ralrimiv ⊢G∈UMGraph∧N∈V→∀j∈FE⁡j∈p∈𝒫V∖N|p=2
33 umgruhgr ⊢G∈UMGraph→G∈UHGraph
34 2 uhgrfun ⊢G∈UHGraph→Fun⁡E
35 33 34 syl ⊢G∈UMGraph→Fun⁡E
36 35 adantr ⊢G∈UMGraph∧N∈V→Fun⁡E
37 3 ssrab3 ⊢F⊆dom⁡E
38 funimass4 ⊢Fun⁡E∧F⊆dom⁡E→EF⊆p∈𝒫V∖N|p=2↔∀j∈FE⁡j∈p∈𝒫V∖N|p=2
39 36 37 38 sylancl ⊢G∈UMGraph∧N∈V→EF⊆p∈𝒫V∖N|p=2↔∀j∈FE⁡j∈p∈𝒫V∖N|p=2
40 32 39 mpbird ⊢G∈UMGraph∧N∈V→EF⊆p∈𝒫V∖N|p=2
41 4 40 eqsstrrid ⊢G∈UMGraph∧N∈V→ran⁡E↾F⊆p∈𝒫V∖N|p=2