Metamath Proof Explorer

Theorem 2clwwlkel

Description: Characterization of an element of the value of operation C , i.e., of a word being a double loop of length N on vertex X . (Contributed by Alexander van der Vekens, 24-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 20-Apr-2022)

Ref Expression
Hypothesis 2clwwlk.c ⊢C=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2=v
Assertion 2clwwlkel ⊢X∈V∧N∈ℤ≥2→W∈XCN↔W∈XClWWalksNOn⁡GN∧W⁡N−2=X

Proof

Step Hyp Ref Expression
1 2clwwlk.c ⊢C=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2=v
2 1 2clwwlk ⊢X∈V∧N∈ℤ≥2→XCN=w∈XClWWalksNOn⁡GN|w⁡N−2=X
3 2 eleq2d ⊢X∈V∧N∈ℤ≥2→W∈XCN↔W∈w∈XClWWalksNOn⁡GN|w⁡N−2=X
4 fveq1 ⊢w=W→w⁡N−2=W⁡N−2
5 4 eqeq1d ⊢w=W→w⁡N−2=X↔W⁡N−2=X
6 5 elrab ⊢W∈w∈XClWWalksNOn⁡GN|w⁡N−2=X↔W∈XClWWalksNOn⁡GN∧W⁡N−2=X
7 3 6 bitrdi ⊢X∈V∧N∈ℤ≥2→W∈XCN↔W∈XClWWalksNOn⁡GN∧W⁡N−2=X