Step | Hyp | Ref
| Expression |
1 | | 2wlkonot 26392 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶))}) |
2 | 1 | eleq2d 2673 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ 𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶))})) |
3 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇)) |
4 | 3 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
5 | 4 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) = 𝐴 ↔ (1st
‘(1st ‘𝑇)) = 𝐴)) |
6 | 3 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
7 | 6 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) = (𝑝‘1) ↔ (2nd
‘(1st ‘𝑇)) = (𝑝‘1))) |
8 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
9 | 8 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → ((2nd ‘𝑡) = 𝐶 ↔ (2nd ‘𝑇) = 𝐶)) |
10 | 5, 7, 9 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶) ↔ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) |
11 | 10 | 3anbi3d 1397 |
. . . . 5
⊢ (𝑡 = 𝑇 → ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶)) ↔ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
12 | 11 | 2exbidv 1839 |
. . . 4
⊢ (𝑡 = 𝑇 → (∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶)) ↔ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
13 | 12 | elrab 3331 |
. . 3
⊢ (𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝐴 ∧ (2nd
‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶))} ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
14 | 2, 13 | syl6bb 275 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))) |
15 | | simpl 472 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) |
16 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
17 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑝 ∈ V |
18 | 16, 17 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (𝑓 ∈ V ∧ 𝑝 ∈ V) |
19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑓 ∈ V ∧ 𝑝 ∈ V)) |
20 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
21 | | iswlkon 26062 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶))) |
22 | 15, 19, 20, 21 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶))) |
23 | 22 | 3anbi1d 1395 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) ↔ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
24 | 23 | anbi2d 736 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))) |
25 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → 𝐴 ∈ 𝑉) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (#‘𝑓) = 2) → 𝐴 ∈ 𝑉) |
29 | | el2wlkonotlem 26389 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → (𝑝‘1) ∈ 𝑉) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(𝑉 Walks 𝐸)𝑝 → ((#‘𝑓) = 2 → (𝑝‘1) ∈ 𝑉)) |
31 | 30 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → ((#‘𝑓) = 2 → (𝑝‘1) ∈ 𝑉)) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → ((#‘𝑓) = 2 → (𝑝‘1) ∈ 𝑉)) |
33 | 32 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (#‘𝑓) = 2) → (𝑝‘1) ∈ 𝑉) |
34 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ 𝑉) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉) |
36 | 35 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → 𝐶 ∈ 𝑉) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (#‘𝑓) = 2) → 𝐶 ∈ 𝑉) |
38 | | el2xptp0 7103 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) ↔ 𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉)) |
39 | 28, 33, 37, 38 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (#‘𝑓) = 2) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) ↔ 𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉)) |
40 | | oteq2 4350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑝‘1) = 𝑏 → 〈𝐴, (𝑝‘1), 𝐶〉 = 〈𝐴, 𝑏, 𝐶〉) |
41 | 40 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑏 = (𝑝‘1) → 〈𝐴, (𝑝‘1), 𝐶〉 = 〈𝐴, 𝑏, 𝐶〉) |
42 | 41 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑏 = (𝑝‘1) → (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ↔ 𝑇 = 〈𝐴, 𝑏, 𝐶〉)) |
43 | 42 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → (𝑏 = (𝑝‘1) → 𝑇 = 〈𝐴, 𝑏, 𝐶〉)) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) → (𝑏 = (𝑝‘1) → 𝑇 = 〈𝐴, 𝑏, 𝐶〉)) |
45 | 44 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → (𝑏 = (𝑝‘1) → 𝑇 = 〈𝐴, 𝑏, 𝐶〉)) |
46 | 45 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → 𝑇 = 〈𝐴, 𝑏, 𝐶〉) |
47 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → 𝑓(𝑉 Walks 𝐸)𝑝) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) → 𝑓(𝑉 Walks 𝐸)𝑝) |
49 | 48 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → 𝑓(𝑉 Walks 𝐸)𝑝) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → 𝑓(𝑉 Walks 𝐸)𝑝) |
51 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → (#‘𝑓) = 2) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) → (#‘𝑓) = 2) |
53 | 52 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → (#‘𝑓) = 2) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → (#‘𝑓) = 2) |
55 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑝‘0) = 𝐴 ↔ 𝐴 = (𝑝‘0)) |
56 | 55 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑝‘0) = 𝐴 → 𝐴 = (𝑝‘0)) |
57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → 𝐴 = (𝑝‘0)) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → 𝐴 = (𝑝‘0)) |
59 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → 𝑏 = (𝑝‘1)) |
60 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((#‘𝑓) = 2
→ (𝑝‘(#‘𝑓)) = (𝑝‘2)) |
61 | 60 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝑓) = 2
→ ((𝑝‘(#‘𝑓)) = 𝐶 ↔ (𝑝‘2) = 𝐶)) |
62 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑝‘2) = 𝐶 ↔ 𝐶 = (𝑝‘2)) |
63 | 62 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑝‘2) = 𝐶 → 𝐶 = (𝑝‘2)) |
64 | 61, 63 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝑓) = 2
→ ((𝑝‘(#‘𝑓)) = 𝐶 → 𝐶 = (𝑝‘2))) |
65 | 64 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((𝑝‘(#‘𝑓)) = 𝐶 → 𝐶 = (𝑝‘2))) |
66 | 65 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) → ((𝑝‘(#‘𝑓)) = 𝐶 → 𝐶 = (𝑝‘2))) |
67 | 66 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) → 𝐶 = (𝑝‘2)) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → 𝐶 = (𝑝‘2)) |
69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → 𝐶 = (𝑝‘2)) |
70 | 58, 59, 69 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) |
71 | 50, 54, 70 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
72 | 46, 71 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑏 = (𝑝‘1) ∧ (((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴)) → (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
73 | 72 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑏 = (𝑝‘1) → ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) ∧ 𝑏 = (𝑝‘1)) → ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
75 | 29, 74 | rspcimedv 3284 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
76 | 75 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2)) ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (𝑝‘0) = 𝐴) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
77 | 76 | exp41 636 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((𝑝‘(#‘𝑓)) = 𝐶 → ((𝑝‘0) = 𝐴 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))) |
78 | 77 | com15 99 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((𝑝‘(#‘𝑓)) = 𝐶 → ((𝑝‘0) = 𝐴 → (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))) |
79 | 78 | pm2.43i 50 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((𝑝‘(#‘𝑓)) = 𝐶 → ((𝑝‘0) = 𝐴 → (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))))) |
80 | 79 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓(𝑉 Walks 𝐸)𝑝 → ((#‘𝑓) = 2 → ((𝑝‘(#‘𝑓)) = 𝐶 → ((𝑝‘0) = 𝐴 → (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))) |
81 | 80 | com24 93 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(𝑉 Walks 𝐸)𝑝 → ((𝑝‘0) = 𝐴 → ((𝑝‘(#‘𝑓)) = 𝐶 → ((#‘𝑓) = 2 → (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))) |
82 | 81 | 3imp 1249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → ((#‘𝑓) = 2 → (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → ((#‘𝑓) = 2 → (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))) |
84 | 83 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (#‘𝑓) = 2) → (𝑇 = 〈𝐴, (𝑝‘1), 𝐶〉 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
85 | 39, 84 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (#‘𝑓) = 2) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
86 | 85 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → ((#‘𝑓) = 2 → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))) |
87 | 86 | com23 84 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) → ((#‘𝑓) = 2 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))) |
88 | 87 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) → ((#‘𝑓) = 2 → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))))) |
89 | 88 | com4t 91 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) → ((#‘𝑓) = 2 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))))) |
90 | 89 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → (((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶) → ((#‘𝑓) = 2 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))) |
91 | 90 | com14 94 |
. . . . . . . . . . 11
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → (((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶) → ((#‘𝑓) = 2 → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))) |
92 | 91 | com23 84 |
. . . . . . . . . 10
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → ((#‘𝑓) = 2 → (((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))) |
93 | 92 | 3imp 1249 |
. . . . . . . . 9
⊢ (((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))) |
94 | 93 | impcom 445 |
. . . . . . . 8
⊢ ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
95 | 94 | com12 32 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) → ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
96 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
97 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉) |
98 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝐶 ∈ 𝑉) |
99 | 96, 97, 98 | 3jca 1235 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
100 | | otel3xp 5077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) |
101 | 99, 100 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉)) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) |
102 | 101 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))) |
104 | 103 | com12 32 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))) |
105 | 104 | adantll 746 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))) |
106 | 105 | imp 444 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) |
107 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑓(𝑉 Walks 𝐸)𝑝 → 𝑓(𝑉 Walks 𝐸)𝑝) |
108 | 107 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(𝑉 Walks 𝐸)𝑝) |
109 | 108 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑓(𝑉 Walks 𝐸)𝑝) |
110 | 109 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → 𝑓(𝑉 Walks 𝐸)𝑝) |
111 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = (𝑝‘0) ↔ (𝑝‘0) = 𝐴) |
112 | 111 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = (𝑝‘0) → (𝑝‘0) = 𝐴) |
113 | 112 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝‘0) = 𝐴) |
114 | 113 | 3ad2ant3 1077 |
. . . . . . . . . . . . . 14
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝‘0) = 𝐴) |
115 | 114 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝‘0) = 𝐴) |
116 | 115 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑝‘0) = 𝐴) |
117 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐶 = (𝑝‘2) ↔ (𝑝‘2) = 𝐶) |
118 | 117 | biimpi 205 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 = (𝑝‘2) → (𝑝‘2) = 𝐶) |
119 | 118 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝‘2) = 𝐶) |
120 | 119, 61 | syl5ibr 235 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑓) = 2
→ ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝‘(#‘𝑓)) = 𝐶)) |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑓(𝑉 Walks 𝐸)𝑝 → ((#‘𝑓) = 2 → ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝‘(#‘𝑓)) = 𝐶))) |
122 | 121 | 3imp 1249 |
. . . . . . . . . . . . . 14
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝‘(#‘𝑓)) = 𝐶) |
123 | 122 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝‘(#‘𝑓)) = 𝐶) |
124 | 123 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑝‘(#‘𝑓)) = 𝐶) |
125 | 110, 116,
124 | 3jca 1235 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶)) |
126 | | id 22 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑓) = 2
→ (#‘𝑓) =
2) |
127 | 126 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (#‘𝑓) = 2) |
128 | 127 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (#‘𝑓) = 2) |
129 | 128 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (#‘𝑓) = 2) |
130 | 99 | adantll 746 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
131 | | oteqimp 7078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 → ((𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶))) |
132 | 130, 131 | syl5 33 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶))) |
133 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑝‘1) → ((2nd
‘(1st ‘𝑇)) = 𝑏 ↔ (2nd
‘(1st ‘𝑇)) = (𝑝‘1))) |
134 | 133 | 3anbi2d 1396 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑝‘1) → (((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶) ↔ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) |
135 | 134 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑝‘1) → (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶)) ↔ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
136 | 132, 135 | syl5ib 233 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑝‘1) → (𝑇 = 〈𝐴, 𝑏, 𝐶〉 → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
137 | 136 | 3ad2ant2 1076 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑇 = 〈𝐴, 𝑏, 𝐶〉 → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
138 | 137 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑇 = 〈𝐴, 𝑏, 𝐶〉 → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
139 | 138 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) |
140 | 139 | impcom 445 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) |
141 | 125, 129,
140 | 3jca 1235 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) |
142 | 106, 141 | jca 553 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
143 | 142 | ex 449 |
. . . . . . . 8
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))) |
144 | 143 | rexlimdva 3013 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))) |
145 | 95, 144 | impbid 201 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
146 | 24, 145 | bitrd 267 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
147 | 146 | 2exbidv 1839 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑓∃𝑝∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
148 | | 19.42vv 1907 |
. . . 4
⊢
(∃𝑓∃𝑝(𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))) |
149 | | rexcom4 3198 |
. . . . 5
⊢
(∃𝑏 ∈
𝑉 ∃𝑓∃𝑝(𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑓∃𝑏 ∈ 𝑉 ∃𝑝(𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
150 | | rexcom4 3198 |
. . . . . 6
⊢
(∃𝑏 ∈
𝑉 ∃𝑝(𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑝∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
151 | 150 | exbii 1764 |
. . . . 5
⊢
(∃𝑓∃𝑏 ∈ 𝑉 ∃𝑝(𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑓∃𝑝∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
152 | 149, 151 | bitr2i 264 |
. . . 4
⊢
(∃𝑓∃𝑝∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑏 ∈ 𝑉 ∃𝑓∃𝑝(𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
153 | 147, 148,
152 | 3bitr3g 301 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑏 ∈ 𝑉 ∃𝑓∃𝑝(𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
154 | | 19.42vv 1907 |
. . . 4
⊢
(∃𝑓∃𝑝(𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
155 | 154 | rexbii 3023 |
. . 3
⊢
(∃𝑏 ∈
𝑉 ∃𝑓∃𝑝(𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
156 | 153, 155 | syl6bb 275 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑇)) = 𝐴 ∧ (2nd
‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
157 | 14, 156 | bitrd 267 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |