Step | Hyp | Ref
| Expression |
1 | | crctprop 26687 |
. . 3
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
2 | | istrl 26593 |
. . . . . . 7
⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹)) |
3 | | uspgrupgr 26071 |
. . . . . . . . 9
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph
) |
4 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
5 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
6 | 4, 5 | upgriswlk 26537 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
7 | | preq2 4269 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃‘2) = (𝑃‘0) → {(𝑃‘1), (𝑃‘2)} = {(𝑃‘1), (𝑃‘0)}) |
8 | | prcom 4267 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {(𝑃‘1), (𝑃‘0)} = {(𝑃‘0), (𝑃‘1)} |
9 | 7, 8 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃‘2) = (𝑃‘0) → {(𝑃‘1), (𝑃‘2)} = {(𝑃‘0), (𝑃‘1)}) |
10 | 9 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘1), (𝑃‘2)} = {(𝑃‘0), (𝑃‘1)}) |
11 | 10 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃‘0) = (𝑃‘2) → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)})) |
12 | 11 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘2) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}))) |
13 | 12 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃‘0) = (𝑃‘2) ∧ ((#‘𝐹) = 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph ))) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}))) |
14 | | eqtr3 2643 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}) → ((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1))) |
15 | 4, 5 | uspgrf 26049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
16 | 15 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
◡𝐹 ∧ 𝐺 ∈ USPGraph ) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
17 | 16 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
19 | | df-f1 5893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ↔ (𝐹:(0..^(#‘𝐹))⟶dom (iEdg‘𝐺) ∧ Fun ◡𝐹)) |
20 | 19 | simplbi2 655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹:(0..^(#‘𝐹))⟶dom (iEdg‘𝐺) → (Fun ◡𝐹 → 𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺))) |
21 | | wrdf 13310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) → 𝐹:(0..^(#‘𝐹))⟶dom (iEdg‘𝐺)) |
22 | 20, 21 | syl11 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
◡𝐹 → (𝐹 ∈ Word dom (iEdg‘𝐺) → 𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺))) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
◡𝐹 ∧ 𝐺 ∈ USPGraph ) → (𝐹 ∈ Word dom (iEdg‘𝐺) → 𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺))) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) → (𝐹 ∈ Word dom
(iEdg‘𝐺) → 𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺))) |
25 | 24 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → 𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺)) |
26 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℕ |
27 | | lbfzo0 12507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (0 ∈
(0..^2) ↔ 2 ∈ ℕ) |
28 | 26, 27 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
(0..^2) |
29 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℕ0 |
30 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 <
2 |
31 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (1 ∈
(0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1
< 2)) |
32 | 29, 26, 30, 31 | mpbir3an 1244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
(0..^2) |
33 | 28, 32 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (0 ∈
(0..^2) ∧ 1 ∈ (0..^2)) |
34 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
35 | 34 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) = 2
→ (0 ∈ (0..^(#‘𝐹)) ↔ 0 ∈
(0..^2))) |
36 | 34 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) = 2
→ (1 ∈ (0..^(#‘𝐹)) ↔ 1 ∈
(0..^2))) |
37 | 35, 36 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐹) = 2
→ ((0 ∈ (0..^(#‘𝐹)) ∧ 1 ∈ (0..^(#‘𝐹))) ↔ (0 ∈ (0..^2)
∧ 1 ∈ (0..^2)))) |
38 | 33, 37 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝐹) = 2
→ (0 ∈ (0..^(#‘𝐹)) ∧ 1 ∈ (0..^(#‘𝐹)))) |
39 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (0 ∈
(0..^(#‘𝐹)) ∧ 1
∈ (0..^(#‘𝐹)))) |
40 | | f1cofveqaeq 6515 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∧
𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺)) ∧ (0 ∈ (0..^(#‘𝐹)) ∧ 1 ∈
(0..^(#‘𝐹)))) →
(((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → 0 = 1)) |
41 | 18, 25, 39, 40 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → 0 = 1)) |
42 | | 0ne1 11088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≠
1 |
43 | | eqneqall 2805 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 = 1
→ (0 ≠ 1 → (𝑃‘0) ≠ (𝑃‘2))) |
44 | 41, 42, 43 | syl6mpi 67 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → (𝑃‘0) ≠ (𝑃‘2))) |
45 | 44 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑃‘0) = (𝑃‘2) ∧ ((#‘𝐹) = 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph ))) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → (𝑃‘0) ≠ (𝑃‘2))) |
46 | 14, 45 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃‘0) = (𝑃‘2) ∧ ((#‘𝐹) = 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph ))) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}) → (𝑃‘0) ≠ (𝑃‘2))) |
47 | 13, 46 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃‘0) = (𝑃‘2) ∧ ((#‘𝐹) = 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph ))) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2))) |
48 | 47 | expimpd 629 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) = (𝑃‘2) ∧ ((#‘𝐹) = 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph ))) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) |
49 | 48 | ex 450 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃‘0) = (𝑃‘2) → (((#‘𝐹) = 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2)))) |
50 | | 2a1 28 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃‘0) ≠ (𝑃‘2) →
(((#‘𝐹) = 2 ∧
(Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2)))) |
51 | 49, 50 | pm2.61ine 2877 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) |
52 | | fzo0to2pr 12553 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0..^2) =
{0, 1} |
53 | 34, 52 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
54 | 53 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
55 | | 2wlklem 26563 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑘 ∈
{0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
56 | 54, 55 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 2
→ (∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
57 | 56 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) = 2
→ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
58 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 2
→ (𝑃‘(#‘𝐹)) = (𝑃‘2)) |
59 | 58 | neeq2d 2854 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) = 2
→ ((𝑃‘0) ≠
(𝑃‘(#‘𝐹)) ↔ (𝑃‘0) ≠ (𝑃‘2))) |
60 | 57, 59 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) = 2
→ (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) ↔ ((𝐹 ∈ Word dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2)))) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) → (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) ↔ ((𝐹 ∈ Word dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2)))) |
62 | 51, 61 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) = 2
∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph )) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) |
63 | 62 | ex 450 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ ((Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph ) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))))) |
64 | 63 | com13 88 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph ) → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))))) |
65 | 64 | expd 452 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (Fun ◡𝐹 → (𝐺 ∈ USPGraph → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))))) |
66 | 65 | 3adant2 1080 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (Fun ◡𝐹 → (𝐺 ∈ USPGraph → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))))) |
67 | 6, 66 | syl6bi 243 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → (Fun ◡𝐹 → (𝐺 ∈ USPGraph → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))))))) |
68 | 67 | impd 447 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UPGraph → ((𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹) → (𝐺 ∈ USPGraph → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))))) |
69 | 68 | com23 86 |
. . . . . . . . 9
⊢ (𝐺 ∈ UPGraph → (𝐺 ∈ USPGraph → ((𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹) → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))))) |
70 | 3, 69 | mpcom 38 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph → ((𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹) → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))))) |
71 | 70 | com12 32 |
. . . . . . 7
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹) → (𝐺 ∈ USPGraph → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))))) |
72 | 2, 71 | sylbi 207 |
. . . . . 6
⊢ (𝐹(Trails‘𝐺)𝑃 → (𝐺 ∈ USPGraph → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))))) |
73 | 72 | imp 445 |
. . . . 5
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ 𝐺 ∈ USPGraph ) → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) |
74 | 73 | necon2d 2817 |
. . . 4
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ 𝐺 ∈ USPGraph ) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (#‘𝐹) ≠ 2)) |
75 | 74 | impancom 456 |
. . 3
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ USPGraph → (#‘𝐹) ≠ 2)) |
76 | 1, 75 | syl 17 |
. 2
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐺 ∈ USPGraph → (#‘𝐹) ≠ 2)) |
77 | 76 | impcom 446 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹(Circuits‘𝐺)𝑃) → (#‘𝐹) ≠ 2) |