Theorem rusgr1vtxlem

Description: Lemma for rusgr1vtx . (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Assertion	rusgr1vtxlem	⊢ ( ( ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ 𝐴 ) = 𝐾 ∧ ∀ 𝑣 ∈ 𝑉 𝐴 = ∅ ) ∧ ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 1 ) ) → 𝐾 = 0 )

Proof

Step	Hyp	Ref	Expression
1		r19.26	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ♯ ‘ 𝐴 ) = 𝐾 ∧ 𝐴 = ∅ ) ↔ ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ 𝐴 ) = 𝐾 ∧ ∀ 𝑣 ∈ 𝑉 𝐴 = ∅ ) )
2		fveqeq2	⊢ ( 𝐴 = ∅ → ( ( ♯ ‘ 𝐴 ) = 𝐾 ↔ ( ♯ ‘ ∅ ) = 𝐾 ) )
3	2	biimpac	⊢ ( ( ( ♯ ‘ 𝐴 ) = 𝐾 ∧ 𝐴 = ∅ ) → ( ♯ ‘ ∅ ) = 𝐾 )
4	3	ralimi	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ♯ ‘ 𝐴 ) = 𝐾 ∧ 𝐴 = ∅ ) → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ∅ ) = 𝐾 )
5		hash1n0	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝑉 ≠ ∅ )
6		rspn0	⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ∅ ) = 𝐾 → ( ♯ ‘ ∅ ) = 𝐾 ) )
7	5 6	syl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ∅ ) = 𝐾 → ( ♯ ‘ ∅ ) = 𝐾 ) )
8		hash0	⊢ ( ♯ ‘ ∅ ) = 0
9		eqeq1	⊢ ( ( ♯ ‘ ∅ ) = 𝐾 → ( ( ♯ ‘ ∅ ) = 0 ↔ 𝐾 = 0 ) )
10	8 9	mpbii	⊢ ( ( ♯ ‘ ∅ ) = 𝐾 → 𝐾 = 0 )
11	7 10	syl6com	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ∅ ) = 𝐾 → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝐾 = 0 ) )
12	4 11	syl	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ♯ ‘ 𝐴 ) = 𝐾 ∧ 𝐴 = ∅ ) → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝐾 = 0 ) )
13	1 12	sylbir	⊢ ( ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ 𝐴 ) = 𝐾 ∧ ∀ 𝑣 ∈ 𝑉 𝐴 = ∅ ) → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 1 ) → 𝐾 = 0 ) )
14	13	imp	⊢ ( ( ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ 𝐴 ) = 𝐾 ∧ ∀ 𝑣 ∈ 𝑉 𝐴 = ∅ ) ∧ ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 1 ) ) → 𝐾 = 0 )