Proof of Theorem usgra2wlkspthlem1
Step | Hyp | Ref
| Expression |
1 | | wrdf 13165 |
. . 3
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
2 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
3 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
4 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
5 | | fzo0to2pr 12420 |
. . . . . . . . . . . . . . . 16
⊢ (0..^2) =
{0, 1} |
6 | 4, 5 | syl6req 2661 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ {0, 1} = (0..^(#‘𝐹))) |
7 | 6 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) = 2
∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → {0, 1} = (0..^(#‘𝐹))) |
8 | 7 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → {0, 1} = (0..^(#‘𝐹))) |
9 | 8 | feq2d 5944 |
. . . . . . . . . . . 12
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝐹:{0, 1}⟶dom 𝐸 ↔ 𝐹:(0..^(#‘𝐹))⟶dom 𝐸)) |
10 | 3, 9 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → 𝐹:{0, 1}⟶dom 𝐸) |
11 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) = 𝐴 → {(𝑃‘0), (𝑃‘1)} = {𝐴, (𝑃‘1)}) |
12 | 11 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘0) = 𝐴 → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ↔ (𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)})) |
13 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘2) = 𝐵 → {(𝑃‘1), (𝑃‘2)} = {(𝑃‘1), 𝐵}) |
14 | 13 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘2) = 𝐵 → ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵})) |
15 | 12, 14 | bi2anan9 913 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) ↔ ((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}))) |
16 | 15 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) ↔ ((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}))) |
17 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹‘0) = (𝐹‘1) → (𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1))) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹‘0) = (𝐹‘1) → ((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ↔ (𝐸‘(𝐹‘1)) = {𝐴, (𝑃‘1)})) |
19 | 18 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹‘0) = (𝐹‘1) → (((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}) ↔ ((𝐸‘(𝐹‘1)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}))) |
20 | 19 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘0) = (𝐹‘1) → (((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ ((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵})) ↔ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ ((𝐸‘(𝐹‘1)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵})))) |
21 | | eqtr2 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐸‘(𝐹‘1)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}) → {𝐴, (𝑃‘1)} = {(𝑃‘1), 𝐵}) |
22 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃‘0) ∈
V |
23 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝐴 = (𝑃‘0) → (𝐴 ∈ V ↔ (𝑃‘0) ∈ V)) |
24 | 23 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑃‘0) = 𝐴 → (𝐴 ∈ V ↔ (𝑃‘0) ∈ V)) |
25 | 22, 24 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑃‘0) = 𝐴 → 𝐴 ∈ V) |
26 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃‘1) ∈
V |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑃‘0) = 𝐴 → (𝑃‘1) ∈ V) |
28 | 25, 27 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃‘0) = 𝐴 → (𝐴 ∈ V ∧ (𝑃‘1) ∈ V)) |
29 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑃‘2) = 𝐵 → (𝑃‘1) ∈ V) |
30 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃‘2) ∈
V |
31 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝐵 = (𝑃‘2) → (𝐵 ∈ V ↔ (𝑃‘2) ∈ V)) |
32 | 31 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑃‘2) = 𝐵 → (𝐵 ∈ V ↔ (𝑃‘2) ∈ V)) |
33 | 30, 32 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑃‘2) = 𝐵 → 𝐵 ∈ V) |
34 | 29, 33 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃‘2) = 𝐵 → ((𝑃‘1) ∈ V ∧ 𝐵 ∈ V)) |
35 | 28, 34 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) → ((𝐴 ∈ V ∧ (𝑃‘1) ∈ V) ∧ ((𝑃‘1) ∈ V ∧ 𝐵 ∈ V))) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) → ((𝐴 ∈ V ∧ (𝑃‘1) ∈ V) ∧ ((𝑃‘1) ∈ V ∧ 𝐵 ∈ V))) |
37 | | preq12bg 4326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐴 ∈ V ∧ (𝑃‘1) ∈ V) ∧
((𝑃‘1) ∈ V ∧
𝐵 ∈ V)) → ({𝐴, (𝑃‘1)} = {(𝑃‘1), 𝐵} ↔ ((𝐴 = (𝑃‘1) ∧ (𝑃‘1) = 𝐵) ∨ (𝐴 = 𝐵 ∧ (𝑃‘1) = (𝑃‘1))))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) → ({𝐴, (𝑃‘1)} = {(𝑃‘1), 𝐵} ↔ ((𝐴 = (𝑃‘1) ∧ (𝑃‘1) = 𝐵) ∨ (𝐴 = 𝐵 ∧ (𝑃‘1) = (𝑃‘1))))) |
39 | | eqtr 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 = (𝑃‘1) ∧ (𝑃‘1) = 𝐵) → 𝐴 = 𝐵) |
40 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 = 𝐵 ∧ (𝑃‘1) = (𝑃‘1)) → 𝐴 = 𝐵) |
41 | 39, 40 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐴 = (𝑃‘1) ∧ (𝑃‘1) = 𝐵) ∨ (𝐴 = 𝐵 ∧ (𝑃‘1) = (𝑃‘1))) → 𝐴 = 𝐵) |
42 | 38, 41 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) → ({𝐴, (𝑃‘1)} = {(𝑃‘1), 𝐵} → 𝐴 = 𝐵)) |
43 | 21, 42 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐸‘(𝐹‘1)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) → 𝐴 = 𝐵)) |
44 | 43 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑃‘0) =
𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ ((𝐸‘(𝐹‘1)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵})) → 𝐴 = 𝐵) |
45 | 20, 44 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘0) = (𝐹‘1) → (((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ ((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵})) → 𝐴 = 𝐵)) |
46 | 45 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑃‘0) =
𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ ((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵})) → ((𝐹‘0) = (𝐹‘1) → 𝐴 = 𝐵)) |
47 | 46 | necon3d 2803 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑃‘0) =
𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ ((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵})) → (𝐴 ≠ 𝐵 → (𝐹‘0) ≠ (𝐹‘1))) |
48 | 47 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑃‘0) =
𝐴 ∧ (𝑃‘2) = 𝐵) ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ ((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵})) → (𝐹:(0..^2)⟶dom 𝐸 → (𝐴 ≠ 𝐵 → (𝐹‘0) ≠ (𝐹‘1)))) |
49 | 48 | exp31 628 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) → (((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}) → (𝐹:(0..^2)⟶dom 𝐸 → (𝐴 ≠ 𝐵 → (𝐹‘0) ≠ (𝐹‘1)))))) |
50 | 49 | com25 97 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵) → (𝐴 ≠ 𝐵 → (((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}) → (𝐹:(0..^2)⟶dom 𝐸 → (((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (𝐹‘0) ≠ (𝐹‘1)))))) |
51 | 50 | 3impia 1253 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) → (((𝐸‘(𝐹‘0)) = {𝐴, (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), 𝐵}) → (𝐹:(0..^2)⟶dom 𝐸 → (((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (𝐹‘0) ≠ (𝐹‘1))))) |
52 | 16, 51 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹:(0..^2)⟶dom 𝐸 → (((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (𝐹‘0) ≠ (𝐹‘1))))) |
53 | 52 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝐹:(0..^2)⟶dom 𝐸 → (((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (𝐹‘0) ≠ (𝐹‘1)))) |
54 | 53 | com13 86 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) = 2
∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (𝐹:(0..^2)⟶dom 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝐹‘0) ≠ (𝐹‘1)))) |
55 | 4 | feq2d 5944 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ↔ 𝐹:(0..^2)⟶dom 𝐸)) |
56 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 2
→ (𝑃‘(#‘𝐹)) = (𝑃‘2)) |
57 | 56 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) = 2
→ ((𝑃‘(#‘𝐹)) = 𝐵 ↔ (𝑃‘2) = 𝐵)) |
58 | 57 | 3anbi2d 1396 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) = 2
→ (((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ ((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵))) |
59 | 4, 5 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
60 | 59 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) = 2
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ {0, 1} (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
61 | | 2wlklem 26094 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑖 ∈
{0, 1} (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
62 | 60, 61 | syl6bb 275 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) = 2
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
63 | 58, 62 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 2
→ ((((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
64 | 63 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (((((𝑃‘0) =
𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐹‘0) ≠ (𝐹‘1)) ↔ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝐹‘0) ≠ (𝐹‘1)))) |
65 | 55, 64 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐹‘0) ≠ (𝐹‘1))) ↔ (𝐹:(0..^2)⟶dom 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝐹‘0) ≠ (𝐹‘1))))) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) = 2
∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐹‘0) ≠ (𝐹‘1))) ↔ (𝐹:(0..^2)⟶dom 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘2) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝐹‘0) ≠ (𝐹‘1))))) |
67 | 54, 66 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
(((#‘𝐹) = 2
∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐹‘0) ≠ (𝐹‘1)))) |
68 | 67 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐹‘0) ≠ (𝐹‘1))) |
69 | 68 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝐹‘0) ≠ (𝐹‘1)) |
70 | 10, 69 | jca 553 |
. . . . . . . . . 10
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝐹:{0, 1}⟶dom 𝐸 ∧ (𝐹‘0) ≠ (𝐹‘1))) |
71 | | c0ex 9913 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
72 | | 1ex 9914 |
. . . . . . . . . . . . 13
⊢ 1 ∈
V |
73 | 71, 72 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (0 ∈
V ∧ 1 ∈ V) |
74 | | 0ne1 10965 |
. . . . . . . . . . . 12
⊢ 0 ≠
1 |
75 | 73, 74 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ ((0
∈ V ∧ 1 ∈ V) ∧ 0 ≠ 1) |
76 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ {0, 1} =
{0, 1} |
77 | 76 | f12dfv 6429 |
. . . . . . . . . . 11
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ 0 ≠ 1) → (𝐹:{0, 1}–1-1→dom 𝐸 ↔ (𝐹:{0, 1}⟶dom 𝐸 ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
78 | 75, 77 | mp1i 13 |
. . . . . . . . . 10
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝐹:{0, 1}–1-1→dom 𝐸 ↔ (𝐹:{0, 1}⟶dom 𝐸 ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
79 | 70, 78 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → 𝐹:{0, 1}–1-1→dom 𝐸) |
80 | | df-f1 5809 |
. . . . . . . . 9
⊢ (𝐹:{0, 1}–1-1→dom 𝐸 ↔ (𝐹:{0, 1}⟶dom 𝐸 ∧ Fun ◡𝐹)) |
81 | 79, 80 | sylib 207 |
. . . . . . . 8
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝐹:{0, 1}⟶dom 𝐸 ∧ Fun ◡𝐹)) |
82 | 81 | simprd 478 |
. . . . . . 7
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) ∧ (((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → Fun ◡𝐹) |
83 | 82 | ex 449 |
. . . . . 6
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ((#‘𝐹) = 2 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸)) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝐹)) |
84 | 83 | expcom 450 |
. . . . 5
⊢
(((#‘𝐹) = 2
∧ 𝐸:dom 𝐸–1-1→ran 𝐸) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝐹))) |
85 | 84 | ex 449 |
. . . 4
⊢
((#‘𝐹) = 2
→ (𝐸:dom 𝐸–1-1→ran 𝐸 → (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝐹)))) |
86 | 85 | com13 86 |
. . 3
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → (𝐸:dom 𝐸–1-1→ran 𝐸 → ((#‘𝐹) = 2 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝐹)))) |
87 | 1, 86 | syl 17 |
. 2
⊢ (𝐹 ∈ Word dom 𝐸 → (𝐸:dom 𝐸–1-1→ran 𝐸 → ((#‘𝐹) = 2 → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝐹)))) |
88 | 87 | 3imp 1249 |
1
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝐸:dom 𝐸–1-1→ran 𝐸 ∧ (#‘𝐹) = 2) → ((((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → Fun ◡𝐹)) |