Metamath Proof Explorer

Theorem rusgr1vtxlem

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

Ref Expression
Assertion rusgr1vtxlem ⊢∀v∈VA=K∧∀v∈VA=∅∧V∈W∧V=1→K=0

Proof

Step Hyp Ref Expression
1 r19.26 ⊢∀v∈VA=K∧A=∅↔∀v∈VA=K∧∀v∈VA=∅
2 fveqeq2 ⊢A=∅→A=K↔∅=K
3 2 biimpac ⊢A=K∧A=∅→∅=K
4 3 ralimi ⊢∀v∈VA=K∧A=∅→∀v∈V∅=K
5 hash1n0 ⊢V∈W∧V=1→V≠∅
6 rspn0 ⊢V≠∅→∀v∈V∅=K→∅=K
7 5 6 syl ⊢V∈W∧V=1→∀v∈V∅=K→∅=K
8 hash0 ⊢∅=0
9 eqeq1 ⊢∅=K→∅=0↔K=0
10 8 9 mpbii ⊢∅=K→K=0
11 7 10 syl6com ⊢∀v∈V∅=K→V∈W∧V=1→K=0
12 4 11 syl ⊢∀v∈VA=K∧A=∅→V∈W∧V=1→K=0
13 1 12 sylbir ⊢∀v∈VA=K∧∀v∈VA=∅→V∈W∧V=1→K=0
14 13 imp ⊢∀v∈VA=K∧∀v∈VA=∅∧V∈W∧V=1→K=0