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 ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
Assertion 2clwwlkel ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → W ∈ X C N ↔ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X

Proof

Step Hyp Ref Expression
1 2clwwlk.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
2 1 2clwwlk ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → X C N = w ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X
3 2 eleq2d ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → W ∈ X C N ↔ W ∈ w ∈ X ClWWalksNOn ⁡ G N | 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 ∈ X ClWWalksNOn ⁡ G N | w ⁡ N − 2 = X ↔ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X
7 3 6 bitrdi ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → W ∈ X C N ↔ W ∈ X ClWWalksNOn ⁡ G N ∧ W ⁡ N − 2 = X