Metamath Proof Explorer


Theorem vtxdginducedm1lem4

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

Ref Expression
Hypotheses vtxdginducedm1.v 𝑉 = ( Vtx ‘ 𝐺 )
vtxdginducedm1.e 𝐸 = ( iEdg ‘ 𝐺 )
vtxdginducedm1.k 𝐾 = ( 𝑉 ∖ { 𝑁 } )
vtxdginducedm1.i 𝐼 = { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) }
vtxdginducedm1.p 𝑃 = ( 𝐸𝐼 )
vtxdginducedm1.s 𝑆 = ⟨ 𝐾 , 𝑃
vtxdginducedm1.j 𝐽 = { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) }
Assertion vtxdginducedm1lem4 ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ♯ ‘ { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } ) = 0 )

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdginducedm1.e 𝐸 = ( iEdg ‘ 𝐺 )
3 vtxdginducedm1.k 𝐾 = ( 𝑉 ∖ { 𝑁 } )
4 vtxdginducedm1.i 𝐼 = { 𝑖 ∈ dom 𝐸𝑁 ∉ ( 𝐸𝑖 ) }
5 vtxdginducedm1.p 𝑃 = ( 𝐸𝐼 )
6 vtxdginducedm1.s 𝑆 = ⟨ 𝐾 , 𝑃
7 vtxdginducedm1.j 𝐽 = { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) }
8 fveq2 ( 𝑖 = 𝑘 → ( 𝐸𝑖 ) = ( 𝐸𝑘 ) )
9 8 eleq2d ( 𝑖 = 𝑘 → ( 𝑁 ∈ ( 𝐸𝑖 ) ↔ 𝑁 ∈ ( 𝐸𝑘 ) ) )
10 9 7 elrab2 ( 𝑘𝐽 ↔ ( 𝑘 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑘 ) ) )
11 eldifsn ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝑊𝑉𝑊𝑁 ) )
12 df-ne ( 𝑊𝑁 ↔ ¬ 𝑊 = 𝑁 )
13 eleq2 ( ( 𝐸𝑘 ) = { 𝑊 } → ( 𝑁 ∈ ( 𝐸𝑘 ) ↔ 𝑁 ∈ { 𝑊 } ) )
14 elsni ( 𝑁 ∈ { 𝑊 } → 𝑁 = 𝑊 )
15 14 eqcomd ( 𝑁 ∈ { 𝑊 } → 𝑊 = 𝑁 )
16 13 15 syl6bi ( ( 𝐸𝑘 ) = { 𝑊 } → ( 𝑁 ∈ ( 𝐸𝑘 ) → 𝑊 = 𝑁 ) )
17 16 com12 ( 𝑁 ∈ ( 𝐸𝑘 ) → ( ( 𝐸𝑘 ) = { 𝑊 } → 𝑊 = 𝑁 ) )
18 17 con3rr3 ( ¬ 𝑊 = 𝑁 → ( 𝑁 ∈ ( 𝐸𝑘 ) → ¬ ( 𝐸𝑘 ) = { 𝑊 } ) )
19 12 18 sylbi ( 𝑊𝑁 → ( 𝑁 ∈ ( 𝐸𝑘 ) → ¬ ( 𝐸𝑘 ) = { 𝑊 } ) )
20 11 19 simplbiim ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( 𝑁 ∈ ( 𝐸𝑘 ) → ¬ ( 𝐸𝑘 ) = { 𝑊 } ) )
21 20 com12 ( 𝑁 ∈ ( 𝐸𝑘 ) → ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ ( 𝐸𝑘 ) = { 𝑊 } ) )
22 10 21 simplbiim ( 𝑘𝐽 → ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ ( 𝐸𝑘 ) = { 𝑊 } ) )
23 22 impcom ( ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑘𝐽 ) → ¬ ( 𝐸𝑘 ) = { 𝑊 } )
24 23 ralrimiva ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ∀ 𝑘𝐽 ¬ ( 𝐸𝑘 ) = { 𝑊 } )
25 rabeq0 ( { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } = ∅ ↔ ∀ 𝑘𝐽 ¬ ( 𝐸𝑘 ) = { 𝑊 } )
26 24 25 sylibr ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } = ∅ )
27 2 fvexi 𝐸 ∈ V
28 27 dmex dom 𝐸 ∈ V
29 7 28 rab2ex { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } ∈ V
30 hasheq0 ( { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } ∈ V → ( ( ♯ ‘ { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } ) = 0 ↔ { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } = ∅ ) )
31 29 30 ax-mp ( ( ♯ ‘ { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } ) = 0 ↔ { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } = ∅ )
32 26 31 sylibr ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ♯ ‘ { 𝑘𝐽 ∣ ( 𝐸𝑘 ) = { 𝑊 } } ) = 0 )