Metamath Proof Explorer

Theorem vtxdginducedm1lem4

Description: Lemma 4 for vtxdginducedm1 . (Contributed by AV, 17-Dec-2021)

Ref Expression
Hypotheses vtxdginducedm1.v ⊢ V = Vtx ⁡ G
vtxdginducedm1.e ⊢ E = iEdg ⁡ G
vtxdginducedm1.k ⊢ K = V ∖ N
vtxdginducedm1.i ⊢ I = i ∈ dom ⁡ E | N ∉ E ⁡ i
vtxdginducedm1.p ⊢ P = E ↾ I
vtxdginducedm1.s ⊢ S = K P
vtxdginducedm1.j ⊢ J = i ∈ dom ⁡ E | N ∈ E ⁡ i
Assertion vtxdginducedm1lem4 ⊢ W ∈ V ∖ N → k ∈ J | E ⁡ k = W = 0

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v ⊢ V = Vtx ⁡ G
2 vtxdginducedm1.e ⊢ E = iEdg ⁡ G
3 vtxdginducedm1.k ⊢ K = V ∖ N
4 vtxdginducedm1.i ⊢ I = i ∈ dom ⁡ E | N ∉ E ⁡ i
5 vtxdginducedm1.p ⊢ P = E ↾ I
6 vtxdginducedm1.s ⊢ S = K P
7 vtxdginducedm1.j ⊢ J = i ∈ dom ⁡ E | N ∈ E ⁡ i
8 fveq2 ⊢ i = k → E ⁡ i = E ⁡ k
9 8 eleq2d ⊢ i = k → N ∈ E ⁡ i ↔ N ∈ E ⁡ k
10 9 7 elrab2 ⊢ k ∈ J ↔ k ∈ dom ⁡ E ∧ N ∈ E ⁡ k
11 eldifsn ⊢ W ∈ V ∖ N ↔ W ∈ V ∧ W ≠ N
12 df-ne ⊢ W ≠ N ↔ ¬ W = N
13 eleq2 ⊢ E ⁡ k = W → N ∈ E ⁡ k ↔ N ∈ W
14 elsni ⊢ N ∈ W → N = W
15 14 eqcomd ⊢ N ∈ W → W = N
16 13 15 biimtrdi ⊢ E ⁡ k = W → N ∈ E ⁡ k → W = N
17 16 com12 ⊢ N ∈ E ⁡ k → E ⁡ k = W → W = N
18 17 con3rr3 ⊢ ¬ W = N → N ∈ E ⁡ k → ¬ E ⁡ k = W
19 12 18 sylbi ⊢ W ≠ N → N ∈ E ⁡ k → ¬ E ⁡ k = W
20 11 19 simplbiim ⊢ W ∈ V ∖ N → N ∈ E ⁡ k → ¬ E ⁡ k = W
21 20 com12 ⊢ N ∈ E ⁡ k → W ∈ V ∖ N → ¬ E ⁡ k = W
22 10 21 simplbiim ⊢ k ∈ J → W ∈ V ∖ N → ¬ E ⁡ k = W
23 22 impcom ⊢ W ∈ V ∖ N ∧ k ∈ J → ¬ E ⁡ k = W
24 23 ralrimiva ⊢ W ∈ V ∖ N → ∀ k ∈ J ¬ E ⁡ k = W
25 rabeq0 ⊢ k ∈ J | E ⁡ k = W = ∅ ↔ ∀ k ∈ J ¬ E ⁡ k = W
26 24 25 sylibr ⊢ W ∈ V ∖ N → k ∈ J | E ⁡ k = W = ∅
27 2 fvexi ⊢ E ∈ V
28 27 dmex ⊢ dom ⁡ E ∈ V
29 7 28 rab2ex ⊢ k ∈ J | E ⁡ k = W ∈ V
30 hasheq0 ⊢ k ∈ J | E ⁡ k = W ∈ V → k ∈ J | E ⁡ k = W = 0 ↔ k ∈ J | E ⁡ k = W = ∅
31 29 30 ax-mp ⊢ k ∈ J | E ⁡ k = W = 0 ↔ k ∈ J | E ⁡ k = W = ∅
32 26 31 sylibr ⊢ W ∈ V ∖ N → k ∈ J | E ⁡ k = W = 0