This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )