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 ⊢ V = Vtx ⁡ G
upgrres.e ⊢ E = iEdg ⁡ G
upgrres.f ⊢ F = i ∈ dom ⁡ E | N ∉ E ⁡ i
Assertion upgrreslem ⊢ G ∈ UPGraph ∧ N ∈ V → ran ⁡ E ↾ F ⊆ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2

Proof

Step Hyp Ref Expression
1 upgrres.v ⊢ V = Vtx ⁡ G
2 upgrres.e ⊢ E = iEdg ⁡ G
3 upgrres.f ⊢ F = i ∈ dom ⁡ E | N ∉ E ⁡ i
4 df-ima ⊢ E F = ran ⁡ E ↾ F
5 fveq2 ⊢ i = j → E ⁡ i = E ⁡ j
6 neleq2 ⊢ E ⁡ i = E ⁡ j → N ∉ E ⁡ i ↔ N ∉ E ⁡ j
7 5 6 syl ⊢ i = j → N ∉ E ⁡ i ↔ N ∉ E ⁡ j
8 7 3 elrab2 ⊢ j ∈ F ↔ j ∈ dom ⁡ E ∧ N ∉ E ⁡ j
9 1 2 upgrf ⊢ G ∈ UPGraph → E : dom ⁡ E ⟶ p ∈ 𝒫 V ∖ ∅ | p ≤ 2
10 ffvelcdm ⊢ E : dom ⁡ E ⟶ p ∈ 𝒫 V ∖ ∅ | p ≤ 2 ∧ j ∈ dom ⁡ E → E ⁡ j ∈ p ∈ 𝒫 V ∖ ∅ | p ≤ 2
11 fveq2 ⊢ p = E ⁡ j → p = E ⁡ j
12 11 breq1d ⊢ p = E ⁡ j → p ≤ 2 ↔ E ⁡ j ≤ 2
13 12 elrab ⊢ E ⁡ j ∈ p ∈ 𝒫 V ∖ ∅ | p ≤ 2 ↔ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2
14 eldifsn ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ↔ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j ≠ ∅
15 simpl ⊢ E ⁡ j ∈ 𝒫 V ∧ N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V
16 elpwi ⊢ E ⁡ j ∈ 𝒫 V → E ⁡ j ⊆ V
17 16 adantr ⊢ E ⁡ j ∈ 𝒫 V ∧ N ∉ E ⁡ j → E ⁡ j ⊆ V
18 simpr ⊢ E ⁡ j ∈ 𝒫 V ∧ N ∉ E ⁡ j → N ∉ E ⁡ j
19 elpwdifsn ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j ⊆ V ∧ N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
20 15 17 18 19 syl3anc ⊢ E ⁡ j ∈ 𝒫 V ∧ N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
21 20 ex ⊢ E ⁡ j ∈ 𝒫 V → N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
22 21 adantr ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j ≠ ∅ → N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
23 14 22 sylbi ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ → N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
24 23 adantr ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 → N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
25 24 imp ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 ∧ N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
26 eldifsni ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ → E ⁡ j ≠ ∅
27 26 adantr ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 → E ⁡ j ≠ ∅
28 27 adantr ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 ∧ N ∉ E ⁡ j → E ⁡ j ≠ ∅
29 eldifsn ⊢ E ⁡ j ∈ 𝒫 V ∖ N ∖ ∅ ↔ E ⁡ j ∈ 𝒫 V ∖ N ∧ E ⁡ j ≠ ∅
30 25 28 29 sylanbrc ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 ∧ N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N ∖ ∅
31 simpr ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 → E ⁡ j ≤ 2
32 31 adantr ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 ∧ N ∉ E ⁡ j → E ⁡ j ≤ 2
33 12 30 32 elrabd ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 ∧ N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
34 33 ex ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
35 34 a1d ⊢ E ⁡ j ∈ 𝒫 V ∖ ∅ ∧ E ⁡ j ≤ 2 → N ∈ V → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
36 13 35 sylbi ⊢ E ⁡ j ∈ p ∈ 𝒫 V ∖ ∅ | p ≤ 2 → N ∈ V → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
37 10 36 syl ⊢ E : dom ⁡ E ⟶ p ∈ 𝒫 V ∖ ∅ | p ≤ 2 ∧ j ∈ dom ⁡ E → N ∈ V → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
38 37 ex ⊢ E : dom ⁡ E ⟶ p ∈ 𝒫 V ∖ ∅ | p ≤ 2 → j ∈ dom ⁡ E → N ∈ V → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
39 38 com23 ⊢ E : dom ⁡ E ⟶ p ∈ 𝒫 V ∖ ∅ | p ≤ 2 → N ∈ V → j ∈ dom ⁡ E → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
40 9 39 syl ⊢ G ∈ UPGraph → N ∈ V → j ∈ dom ⁡ E → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
41 40 imp4b ⊢ G ∈ UPGraph ∧ N ∈ V → j ∈ dom ⁡ E ∧ N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
42 8 41 biimtrid ⊢ G ∈ UPGraph ∧ N ∈ V → j ∈ F → E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
43 42 ralrimiv ⊢ G ∈ UPGraph ∧ N ∈ V → ∀ j ∈ F E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
44 upgruhgr ⊢ G ∈ UPGraph → G ∈ UHGraph
45 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ E
46 44 45 syl ⊢ G ∈ UPGraph → Fun ⁡ E
47 46 adantr ⊢ G ∈ UPGraph ∧ N ∈ V → Fun ⁡ E
48 3 ssrab3 ⊢ F ⊆ dom ⁡ E
49 funimass4 ⊢ Fun ⁡ E ∧ F ⊆ dom ⁡ E → E F ⊆ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2 ↔ ∀ j ∈ F E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
50 47 48 49 sylancl ⊢ G ∈ UPGraph ∧ N ∈ V → E F ⊆ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2 ↔ ∀ j ∈ F E ⁡ j ∈ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
51 43 50 mpbird ⊢ G ∈ UPGraph ∧ N ∈ V → E F ⊆ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2
52 4 51 eqsstrrid ⊢ G ∈ UPGraph ∧ N ∈ V → ran ⁡ E ↾ F ⊆ p ∈ 𝒫 V ∖ N ∖ ∅ | p ≤ 2