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	biimtrid	⊢ ( 𝐺 ∈ 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 )

Metamath Proof Explorer

Theorem upgrres1

Proof