Metamath Proof Explorer

Theorem umgrreslem

Description: Lemma for umgrres and usgrres . (Contributed by AV, 27-Nov-2020) (Revised by AV, 19-Dec-2021)

Ref Expression
Hypotheses upgrres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
upgrres.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
upgrres.f ⊢ 𝐹 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
Assertion umgrreslem ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( 𝐸 ↾ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )

Proof

Step Hyp Ref Expression
1 upgrres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upgrres.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 upgrres.f ⊢ 𝐹 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
4 df-ima ⊢ ( 𝐸 “ 𝐹 ) = ran ( 𝐸 ↾ 𝐹 )
5 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑗 ) )
6 neleq2 ⊢ ( ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑗 ) → ( 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) ↔ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) )
7 5 6 syl ⊢ ( 𝑖 = 𝑗 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) ↔ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) )
8 7 3 elrab2 ⊢ ( 𝑗 ∈ 𝐹 ↔ ( 𝑗 ∈ dom 𝐸 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) )
9 1 2 umgrf ⊢ ( 𝐺 ∈ UMGraph → 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } )
10 ffvelcdm ⊢ ( ( 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } ∧ 𝑗 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } )
11 fveqeq2 ⊢ ( 𝑝 = ( 𝐸 ‘ 𝑗 ) → ( ( ♯ ‘ 𝑝 ) = 2 ↔ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) )
12 11 elrab ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) )
13 simpll ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 )
14 elpwi ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 → ( 𝐸 ‘ 𝑗 ) ⊆ 𝑉 )
15 14 adantr ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) → ( 𝐸 ‘ 𝑗 ) ⊆ 𝑉 )
16 15 adantr ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ 𝑉 )
17 simpr ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) )
18 elpwdifsn ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( 𝐸 ‘ 𝑗 ) ⊆ 𝑉 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
19 13 16 17 18 syl3anc ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
20 simpr ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 )
21 20 adantr ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 )
22 11 19 21 elrabd ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
23 22 ex ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
24 23 a1d ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) = 2 ) → ( 𝑁 ∈ 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) ) )
25 12 24 sylbi ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } → ( 𝑁 ∈ 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) ) )
26 10 25 syl ⊢ ( ( 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } ∧ 𝑗 ∈ dom 𝐸 ) → ( 𝑁 ∈ 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) ) )
27 26 ex ⊢ ( 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } → ( 𝑗 ∈ dom 𝐸 → ( 𝑁 ∈ 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) ) ) )
28 27 com23 ⊢ ( 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } → ( 𝑁 ∈ 𝑉 → ( 𝑗 ∈ dom 𝐸 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) ) ) )
29 9 28 syl ⊢ ( 𝐺 ∈ UMGraph → ( 𝑁 ∈ 𝑉 → ( 𝑗 ∈ dom 𝐸 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) ) ) )
30 29 imp4b ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑗 ∈ dom 𝐸 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
31 8 30 biimtrid ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑗 ∈ 𝐹 → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
32 31 ralrimiv ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑗 ∈ 𝐹 ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
33 umgruhgr ⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
34 2 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
35 33 34 syl ⊢ ( 𝐺 ∈ UMGraph → Fun 𝐸 )
36 35 adantr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → Fun 𝐸 )
37 3 ssrab3 ⊢ 𝐹 ⊆ dom 𝐸
38 funimass4 ⊢ ( ( Fun 𝐸 ∧ 𝐹 ⊆ dom 𝐸 ) → ( ( 𝐸 “ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ∀ 𝑗 ∈ 𝐹 ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
39 36 37 38 sylancl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝐸 “ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ∀ 𝑗 ∈ 𝐹 ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
40 32 39 mpbird ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 “ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
41 4 40 eqsstrrid ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( 𝐸 ↾ 𝐹 ) ⊆ { 𝑝 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )