Proof of Theorem usgra2wlkspthlem2
Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 2
→ (0...(#‘𝐹)) =
(0...2)) |
2 | 1 | feq2d 5944 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...2)⟶𝑉)) |
3 | | fz0tp 12309 |
. . . . . . . . . . . . . . 15
⊢ (0...2) =
{0, 1, 2} |
4 | 3 | feq2i 5950 |
. . . . . . . . . . . . . 14
⊢ (𝑃:(0...2)⟶𝑉 ↔ 𝑃:{0, 1, 2}⟶𝑉) |
5 | 4 | biimpi 205 |
. . . . . . . . . . . . 13
⊢ (𝑃:(0...2)⟶𝑉 → 𝑃:{0, 1, 2}⟶𝑉) |
6 | 2, 5 | syl6bi 242 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃:{0, 1, 2}⟶𝑉)) |
7 | 6 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) → (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃:{0, 1, 2}⟶𝑉)) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃:{0, 1, 2}⟶𝑉)) |
9 | 8 | impcom 445 |
. . . . . . . . 9
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) → 𝑃:{0, 1, 2}⟶𝑉) |
10 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) → ((𝑃‘0) = (𝑃‘2) ↔ 𝐴 = 𝐵)) |
11 | 10 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) → ((𝑃‘0) = (𝑃‘2) → 𝐴 = 𝐵)) |
12 | 11 | necon3d 2803 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) → (𝐴 ≠ 𝐵 → (𝑃‘0) ≠ (𝑃‘2))) |
13 | 12 | 3impia 1253 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) → (𝑃‘0) ≠ (𝑃‘2)) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2)) |
15 | 14 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) → (𝑃‘0) ≠ (𝑃‘2)) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ Word
dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) ∧ 𝑃:(0...2)⟶𝑉) → (𝑃‘0) ≠ (𝑃‘2)) |
17 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) → 𝑉 USGrph 𝐸) |
18 | | usgrafun 25878 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
19 | | wrdf 13165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
20 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
21 | 20 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ↔ 𝐹:(0..^2)⟶dom 𝐸)) |
22 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 0 ∈
V |
23 | 22 | prid1 4241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
{0, 1} |
24 | | fzo0to2pr 12420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0..^2) =
{0, 1} |
25 | 23, 24 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
(0..^2) |
26 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:(0..^2)⟶dom 𝐸 ∧ 0 ∈ (0..^2)) →
(𝐹‘0) ∈ dom
𝐸) |
27 | 25, 26 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹:(0..^2)⟶dom 𝐸 → (𝐹‘0) ∈ dom 𝐸) |
28 | 21, 27 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → (𝐹‘0) ∈ dom 𝐸)) |
29 | 19, 28 | mpan9 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) → (𝐹‘0) ∈ dom 𝐸) |
30 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Fun
𝐸 ∧ (𝐹‘0) ∈ dom 𝐸) → (𝐸‘(𝐹‘0)) ∈ ran 𝐸) |
31 | 18, 29, 30 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) → (𝐸‘(𝐹‘0)) ∈ ran 𝐸) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) → (𝐸‘(𝐹‘0)) ∈ ran 𝐸) |
33 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → ((𝐸‘(𝐹‘0)) ∈ ran 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸)) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) → ((𝐸‘(𝐹‘0)) ∈ ran 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸)) |
35 | 32, 34 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) → {(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸) |
36 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑃‘0), (𝑃‘1)} ∈ ran 𝐸) → (𝑃‘0) ≠ (𝑃‘1)) |
37 | 17, 35, 36 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) → (𝑃‘0) ≠ (𝑃‘1)) |
38 | 37 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} → (𝑃‘0) ≠ (𝑃‘1))) |
39 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → 𝑉 USGrph 𝐸) |
40 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
V |
41 | 40 | prid2 4242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
{0, 1} |
42 | 41, 24 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 1 ∈
(0..^2) |
43 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:(0..^2)⟶dom 𝐸 ∧ 1 ∈ (0..^2)) →
(𝐹‘1) ∈ dom
𝐸) |
44 | 42, 43 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹:(0..^2)⟶dom 𝐸 → (𝐹‘1) ∈ dom 𝐸) |
45 | 21, 44 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → (𝐹‘1) ∈ dom 𝐸)) |
46 | 19, 45 | mpan9 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) → (𝐹‘1) ∈ dom 𝐸) |
47 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Fun
𝐸 ∧ (𝐹‘1) ∈ dom 𝐸) → (𝐸‘(𝐹‘1)) ∈ ran 𝐸) |
48 | 18, 46, 47 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) → (𝐸‘(𝐹‘1)) ∈ ran 𝐸) |
49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐸‘(𝐹‘1)) ∈ ran 𝐸) |
50 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → ((𝐸‘(𝐹‘1)) ∈ ran 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸)) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝐸‘(𝐹‘1)) ∈ ran 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸)) |
52 | 49, 51 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸) |
53 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ ran 𝐸) → (𝑃‘1) ≠ (𝑃‘2)) |
54 | 39, 52, 53 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘1) ≠ (𝑃‘2)) |
55 | 54 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) → ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} → (𝑃‘1) ≠ (𝑃‘2))) |
56 | 38, 55 | anim12d 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)))) |
57 | 56 | adantld 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)))) |
58 | 57 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐹 ∈ Word
dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) ∧ 𝑃:(0...2)⟶𝑉) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2))) |
60 | | 3anan12 1044 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ↔ ((𝑃‘0) ≠ (𝑃‘2) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2)))) |
61 | 16, 59, 60 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹 ∈ Word
dom 𝐸 ∧ (#‘𝐹) = 2) ∧ 𝑉 USGrph 𝐸) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) ∧ 𝑃:(0...2)⟶𝑉) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))) |
62 | 61 | exp41 636 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) → (𝑉 USGrph 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃:(0...2)⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)))))) |
63 | 62 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃:(0...2)⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))))) |
64 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 2
→ (𝑃‘(#‘𝐹)) = (𝑃‘2)) |
65 | 64 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ ((𝑃‘(#‘𝐹)) = 𝐵 ↔ (𝑃‘2) = 𝐵)) |
66 | 65 | 3anbi2d 1396 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ (((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ ((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵))) |
67 | 20, 24 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
68 | 67 | raleqdv 3121 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ {0, 1} (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
69 | | 2wlklem 26094 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ∈
{0, 1} (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
70 | 68, 69 | syl6bb 275 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
71 | 66, 70 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 2
→ ((((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
72 | 2 | imbi1d 330 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 2
→ ((𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))) ↔ (𝑃:(0...2)⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))))) |
73 | 71, 72 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 2
→ (((((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)))) ↔ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃:(0...2)⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)))))) |
74 | 73 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) → (((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)))) ↔ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃:(0...2)⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)))))) |
75 | 63, 74 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))))) |
76 | 75 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)))) |
77 | 76 | impcom 445 |
. . . . . . . . 9
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))) |
78 | | 2z 11286 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
79 | 22, 40, 78 | 3pm3.2i 1232 |
. . . . . . . . . . 11
⊢ (0 ∈
V ∧ 1 ∈ V ∧ 2 ∈ ℤ) |
80 | | 0ne1 10965 |
. . . . . . . . . . . 12
⊢ 0 ≠
1 |
81 | | 0ne2 11116 |
. . . . . . . . . . . 12
⊢ 0 ≠
2 |
82 | | 1ne2 11117 |
. . . . . . . . . . . 12
⊢ 1 ≠
2 |
83 | 80, 81, 82 | 3pm3.2i 1232 |
. . . . . . . . . . 11
⊢ (0 ≠ 1
∧ 0 ≠ 2 ∧ 1 ≠ 2) |
84 | 79, 83 | pm3.2i 470 |
. . . . . . . . . 10
⊢ ((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (0 ≠ 1 ∧ 0 ≠
2 ∧ 1 ≠ 2)) |
85 | | eqid 2610 |
. . . . . . . . . . 11
⊢ {0, 1, 2}
= {0, 1, 2} |
86 | 85 | f13dfv 6430 |
. . . . . . . . . 10
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (0 ≠ 1 ∧ 0 ≠
2 ∧ 1 ≠ 2)) → (𝑃:{0, 1, 2}–1-1→𝑉 ↔ (𝑃:{0, 1, 2}⟶𝑉 ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))))) |
87 | 84, 86 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) → (𝑃:{0, 1, 2}–1-1→𝑉 ↔ (𝑃:{0, 1, 2}⟶𝑉 ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2))))) |
88 | 9, 77, 87 | mpbir2and 959 |
. . . . . . . 8
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) → 𝑃:{0, 1, 2}–1-1→𝑉) |
89 | | df-f1 5809 |
. . . . . . . 8
⊢ (𝑃:{0, 1, 2}–1-1→𝑉 ↔ (𝑃:{0, 1, 2}⟶𝑉 ∧ Fun ◡𝑃)) |
90 | 88, 89 | sylib 207 |
. . . . . . 7
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) → (𝑃:{0, 1, 2}⟶𝑉 ∧ Fun ◡𝑃)) |
91 | 90 | simprd 478 |
. . . . . 6
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) → Fun ◡𝑃) |
92 | 91 | expcom 450 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑃:(0...(#‘𝐹))⟶𝑉 → Fun ◡𝑃)) |
93 | 92 | ex 449 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃:(0...(#‘𝐹))⟶𝑉 → Fun ◡𝑃))) |
94 | 93 | com23 84 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2)) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝑃))) |
95 | 94 | impancom 455 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝑃))) |
96 | 95 | impcom 445 |
1
⊢ (((𝐹 ∈ Word dom 𝐸 ∧ (#‘𝐹) = 2) ∧ (𝑉 USGrph 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝑃)) |