Metamath Proof Explorer

Theorem s2elclwwlknon2

Description: Sufficient conditions of a doubleton word to represent a closed walk on vertex X of length 2 . (Contributed by AV, 11-May-2022)

Ref Expression
Hypotheses clwwlknon2.c ⊢ C = ClWWalksNOn ⁡ G
clwwlknon2x.v ⊢ V = Vtx ⁡ G
clwwlknon2x.e ⊢ E = Edg ⁡ G
Assertion s2elclwwlknon2 ⊢ X ∈ V ∧ Y ∈ V ∧ X Y ∈ E → ⟨“ XY ”⟩ ∈ X C 2

Proof

Step Hyp Ref Expression
1 clwwlknon2.c ⊢ C = ClWWalksNOn ⁡ G
2 clwwlknon2x.v ⊢ V = Vtx ⁡ G
3 clwwlknon2x.e ⊢ E = Edg ⁡ G
4 s2cl ⊢ X ∈ V ∧ Y ∈ V → ⟨“ XY ”⟩ ∈ Word V
5 4 3adant3 ⊢ X ∈ V ∧ Y ∈ V ∧ X Y ∈ E → ⟨“ XY ”⟩ ∈ Word V
6 s2len ⊢ ⟨“ XY ”⟩ = 2
7 6 a1i ⊢ X ∈ V ∧ Y ∈ V ∧ X Y ∈ E → ⟨“ XY ”⟩ = 2
8 s2fv0 ⊢ X ∈ V → ⟨“ XY ”⟩ ⁡ 0 = X
9 8 adantr ⊢ X ∈ V ∧ Y ∈ V → ⟨“ XY ”⟩ ⁡ 0 = X
10 s2fv1 ⊢ Y ∈ V → ⟨“ XY ”⟩ ⁡ 1 = Y
11 10 adantl ⊢ X ∈ V ∧ Y ∈ V → ⟨“ XY ”⟩ ⁡ 1 = Y
12 9 11 preq12d ⊢ X ∈ V ∧ Y ∈ V → ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1 = X Y
13 12 eqcomd ⊢ X ∈ V ∧ Y ∈ V → X Y = ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1
14 13 eleq1d ⊢ X ∈ V ∧ Y ∈ V → X Y ∈ E ↔ ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1 ∈ E
15 14 biimp3a ⊢ X ∈ V ∧ Y ∈ V ∧ X Y ∈ E → ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1 ∈ E
16 9 3adant3 ⊢ X ∈ V ∧ Y ∈ V ∧ X Y ∈ E → ⟨“ XY ”⟩ ⁡ 0 = X
17 7 15 16 3jca ⊢ X ∈ V ∧ Y ∈ V ∧ X Y ∈ E → ⟨“ XY ”⟩ = 2 ∧ ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1 ∈ E ∧ ⟨“ XY ”⟩ ⁡ 0 = X
18 fveqeq2 ⊢ w = ⟨“ XY ”⟩ → w = 2 ↔ ⟨“ XY ”⟩ = 2
19 fveq1 ⊢ w = ⟨“ XY ”⟩ → w ⁡ 0 = ⟨“ XY ”⟩ ⁡ 0
20 fveq1 ⊢ w = ⟨“ XY ”⟩ → w ⁡ 1 = ⟨“ XY ”⟩ ⁡ 1
21 19 20 preq12d ⊢ w = ⟨“ XY ”⟩ → w ⁡ 0 w ⁡ 1 = ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1
22 21 eleq1d ⊢ w = ⟨“ XY ”⟩ → w ⁡ 0 w ⁡ 1 ∈ E ↔ ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1 ∈ E
23 19 eqeq1d ⊢ w = ⟨“ XY ”⟩ → w ⁡ 0 = X ↔ ⟨“ XY ”⟩ ⁡ 0 = X
24 18 22 23 3anbi123d ⊢ w = ⟨“ XY ”⟩ → w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X ↔ ⟨“ XY ”⟩ = 2 ∧ ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1 ∈ E ∧ ⟨“ XY ”⟩ ⁡ 0 = X
25 1 2 3 clwwlknon2x ⊢ X C 2 = w ∈ Word V | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ E ∧ w ⁡ 0 = X
26 24 25 elrab2 ⊢ ⟨“ XY ”⟩ ∈ X C 2 ↔ ⟨“ XY ”⟩ ∈ Word V ∧ ⟨“ XY ”⟩ = 2 ∧ ⟨“ XY ”⟩ ⁡ 0 ⟨“ XY ”⟩ ⁡ 1 ∈ E ∧ ⟨“ XY ”⟩ ⁡ 0 = X
27 5 17 26 sylanbrc ⊢ X ∈ V ∧ Y ∈ V ∧ X Y ∈ E → ⟨“ XY ”⟩ ∈ X C 2