Proof of Theorem elwwlks2ons3
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) |
2 | | elwwlks2ons3.v |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
3 | 2 | wwlknon 41053 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ (𝑊 ∈ (2 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶))) |
4 | 3 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ (𝑊 ∈ (2 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶))) |
5 | | wwlknbp2 41063 |
. . . . . . . . . 10
⊢ (𝑊 ∈ (2 WWalkSN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (2 + 1))) |
6 | | 2p1e3 11028 |
. . . . . . . . . . . 12
⊢ (2 + 1) =
3 |
7 | 6 | eqeq2i 2622 |
. . . . . . . . . . 11
⊢
((#‘𝑊) = (2 +
1) ↔ (#‘𝑊) =
3) |
8 | | 1ex 9914 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
V |
9 | 8 | tpid2 4247 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
{0, 1, 2} |
10 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) = 3
→ (0..^(#‘𝑊)) =
(0..^3)) |
11 | | fzo0to3tp 12421 |
. . . . . . . . . . . . . . . . 17
⊢ (0..^3) =
{0, 1, 2} |
12 | 10, 11 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) = 3
→ (0..^(#‘𝑊)) =
{0, 1, 2}) |
13 | 9, 12 | syl5eleqr 2695 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) = 3
→ 1 ∈ (0..^(#‘𝑊))) |
14 | | wrdsymbcl 13173 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ∈
(0..^(#‘𝑊))) →
(𝑊‘1) ∈
(Vtx‘𝐺)) |
15 | 13, 14 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) → (𝑊‘1) ∈ (Vtx‘𝐺)) |
16 | 15 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊‘1) ∈ (Vtx‘𝐺)) |
17 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) → (#‘𝑊) = 3) |
18 | 17 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (#‘𝑊) = 3) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → (#‘𝑊) = 3) |
20 | | simpl 472 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → (𝑊‘0) = 𝐴) |
21 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → (𝑊‘1) = (𝑊‘1)) |
22 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → (𝑊‘2) = 𝐶) |
23 | 20, 21, 22 | 3jca 1235 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)) |
24 | 23 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)) |
25 | 24 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)) |
26 | 2 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Vtx‘𝐺) =
𝑉 |
27 | 26 | wrdeqi 13183 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ Word
(Vtx‘𝐺) = Word 𝑉 |
28 | 27 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ Word (Vtx‘𝐺) ↔ 𝑊 ∈ Word 𝑉) |
29 | 28 | biimpi 205 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) → 𝑊 ∈ Word 𝑉) |
31 | 30 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑊 ∈ Word 𝑉) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → 𝑊 ∈ Word 𝑉) |
33 | | simpl32 1136 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → 𝐴 ∈ 𝑉) |
34 | 26 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊‘1) ∈
(Vtx‘𝐺) ↔ (𝑊‘1) ∈ 𝑉) |
35 | 34 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊‘1) ∈
(Vtx‘𝐺) → (𝑊‘1) ∈ 𝑉) |
36 | 35 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → (𝑊‘1) ∈ 𝑉) |
37 | | simpl33 1137 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → 𝐶 ∈ 𝑉) |
38 | | eqwrds3 13552 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ (𝑊‘1) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)))) |
39 | 32, 33, 36, 37, 38 | syl13anc 1320 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = (𝑊‘1) ∧ (𝑊‘2) = 𝐶)))) |
40 | 19, 25, 39 | mpbir2and 959 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) |
41 | 40, 36 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑊‘1) ∈ (Vtx‘𝐺)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)) |
42 | 16, 41 | mpdan 699 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) ∧ (𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)) |
43 | 42 | 3exp 1256 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = 3) → (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)))) |
44 | 7, 43 | sylan2b 491 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (2 + 1)) → (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)))) |
45 | 5, 44 | syl 17 |
. . . . . . . . 9
⊢ (𝑊 ∈ (2 WWalkSN 𝐺) → (((𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)))) |
46 | 45 | 3impib 1254 |
. . . . . . . 8
⊢ ((𝑊 ∈ (2 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉))) |
47 | 46 | com12 32 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ∈ (2 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘2) = 𝐶) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉))) |
48 | 4, 47 | sylbid 229 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉))) |
49 | 48 | imp 444 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)) |
50 | | anass 679 |
. . . . 5
⊢ (((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) ∧ (𝑊‘1) ∈ 𝑉) ↔ (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉))) |
51 | 1, 49, 50 | sylanbrc 695 |
. . . 4
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → ((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) ∧ (𝑊‘1) ∈ 𝑉)) |
52 | | simpr 476 |
. . . . 5
⊢ (((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) ∧ (𝑊‘1) ∈ 𝑉) → (𝑊‘1) ∈ 𝑉) |
53 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝑏 = (𝑊‘1) → 𝐴 = 𝐴) |
54 | | id 22 |
. . . . . . . 8
⊢ (𝑏 = (𝑊‘1) → 𝑏 = (𝑊‘1)) |
55 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝑏 = (𝑊‘1) → 𝐶 = 𝐶) |
56 | 53, 54, 55 | s3eqd 13460 |
. . . . . . 7
⊢ (𝑏 = (𝑊‘1) → 〈“𝐴𝑏𝐶”〉 = 〈“𝐴(𝑊‘1)𝐶”〉) |
57 | | eqeq2 2621 |
. . . . . . . 8
⊢
(〈“𝐴𝑏𝐶”〉 = 〈“𝐴(𝑊‘1)𝐶”〉 → (𝑊 = 〈“𝐴𝑏𝐶”〉 ↔ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉)) |
58 | | eleq1 2676 |
. . . . . . . 8
⊢
(〈“𝐴𝑏𝐶”〉 = 〈“𝐴(𝑊‘1)𝐶”〉 → (〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 〈“𝐴(𝑊‘1)𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
59 | 57, 58 | anbi12d 743 |
. . . . . . 7
⊢
(〈“𝐴𝑏𝐶”〉 = 〈“𝐴(𝑊‘1)𝐶”〉 → ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) ↔ (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ 〈“𝐴(𝑊‘1)𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))) |
60 | 56, 59 | syl 17 |
. . . . . 6
⊢ (𝑏 = (𝑊‘1) → ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) ↔ (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ 〈“𝐴(𝑊‘1)𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))) |
61 | 60 | adantl 481 |
. . . . 5
⊢ ((((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) ∧ (𝑊‘1) ∈ 𝑉) ∧ 𝑏 = (𝑊‘1)) → ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) ↔ (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ 〈“𝐴(𝑊‘1)𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))) |
62 | | simpr 476 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) → 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) |
63 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 〈“𝐴(𝑊‘1)𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
64 | 63 | biimpac 502 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) → 〈“𝐴(𝑊‘1)𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) |
65 | 62, 64 | jca 553 |
. . . . . 6
⊢ ((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ 〈“𝐴(𝑊‘1)𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
66 | 65 | adantr 480 |
. . . . 5
⊢ (((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) ∧ (𝑊‘1) ∈ 𝑉) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ 〈“𝐴(𝑊‘1)𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
67 | 52, 61, 66 | rspcedvd 3289 |
. . . 4
⊢ (((𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ∧ 𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉) ∧ (𝑊‘1) ∈ 𝑉) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
68 | 51, 67 | syl 17 |
. . 3
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
69 | 68 | ex 449 |
. 2
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))) |
70 | | eleq1 2676 |
. . . . . 6
⊢
(〈“𝐴𝑏𝐶”〉 = 𝑊 → (〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
71 | 70 | eqcoms 2618 |
. . . . 5
⊢ (𝑊 = 〈“𝐴𝑏𝐶”〉 → (〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
72 | 71 | biimpa 500 |
. . . 4
⊢ ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) |
73 | 72 | a1i 11 |
. . 3
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
74 | 73 | rexlimdvw 3016 |
. 2
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → 𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
75 | 69, 74 | impbid 201 |
1
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)))) |