This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( 𝐸 ‘ 𝑘 ) = { 𝑊 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) → 𝑊 = 𝑁 ) )
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 )