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 )