Metamath Proof Explorer

Theorem upgrreslem

Description: Lemma for upgrres . (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 upgrreslem ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 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 upgrf ⊢ ( 𝐺 ∈ UPGraph → 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
10 ffvelrn ⊢ ( ( 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ∧ 𝑗 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
11 fveq2 ⊢ ( 𝑝 = ( 𝐸 ‘ 𝑗 ) → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) )
12 11 breq1d ⊢ ( 𝑝 = ( 𝐸 ‘ 𝑗 ) → ( ( ♯ ‘ 𝑝 ) ≤ 2 ↔ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) )
13 12 elrab ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) )
14 eldifsn ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( 𝐸 ‘ 𝑗 ) ≠ ∅ ) )
15 simpl ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 )
16 elpwi ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 → ( 𝐸 ‘ 𝑗 ) ⊆ 𝑉 )
17 16 adantr ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ 𝑉 )
18 simpr ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) )
19 elpwdifsn ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( 𝐸 ‘ 𝑗 ) ⊆ 𝑉 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
20 15 17 18 19 syl3anc ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
21 20 ex ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
22 21 adantr ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 𝑉 ∧ ( 𝐸 ‘ 𝑗 ) ≠ ∅ ) → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
23 14 22 sylbi ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
24 23 adantr ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
25 24 imp ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
26 eldifsni ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝐸 ‘ 𝑗 ) ≠ ∅ )
27 26 adantr ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) → ( 𝐸 ‘ 𝑗 ) ≠ ∅ )
28 27 adantr ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ≠ ∅ )
29 eldifsn ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ↔ ( ( 𝐸 ‘ 𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∧ ( 𝐸 ‘ 𝑗 ) ≠ ∅ ) )
30 25 28 29 sylanbrc ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) )
31 simpr ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 )
32 31 adantr ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 )
33 12 30 32 elrabd ⊢ ( ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
34 33 ex ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
35 34 a1d ⊢ ( ( ( 𝐸 ‘ 𝑗 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ 2 ) → ( 𝑁 ∈ 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) )
36 13 35 sylbi ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } → ( 𝑁 ∈ 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) )
37 10 36 syl ⊢ ( ( 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ∧ 𝑗 ∈ dom 𝐸 ) → ( 𝑁 ∈ 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) )
38 37 ex ⊢ ( 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } → ( 𝑗 ∈ dom 𝐸 → ( 𝑁 ∈ 𝑉 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) ) )
39 38 com23 ⊢ ( 𝐸 : dom 𝐸 ⟶ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } → ( 𝑁 ∈ 𝑉 → ( 𝑗 ∈ dom 𝐸 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) ) )
40 9 39 syl ⊢ ( 𝐺 ∈ UPGraph → ( 𝑁 ∈ 𝑉 → ( 𝑗 ∈ dom 𝐸 → ( 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) ) ) )
41 40 imp4b ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑗 ∈ dom 𝐸 ∧ 𝑁 ∉ ( 𝐸 ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
42 8 41 syl5bi ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑗 ∈ 𝐹 → ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
43 42 ralrimiv ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑗 ∈ 𝐹 ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
44 upgruhgr ⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
45 2 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
46 44 45 syl ⊢ ( 𝐺 ∈ UPGraph → Fun 𝐸 )
47 46 adantr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → Fun 𝐸 )
48 3 ssrab3 ⊢ 𝐹 ⊆ dom 𝐸
49 funimass4 ⊢ ( ( Fun 𝐸 ∧ 𝐹 ⊆ dom 𝐸 ) → ( ( 𝐸 “ 𝐹 ) ⊆ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ ∀ 𝑗 ∈ 𝐹 ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
50 47 48 49 sylancl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝐸 “ 𝐹 ) ⊆ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ ∀ 𝑗 ∈ 𝐹 ( 𝐸 ‘ 𝑗 ) ∈ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
51 43 50 mpbird ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 “ 𝐹 ) ⊆ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
52 4 51 eqsstrrid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ran ( 𝐸 ↾ 𝐹 ) ⊆ { 𝑝 ∈ ( 𝒫 ( 𝑉 ∖ { 𝑁 } ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )