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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
upgrres1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
upgrres1.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
upgrres1.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
Assertion upgrres1 ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ UPGraph )

Proof

Step Hyp Ref Expression
1 upgrres1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upgrres1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 upgrres1.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4 upgrres1.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
5 f1oi ⊢ ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹
6 f1of ⊢ ( ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹 → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 )
7 5 6 mp1i ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 )
8 7 ffdmd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐹 )
9 simpr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐸 )
10 9 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ∈ 𝐸 )
11 2 eleq2i ⊢ ( 𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ( Edg ‘ 𝐺 ) )
12 edgupgr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝑒 ≠ ∅ ∧ ( ♯ ‘ 𝑒 ) ≤ 2 ) )
13 elpwi ⊢ ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → 𝑒 ⊆ ( Vtx ‘ 𝐺 ) )
14 13 1 sseqtrrdi ⊢ ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → 𝑒 ⊆ 𝑉 )
15 14 3ad2ant1 ⊢ ( ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝑒 ≠ ∅ ∧ ( ♯ ‘ 𝑒 ) ≤ 2 ) → 𝑒 ⊆ 𝑉 )
16 12 15 syl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ⊆ 𝑉 )
17 11 16 sylan2b ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ⊆ 𝑉 )
18 17 ad4ant13 ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ⊆ 𝑉 )
19 simpr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑁 ∉ 𝑒 )
20 elpwdifsn ⊢ ( ( 𝑒 ∈ 𝐸 ∧ 𝑒 ⊆ 𝑉 ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
21 10 18 19 20 syl3anc ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
22 simpl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐺 ∈ UPGraph )
23 11 biimpi ⊢ ( 𝑒 ∈ 𝐸 → 𝑒 ∈ ( Edg ‘ 𝐺 ) )
24 12 simp2d ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ≠ ∅ )
25 22 23 24 syl2an ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ≠ ∅ )
26 25 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ≠ ∅ )
27 nelsn ⊢ ( 𝑒 ≠ ∅ → ¬ 𝑒 ∈ { ∅ } )
28 26 27 syl ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → ¬ 𝑒 ∈ { ∅ } )
29 21 28 eldifd ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) )
30 29 ex ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑁 ∉ 𝑒 → 𝑒 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ) )
31 30 ralrimiva ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑒 ∈ 𝐸 ( 𝑁 ∉ 𝑒 → 𝑒 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ) )
32 rabss ⊢ ( { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } ⊆ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ↔ ∀ 𝑒 ∈ 𝐸 ( 𝑁 ∉ 𝑒 → 𝑒 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ) )
33 31 32 sylibr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } ⊆ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) )
34 3 33 eqsstrid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 ⊆ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) )
35 elrabi ⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } → 𝑝 ∈ 𝐸 )
36 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
37 2 36 eqtri ⊢ 𝐸 = ran ( iEdg ‘ 𝐺 )
38 37 eleq2i ⊢ ( 𝑝 ∈ 𝐸 ↔ 𝑝 ∈ ran ( iEdg ‘ 𝐺 ) )
39 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
40 1 39 upgrf ⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
41 40 frnd ⊢ ( 𝐺 ∈ UPGraph → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
42 41 sseld ⊢ ( 𝐺 ∈ UPGraph → ( 𝑝 ∈ ran ( iEdg ‘ 𝐺 ) → 𝑝 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
43 38 42 syl5bi ⊢ ( 𝐺 ∈ UPGraph → ( 𝑝 ∈ 𝐸 → 𝑝 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
44 fveq2 ⊢ ( 𝑥 = 𝑝 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑝 ) )
45 44 breq1d ⊢ ( 𝑥 = 𝑝 → ( ( ♯ ‘ 𝑥 ) ≤ 2 ↔ ( ♯ ‘ 𝑝 ) ≤ 2 ) )
46 45 elrab ⊢ ( 𝑝 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ ( 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ 𝑝 ) ≤ 2 ) )
47 46 simprbi ⊢ ( 𝑝 ∈ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( ♯ ‘ 𝑝 ) ≤ 2 )
48 43 47 syl6 ⊢ ( 𝐺 ∈ UPGraph → ( 𝑝 ∈ 𝐸 → ( ♯ ‘ 𝑝 ) ≤ 2 ) )
49 48 adantr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑝 ∈ 𝐸 → ( ♯ ‘ 𝑝 ) ≤ 2 ) )
50 35 49 syl5com ⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } → ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ 𝑝 ) ≤ 2 ) )
51 50 3 eleq2s ⊢ ( 𝑝 ∈ 𝐹 → ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ 𝑝 ) ≤ 2 ) )
52 51 impcom ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑝 ∈ 𝐹 ) → ( ♯ ‘ 𝑝 ) ≤ 2 )
53 34 52 ssrabdv ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 ⊆ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
54 8 53 fssd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
55 opex ⊢ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩ ∈ V
56 4 55 eqeltri ⊢ 𝑆 ∈ V
57 1 2 3 4 upgrres1lem2 ⊢ ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
58 57 eqcomi ⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
59 1 2 3 4 upgrres1lem3 ⊢ ( iEdg ‘ 𝑆 ) = ( I ↾ 𝐹 )
60 59 eqcomi ⊢ ( I ↾ 𝐹 ) = ( iEdg ‘ 𝑆 )
61 58 60 isupgr ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ UPGraph ↔ ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
62 56 61 mp1i ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑆 ∈ UPGraph ↔ ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
63 54 62 mpbird ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ UPGraph )