Metamath Proof Explorer

Theorem upgrres1

Description: A pseudograph obtained by removing one vertex and all edges incident with this vertex is a pseudograph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr since the domains of the edge functions may not be compatible. (Contributed by AV, 8-Nov-2020)

Ref Expression
Hypotheses upgrres1.v ⊢V=Vtx⁡G
upgrres1.e ⊢E=Edg⁡G
upgrres1.f ⊢F=e∈E|N∉e
upgrres1.s ⊢S=V∖NI↾F
Assertion upgrres1 ⊢G∈UPGraph∧N∈V→S∈UPGraph

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 upgrres1.s ⊢S=V∖NI↾F
5 f1oi ⊢I↾F:F⟶1-1 ontoF
6 f1of ⊢I↾F:F⟶1-1 ontoF→I↾F:F⟶F
7 5 6 mp1i ⊢G∈UPGraph∧N∈V→I↾F:F⟶F
8 7 ffdmd ⊢G∈UPGraph∧N∈V→I↾F:dom⁡I↾F⟶F
9 simpr ⊢G∈UPGraph∧N∈V∧e∈E→e∈E
10 9 adantr ⊢G∈UPGraph∧N∈V∧e∈E∧N∉e→e∈E
11 2 eleq2i ⊢e∈E↔e∈Edg⁡G
12 edgupgr ⊢G∈UPGraph∧e∈Edg⁡G→e∈𝒫Vtx⁡G∧e≠∅∧e≤2
13 elpwi ⊢e∈𝒫Vtx⁡G→e⊆Vtx⁡G
14 13 1 sseqtrrdi ⊢e∈𝒫Vtx⁡G→e⊆V
15 14 3ad2ant1 ⊢e∈𝒫Vtx⁡G∧e≠∅∧e≤2→e⊆V
16 12 15 syl ⊢G∈UPGraph∧e∈Edg⁡G→e⊆V
17 11 16 sylan2b ⊢G∈UPGraph∧e∈E→e⊆V
18 17 ad4ant13 ⊢G∈UPGraph∧N∈V∧e∈E∧N∉e→e⊆V
19 simpr ⊢G∈UPGraph∧N∈V∧e∈E∧N∉e→N∉e
20 elpwdifsn ⊢e∈E∧e⊆V∧N∉e→e∈𝒫V∖N
21 10 18 19 20 syl3anc ⊢G∈UPGraph∧N∈V∧e∈E∧N∉e→e∈𝒫V∖N
22 simpl ⊢G∈UPGraph∧N∈V→G∈UPGraph
23 11 biimpi ⊢e∈E→e∈Edg⁡G
24 12 simp2d ⊢G∈UPGraph∧e∈Edg⁡G→e≠∅
25 22 23 24 syl2an ⊢G∈UPGraph∧N∈V∧e∈E→e≠∅
26 25 adantr ⊢G∈UPGraph∧N∈V∧e∈E∧N∉e→e≠∅
27 nelsn ⊢e≠∅→¬e∈∅
28 26 27 syl ⊢G∈UPGraph∧N∈V∧e∈E∧N∉e→¬e∈∅
29 21 28 eldifd ⊢G∈UPGraph∧N∈V∧e∈E∧N∉e→e∈𝒫V∖N∖∅
30 29 ex ⊢G∈UPGraph∧N∈V∧e∈E→N∉e→e∈𝒫V∖N∖∅
31 30 ralrimiva ⊢G∈UPGraph∧N∈V→∀e∈EN∉e→e∈𝒫V∖N∖∅
32 rabss ⊢e∈E|N∉e⊆𝒫V∖N∖∅↔∀e∈EN∉e→e∈𝒫V∖N∖∅
33 31 32 sylibr ⊢G∈UPGraph∧N∈V→e∈E|N∉e⊆𝒫V∖N∖∅
34 3 33 eqsstrid ⊢G∈UPGraph∧N∈V→F⊆𝒫V∖N∖∅
35 elrabi ⊢p∈e∈E|N∉e→p∈E
36 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
37 2 36 eqtri ⊢E=ran⁡iEdg⁡G
38 37 eleq2i ⊢p∈E↔p∈ran⁡iEdg⁡G
39 eqid ⊢iEdg⁡G=iEdg⁡G
40 1 39 upgrf ⊢G∈UPGraph→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫V∖∅|x≤2
41 40 frnd ⊢G∈UPGraph→ran⁡iEdg⁡G⊆x∈𝒫V∖∅|x≤2
42 41 sseld ⊢G∈UPGraph→p∈ran⁡iEdg⁡G→p∈x∈𝒫V∖∅|x≤2
43 38 42 biimtrid ⊢G∈UPGraph→p∈E→p∈x∈𝒫V∖∅|x≤2
44 fveq2 ⊢x=p→x=p
45 44 breq1d ⊢x=p→x≤2↔p≤2
46 45 elrab ⊢p∈x∈𝒫V∖∅|x≤2↔p∈𝒫V∖∅∧p≤2
47 46 simprbi ⊢p∈x∈𝒫V∖∅|x≤2→p≤2
48 43 47 syl6 ⊢G∈UPGraph→p∈E→p≤2
49 48 adantr ⊢G∈UPGraph∧N∈V→p∈E→p≤2
50 35 49 syl5com ⊢p∈e∈E|N∉e→G∈UPGraph∧N∈V→p≤2
51 50 3 eleq2s ⊢p∈F→G∈UPGraph∧N∈V→p≤2
52 51 impcom ⊢G∈UPGraph∧N∈V∧p∈F→p≤2
53 34 52 ssrabdv ⊢G∈UPGraph∧N∈V→F⊆p∈𝒫V∖N∖∅|p≤2
54 8 53 fssd ⊢G∈UPGraph∧N∈V→I↾F:dom⁡I↾F⟶p∈𝒫V∖N∖∅|p≤2
55 opex ⊢V∖NI↾F∈V
56 4 55 eqeltri ⊢S∈V
57 1 2 3 4 upgrres1lem2 ⊢Vtx⁡S=V∖N
58 57 eqcomi ⊢V∖N=Vtx⁡S
59 1 2 3 4 upgrres1lem3 ⊢iEdg⁡S=I↾F
60 59 eqcomi ⊢I↾F=iEdg⁡S
61 58 60 isupgr ⊢S∈V→S∈UPGraph↔I↾F:dom⁡I↾F⟶p∈𝒫V∖N∖∅|p≤2
62 56 61 mp1i ⊢G∈UPGraph∧N∈V→S∈UPGraph↔I↾F:dom⁡I↾F⟶p∈𝒫V∖N∖∅|p≤2
63 54 62 mpbird ⊢G∈UPGraph∧N∈V→S∈UPGraph