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=Vtx⁡G
upgrres.e ⊢E=iEdg⁡G
upgrres.f ⊢F=i∈dom⁡E|N∉E⁡i
Assertion upgrreslem ⊢G∈UPGraph∧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 upgrf ⊢G∈UPGraph→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 fveq2 ⊢p=E⁡j→p=E⁡j
12 11 breq1d ⊢p=E⁡j→p≤2↔E⁡j≤2
13 12 elrab ⊢E⁡j∈p∈𝒫V∖∅|p≤2↔E⁡j∈𝒫V∖∅∧E⁡j≤2
14 eldifsn ⊢E⁡j∈𝒫V∖∅↔E⁡j∈𝒫V∧E⁡j≠∅
15 simpl ⊢E⁡j∈𝒫V∧N∉E⁡j→E⁡j∈𝒫V
16 elpwi ⊢E⁡j∈𝒫V→E⁡j⊆V
17 16 adantr ⊢E⁡j∈𝒫V∧N∉E⁡j→E⁡j⊆V
18 simpr ⊢E⁡j∈𝒫V∧N∉E⁡j→N∉E⁡j
19 elpwdifsn ⊢E⁡j∈𝒫V∧E⁡j⊆V∧N∉E⁡j→E⁡j∈𝒫V∖N
20 15 17 18 19 syl3anc ⊢E⁡j∈𝒫V∧N∉E⁡j→E⁡j∈𝒫V∖N
21 20 ex ⊢E⁡j∈𝒫V→N∉E⁡j→E⁡j∈𝒫V∖N
22 21 adantr ⊢E⁡j∈𝒫V∧E⁡j≠∅→N∉E⁡j→E⁡j∈𝒫V∖N
23 14 22 sylbi ⊢E⁡j∈𝒫V∖∅→N∉E⁡j→E⁡j∈𝒫V∖N
24 23 adantr ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2→N∉E⁡j→E⁡j∈𝒫V∖N
25 24 imp ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2∧N∉E⁡j→E⁡j∈𝒫V∖N
26 eldifsni ⊢E⁡j∈𝒫V∖∅→E⁡j≠∅
27 26 adantr ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2→E⁡j≠∅
28 27 adantr ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2∧N∉E⁡j→E⁡j≠∅
29 eldifsn ⊢E⁡j∈𝒫V∖N∖∅↔E⁡j∈𝒫V∖N∧E⁡j≠∅
30 25 28 29 sylanbrc ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2∧N∉E⁡j→E⁡j∈𝒫V∖N∖∅
31 simpr ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2→E⁡j≤2
32 31 adantr ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2∧N∉E⁡j→E⁡j≤2
33 12 30 32 elrabd ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2∧N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
34 33 ex ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2→N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
35 34 a1d ⊢E⁡j∈𝒫V∖∅∧E⁡j≤2→N∈V→N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
36 13 35 sylbi ⊢E⁡j∈p∈𝒫V∖∅|p≤2→N∈V→N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
37 10 36 syl ⊢E:dom⁡E⟶p∈𝒫V∖∅|p≤2∧j∈dom⁡E→N∈V→N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
38 37 ex ⊢E:dom⁡E⟶p∈𝒫V∖∅|p≤2→j∈dom⁡E→N∈V→N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
39 38 com23 ⊢E:dom⁡E⟶p∈𝒫V∖∅|p≤2→N∈V→j∈dom⁡E→N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
40 9 39 syl ⊢G∈UPGraph→N∈V→j∈dom⁡E→N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
41 40 imp4b ⊢G∈UPGraph∧N∈V→j∈dom⁡E∧N∉E⁡j→E⁡j∈p∈𝒫V∖N∖∅|p≤2
42 8 41 biimtrid ⊢G∈UPGraph∧N∈V→j∈F→E⁡j∈p∈𝒫V∖N∖∅|p≤2
43 42 ralrimiv ⊢G∈UPGraph∧N∈V→∀j∈FE⁡j∈p∈𝒫V∖N∖∅|p≤2
44 upgruhgr ⊢G∈UPGraph→G∈UHGraph
45 2 uhgrfun ⊢G∈UHGraph→Fun⁡E
46 44 45 syl ⊢G∈UPGraph→Fun⁡E
47 46 adantr ⊢G∈UPGraph∧N∈V→Fun⁡E
48 3 ssrab3 ⊢F⊆dom⁡E
49 funimass4 ⊢Fun⁡E∧F⊆dom⁡E→EF⊆p∈𝒫V∖N∖∅|p≤2↔∀j∈FE⁡j∈p∈𝒫V∖N∖∅|p≤2
50 47 48 49 sylancl ⊢G∈UPGraph∧N∈V→EF⊆p∈𝒫V∖N∖∅|p≤2↔∀j∈FE⁡j∈p∈𝒫V∖N∖∅|p≤2
51 43 50 mpbird ⊢G∈UPGraph∧N∈V→EF⊆p∈𝒫V∖N∖∅|p≤2
52 4 51 eqsstrrid ⊢G∈UPGraph∧N∈V→ran⁡E↾F⊆p∈𝒫V∖N∖∅|p≤2