Metamath Proof Explorer

Theorem umgrres1lem

Description: Lemma for umgrres1 . (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses upgrres1.v ⊢ V = Vtx ⁡ G
upgrres1.e ⊢ E = Edg ⁡ G
upgrres1.f ⊢ F = e ∈ E | N ∉ e
Assertion umgrres1lem ⊢ G ∈ UMGraph ∧ N ∈ V → ran ⁡ I ↾ F ⊆ p ∈ 𝒫 V ∖ N | p = 2

Proof

Step Hyp Ref Expression
1 upgrres1.v ⊢ V = Vtx ⁡ G
2 upgrres1.e ⊢ E = Edg ⁡ G
3 upgrres1.f ⊢ F = e ∈ E | N ∉ e
4 rnresi ⊢ ran ⁡ I ↾ F = F
5 simpr ⊢ G ∈ UMGraph ∧ N ∈ V ∧ e ∈ E → e ∈ E
6 5 adantr ⊢ G ∈ UMGraph ∧ N ∈ V ∧ e ∈ E ∧ N ∉ e → e ∈ E
7 umgruhgr ⊢ G ∈ UMGraph → G ∈ UHGraph
8 2 eleq2i ⊢ e ∈ E ↔ e ∈ Edg ⁡ G
9 8 biimpi ⊢ e ∈ E → e ∈ Edg ⁡ G
10 edguhgr ⊢ G ∈ UHGraph ∧ e ∈ Edg ⁡ G → e ∈ 𝒫 Vtx ⁡ G
11 elpwi ⊢ e ∈ 𝒫 Vtx ⁡ G → e ⊆ Vtx ⁡ G
12 11 1 sseqtrrdi ⊢ e ∈ 𝒫 Vtx ⁡ G → e ⊆ V
13 10 12 syl ⊢ G ∈ UHGraph ∧ e ∈ Edg ⁡ G → e ⊆ V
14 7 9 13 syl2an ⊢ G ∈ UMGraph ∧ e ∈ E → e ⊆ V
15 14 ad4ant13 ⊢ G ∈ UMGraph ∧ N ∈ V ∧ e ∈ E ∧ N ∉ e → e ⊆ V
16 simpr ⊢ G ∈ UMGraph ∧ N ∈ V ∧ e ∈ E ∧ N ∉ e → N ∉ e
17 elpwdifsn ⊢ e ∈ E ∧ e ⊆ V ∧ N ∉ e → e ∈ 𝒫 V ∖ N
18 6 15 16 17 syl3anc ⊢ G ∈ UMGraph ∧ N ∈ V ∧ e ∈ E ∧ N ∉ e → e ∈ 𝒫 V ∖ N
19 18 ex ⊢ G ∈ UMGraph ∧ N ∈ V ∧ e ∈ E → N ∉ e → e ∈ 𝒫 V ∖ N
20 19 ralrimiva ⊢ G ∈ UMGraph ∧ N ∈ V → ∀ e ∈ E N ∉ e → e ∈ 𝒫 V ∖ N
21 rabss ⊢ e ∈ E | N ∉ e ⊆ 𝒫 V ∖ N ↔ ∀ e ∈ E N ∉ e → e ∈ 𝒫 V ∖ N
22 20 21 sylibr ⊢ G ∈ UMGraph ∧ N ∈ V → e ∈ E | N ∉ e ⊆ 𝒫 V ∖ N
23 3 22 eqsstrid ⊢ G ∈ UMGraph ∧ N ∈ V → F ⊆ 𝒫 V ∖ N
24 elrabi ⊢ p ∈ e ∈ E | N ∉ e → p ∈ E
25 24 2 eleqtrdi ⊢ p ∈ e ∈ E | N ∉ e → p ∈ Edg ⁡ G
26 edgumgr ⊢ G ∈ UMGraph ∧ p ∈ Edg ⁡ G → p ∈ 𝒫 Vtx ⁡ G ∧ p = 2
27 26 simprd ⊢ G ∈ UMGraph ∧ p ∈ Edg ⁡ G → p = 2
28 27 ex ⊢ G ∈ UMGraph → p ∈ Edg ⁡ G → p = 2
29 28 adantr ⊢ G ∈ UMGraph ∧ N ∈ V → p ∈ Edg ⁡ G → p = 2
30 25 29 syl5com ⊢ p ∈ e ∈ E | N ∉ e → G ∈ UMGraph ∧ N ∈ V → p = 2
31 30 3 eleq2s ⊢ p ∈ F → G ∈ UMGraph ∧ N ∈ V → p = 2
32 31 impcom ⊢ G ∈ UMGraph ∧ N ∈ V ∧ p ∈ F → p = 2
33 23 32 ssrabdv ⊢ G ∈ UMGraph ∧ N ∈ V → F ⊆ p ∈ 𝒫 V ∖ N | p = 2
34 4 33 eqsstrid ⊢ G ∈ UMGraph ∧ N ∈ V → ran ⁡ I ↾ F ⊆ p ∈ 𝒫 V ∖ N | p = 2