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 N I 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 N I F
5 f1oi I F : F 1-1 onto F
6 f1of I F : F 1-1 onto F 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 E N e e 𝒫 V N
32 rabss e E | N e 𝒫 V N e E N 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 syl5bi 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 N I 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