Theorem umgrres1lem

Description: Lemma for umgrres1 . (Contributed by AV, 27-Nov-2020)

	Ref	Expression
Hypotheses	upgrres1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	upgrres1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	upgrres1.f	⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
Assertion	umgrres1lem	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( I ↾ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )

Proof

Step	Hyp	Ref	Expression
1		upgrres1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		upgrres1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		upgrres1.f	⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4		rnresi	⊢ ran ( I ↾ 𝐹 ) = 𝐹
5		simpr	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐸 )
6	5	adantr	⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ∈ 𝐸 )
7		umgruhgr	⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
8	2	eleq2i	⊢ ( 𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ( Edg ‘ 𝐺 ) )
9	8	biimpi	⊢ ( 𝑒 ∈ 𝐸 → 𝑒 ∈ ( Edg ‘ 𝐺 ) )
10		edguhgr	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
11		elpwi	⊢ ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → 𝑒 ⊆ ( Vtx ‘ 𝐺 ) )
12	11 1	sseqtrrdi	⊢ ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → 𝑒 ⊆ 𝑉 )
13	10 12	syl	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ⊆ 𝑉 )
14	7 9 13	syl2an	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ⊆ 𝑉 )
15	14	ad4ant13	⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ⊆ 𝑉 )
16		simpr	⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑁 ∉ 𝑒 )
17		elpwdifsn	⊢ ( ( 𝑒 ∈ 𝐸 ∧ 𝑒 ⊆ 𝑉 ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
18	6 15 16 17	syl3anc	⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑁 ∉ 𝑒 ) → 𝑒 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
19	18	ex	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑁 ∉ 𝑒 → 𝑒 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
20	19	ralrimiva	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑒 ∈ 𝐸 ( 𝑁 ∉ 𝑒 → 𝑒 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
21		rabss	⊢ ( { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } ⊆ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ↔ ∀ 𝑒 ∈ 𝐸 ( 𝑁 ∉ 𝑒 → 𝑒 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
22	20 21	sylibr	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } ⊆ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
23	3 22	eqsstrid	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 ⊆ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
24		elrabi	⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } → 𝑝 ∈ 𝐸 )
25	24 2	eleqtrdi	⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } → 𝑝 ∈ ( Edg ‘ 𝐺 ) )
26		edgumgr	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑝 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑝 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
27	26	simprd	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑝 ∈ ( Edg ‘ 𝐺 ) ) → ( ♯ ‘ 𝑝 ) = 2 )
28	27	ex	⊢ ( 𝐺 ∈ UMGraph → ( 𝑝 ∈ ( Edg ‘ 𝐺 ) → ( ♯ ‘ 𝑝 ) = 2 ) )
29	28	adantr	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑝 ∈ ( Edg ‘ 𝐺 ) → ( ♯ ‘ 𝑝 ) = 2 ) )
30	25 29	syl5com	⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ 𝑝 ) = 2 ) )
31	30 3	eleq2s	⊢ ( 𝑝 ∈ 𝐹 → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ 𝑝 ) = 2 ) )
32	31	impcom	⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑝 ∈ 𝐹 ) → ( ♯ ‘ 𝑝 ) = 2 )
33	23 32	ssrabdv	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
34	4 33	eqsstrid	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( I ↾ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )