Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlknon2.c |
⊢ 𝐶 = ( ClWWalksNOn ‘ 𝐺 ) |
2 |
|
clwwlknon2x.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
3 |
|
clwwlknon2x.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
4 |
|
s2cl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 〈“ 𝑋 𝑌 ”〉 ∈ Word 𝑉 ) |
5 |
4
|
3adant3 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 〈“ 𝑋 𝑌 ”〉 ∈ Word 𝑉 ) |
6 |
|
s2len |
⊢ ( ♯ ‘ 〈“ 𝑋 𝑌 ”〉 ) = 2 |
7 |
6
|
a1i |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ♯ ‘ 〈“ 𝑋 𝑌 ”〉 ) = 2 ) |
8 |
|
s2fv0 |
⊢ ( 𝑋 ∈ 𝑉 → ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) = 𝑋 ) |
9 |
8
|
adantr |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) = 𝑋 ) |
10 |
|
s2fv1 |
⊢ ( 𝑌 ∈ 𝑉 → ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) = 𝑌 ) |
11 |
10
|
adantl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) = 𝑌 ) |
12 |
9 11
|
preq12d |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } = { 𝑋 , 𝑌 } ) |
13 |
12
|
eqcomd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } = { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } ) |
14 |
13
|
eleq1d |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 ↔ { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } ∈ 𝐸 ) ) |
15 |
14
|
biimp3a |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } ∈ 𝐸 ) |
16 |
9
|
3adant3 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) = 𝑋 ) |
17 |
7 15 16
|
3jca |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → ( ( ♯ ‘ 〈“ 𝑋 𝑌 ”〉 ) = 2 ∧ { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } ∈ 𝐸 ∧ ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) = 𝑋 ) ) |
18 |
|
fveqeq2 |
⊢ ( 𝑤 = 〈“ 𝑋 𝑌 ”〉 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 〈“ 𝑋 𝑌 ”〉 ) = 2 ) ) |
19 |
|
fveq1 |
⊢ ( 𝑤 = 〈“ 𝑋 𝑌 ”〉 → ( 𝑤 ‘ 0 ) = ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) ) |
20 |
|
fveq1 |
⊢ ( 𝑤 = 〈“ 𝑋 𝑌 ”〉 → ( 𝑤 ‘ 1 ) = ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) ) |
21 |
19 20
|
preq12d |
⊢ ( 𝑤 = 〈“ 𝑋 𝑌 ”〉 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } ) |
22 |
21
|
eleq1d |
⊢ ( 𝑤 = 〈“ 𝑋 𝑌 ”〉 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ↔ { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } ∈ 𝐸 ) ) |
23 |
19
|
eqeq1d |
⊢ ( 𝑤 = 〈“ 𝑋 𝑌 ”〉 → ( ( 𝑤 ‘ 0 ) = 𝑋 ↔ ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) = 𝑋 ) ) |
24 |
18 22 23
|
3anbi123d |
⊢ ( 𝑤 = 〈“ 𝑋 𝑌 ”〉 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) ↔ ( ( ♯ ‘ 〈“ 𝑋 𝑌 ”〉 ) = 2 ∧ { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } ∈ 𝐸 ∧ ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) = 𝑋 ) ) ) |
25 |
1 2 3
|
clwwlknon2x |
⊢ ( 𝑋 𝐶 2 ) = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝐸 ∧ ( 𝑤 ‘ 0 ) = 𝑋 ) } |
26 |
24 25
|
elrab2 |
⊢ ( 〈“ 𝑋 𝑌 ”〉 ∈ ( 𝑋 𝐶 2 ) ↔ ( 〈“ 𝑋 𝑌 ”〉 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 〈“ 𝑋 𝑌 ”〉 ) = 2 ∧ { ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) , ( 〈“ 𝑋 𝑌 ”〉 ‘ 1 ) } ∈ 𝐸 ∧ ( 〈“ 𝑋 𝑌 ”〉 ‘ 0 ) = 𝑋 ) ) ) |
27 |
5 17 26
|
sylanbrc |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ) → 〈“ 𝑋 𝑌 ”〉 ∈ ( 𝑋 𝐶 2 ) ) |