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 ⊢ V = Vtx ⁡ G
upgrres.e ⊢ E = iEdg ⁡ G
upgrres.f ⊢ F = i ∈ dom ⁡ E | N ∉ E ⁡ i
Assertion umgrreslem ⊢ G ∈ UMGraph ∧ 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 umgrf ⊢ G ∈ UMGraph → E : dom ⁡ E ⟶ p ∈ 𝒫 V | p = 2
10 ffvelrn ⊢ E : dom ⁡ E ⟶ p ∈ 𝒫 V | p = 2 ∧ j ∈ dom ⁡ E → E ⁡ j ∈ p ∈ 𝒫 V | p = 2
11 fveqeq2 ⊢ p = E ⁡ j → p = 2 ↔ E ⁡ j = 2
12 11 elrab ⊢ E ⁡ j ∈ p ∈ 𝒫 V | p = 2 ↔ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2
13 simpll ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 ∧ N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V
14 elpwi ⊢ E ⁡ j ∈ 𝒫 V → E ⁡ j ⊆ V
15 14 adantr ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 → E ⁡ j ⊆ V
16 15 adantr ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 ∧ N ∉ E ⁡ j → E ⁡ j ⊆ V
17 simpr ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 ∧ N ∉ E ⁡ j → N ∉ E ⁡ j
18 elpwdifsn ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j ⊆ V ∧ N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
19 13 16 17 18 syl3anc ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 ∧ N ∉ E ⁡ j → E ⁡ j ∈ 𝒫 V ∖ N
20 simpr ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 → E ⁡ j = 2
21 20 adantr ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 ∧ N ∉ E ⁡ j → E ⁡ j = 2
22 11 19 21 elrabd ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 ∧ N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
23 22 ex ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
24 23 a1d ⊢ E ⁡ j ∈ 𝒫 V ∧ E ⁡ j = 2 → N ∈ V → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
25 12 24 sylbi ⊢ E ⁡ j ∈ p ∈ 𝒫 V | p = 2 → N ∈ V → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
26 10 25 syl ⊢ E : dom ⁡ E ⟶ p ∈ 𝒫 V | p = 2 ∧ j ∈ dom ⁡ E → N ∈ V → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
27 26 ex ⊢ E : dom ⁡ E ⟶ p ∈ 𝒫 V | p = 2 → j ∈ dom ⁡ E → N ∈ V → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
28 27 com23 ⊢ E : dom ⁡ E ⟶ p ∈ 𝒫 V | p = 2 → N ∈ V → j ∈ dom ⁡ E → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
29 9 28 syl ⊢ G ∈ UMGraph → N ∈ V → j ∈ dom ⁡ E → N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
30 29 imp4b ⊢ G ∈ UMGraph ∧ N ∈ V → j ∈ dom ⁡ E ∧ N ∉ E ⁡ j → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
31 8 30 syl5bi ⊢ G ∈ UMGraph ∧ N ∈ V → j ∈ F → E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
32 31 ralrimiv ⊢ G ∈ UMGraph ∧ N ∈ V → ∀ j ∈ F E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
33 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
34 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ E
35 33 34 syl ⊢ G ∈ UMGraph → Fun ⁡ E
36 35 adantr ⊢ G ∈ UMGraph ∧ N ∈ V → Fun ⁡ E
37 3 ssrab3 ⊢ F ⊆ dom ⁡ E
38 funimass4 ⊢ Fun ⁡ E ∧ F ⊆ dom ⁡ E → E F ⊆ p ∈ 𝒫 V ∖ N | p = 2 ↔ ∀ j ∈ F E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
39 36 37 38 sylancl ⊢ G ∈ UMGraph ∧ N ∈ V → E F ⊆ p ∈ 𝒫 V ∖ N | p = 2 ↔ ∀ j ∈ F E ⁡ j ∈ p ∈ 𝒫 V ∖ N | p = 2
40 32 39 mpbird ⊢ G ∈ UMGraph ∧ N ∈ V → E F ⊆ p ∈ 𝒫 V ∖ N | p = 2
41 4 40 eqsstrrid ⊢ G ∈ UMGraph ∧ N ∈ V → ran ⁡ E ↾ F ⊆ p ∈ 𝒫 V ∖ N | p = 2