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