| Step | Hyp | Ref
| Expression |
| 1 | | crctprop 29812 |
. . 3
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) |
| 2 | | istrl 29714 |
. . . . . . 7
⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹)) |
| 3 | | uspgrupgr 29195 |
. . . . . . . . 9
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈
UPGraph) |
| 4 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 5 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 6 | 4, 5 | upgriswlk 29659 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 7 | | preq2 4734 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃‘2) = (𝑃‘0) → {(𝑃‘1), (𝑃‘2)} = {(𝑃‘1), (𝑃‘0)}) |
| 8 | | prcom 4732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {(𝑃‘1), (𝑃‘0)} = {(𝑃‘0), (𝑃‘1)} |
| 9 | 7, 8 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃‘2) = (𝑃‘0) → {(𝑃‘1), (𝑃‘2)} = {(𝑃‘0), (𝑃‘1)}) |
| 10 | 9 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘1), (𝑃‘2)} = {(𝑃‘0), (𝑃‘1)}) |
| 11 | 10 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃‘0) = (𝑃‘2) → (((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)})) |
| 12 | 11 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘2) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}))) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 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 2763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}) → ((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1))) |
| 15 | 4, 5 | uspgrf 29171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 16 | 15 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
◡𝐹 ∧ 𝐺 ∈ USPGraph) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝐹)
= 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph)) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((♯‘𝐹)
= 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph)) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 19 | | df-f1 6566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ↔ (𝐹:(0..^(♯‘𝐹))⟶dom (iEdg‘𝐺) ∧ Fun ◡𝐹)) |
| 20 | 19 | simplbi2 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹:(0..^(♯‘𝐹))⟶dom (iEdg‘𝐺) → (Fun ◡𝐹 → 𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺))) |
| 21 | | wrdf 14557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
◡𝐹 ∧ 𝐺 ∈ USPGraph) → (𝐹 ∈ Word dom (iEdg‘𝐺) → 𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺))) |
| 24 | 23 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝐹)
= 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph)) → (𝐹 ∈ Word dom (iEdg‘𝐺) → 𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺))) |
| 25 | 24 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((♯‘𝐹)
= 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph)) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → 𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺)) |
| 26 | | 2nn 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 2 ∈
ℕ |
| 27 | | lbfzo0 13739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (0 ∈
(0..^2) ↔ 2 ∈ ℕ) |
| 28 | 26, 27 | mpbir 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
(0..^2) |
| 29 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℕ0 |
| 30 | | 1lt2 12437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 <
2 |
| 31 | | elfzo0 13740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (1 ∈
(0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1
< 2)) |
| 32 | 29, 26, 30, 31 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
(0..^2) |
| 33 | 28, 32 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (0 ∈
(0..^2) ∧ 1 ∈ (0..^2)) |
| 34 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝐹) =
2 → (0..^(♯‘𝐹)) = (0..^2)) |
| 35 | 34 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝐹) =
2 → (0 ∈ (0..^(♯‘𝐹)) ↔ 0 ∈
(0..^2))) |
| 36 | 34 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝐹) =
2 → (1 ∈ (0..^(♯‘𝐹)) ↔ 1 ∈
(0..^2))) |
| 37 | 35, 36 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((♯‘𝐹) =
2 → ((0 ∈ (0..^(♯‘𝐹)) ∧ 1 ∈ (0..^(♯‘𝐹))) ↔ (0 ∈ (0..^2)
∧ 1 ∈ (0..^2)))) |
| 38 | 33, 37 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝐹) =
2 → (0 ∈ (0..^(♯‘𝐹)) ∧ 1 ∈ (0..^(♯‘𝐹)))) |
| 39 | 38 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((♯‘𝐹)
= 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph)) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (0 ∈
(0..^(♯‘𝐹))
∧ 1 ∈ (0..^(♯‘𝐹)))) |
| 40 | | f1cofveqaeq 7278 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((♯‘𝐹)
= 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph)) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → 0 = 1)) |
| 42 | | 0ne1 12337 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≠
1 |
| 43 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . . . . . . . . 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 714 |
. . . . . . . . . . . . . . . . . . . . . 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 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃‘0) = (𝑃‘2) ∧ ((♯‘𝐹) = 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph))) ∧ 𝐹 ∈ Word dom (iEdg‘𝐺)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2))) |
| 48 | 47 | expimpd 453 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃‘0) = (𝑃‘2) ∧ ((♯‘𝐹) = 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph))) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) |
| 49 | 48 | ex 412 |
. . . . . . . . . . . . . . . . . 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 3025 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝐹)
= 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph)) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
(((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) |
| 52 | | fzo0to2pr 13789 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0..^2) =
{0, 1} |
| 53 | 34, 52 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝐹) =
2 → (0..^(♯‘𝐹)) = {0, 1}) |
| 54 | 53 | raleqdv 3326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐹) =
2 → (∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 55 | | 2wlklem 29685 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑘 ∈
{0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
| 56 | 54, 55 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
2 → (∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
| 57 | 56 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝐹) =
2 → ((𝐹 ∈ Word
dom (iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
| 58 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝐹) =
2 → (𝑃‘(♯‘𝐹)) = (𝑃‘2)) |
| 59 | 58 | neeq2d 3001 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝐹) =
2 → ((𝑃‘0) ≠
(𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) ≠ (𝑃‘2))) |
| 60 | 57, 59 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . . . . . . 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 257 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐹)
= 2 ∧ (Fun ◡𝐹 ∧ 𝐺 ∈ USPGraph)) → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) |
| 63 | 62 | ex 412 |
. . . . . . . . . . . . . . 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 415 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧
∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (Fun ◡𝐹 → (𝐺 ∈ USPGraph →
((♯‘𝐹) = 2
→ (𝑃‘0) ≠
(𝑃‘(♯‘𝐹)))))) |
| 66 | 65 | 3adant2 1132 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (Fun ◡𝐹 → (𝐺 ∈ USPGraph →
((♯‘𝐹) = 2
→ (𝑃‘0) ≠
(𝑃‘(♯‘𝐹)))))) |
| 67 | 6, 66 | biimtrdi 253 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → (Fun ◡𝐹 → (𝐺 ∈ USPGraph →
((♯‘𝐹) = 2
→ (𝑃‘0) ≠
(𝑃‘(♯‘𝐹))))))) |
| 68 | 67 | impd 410 |
. . . . . . . . . 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 217 |
. . . . . 6
⊢ (𝐹(Trails‘𝐺)𝑃 → (𝐺 ∈ USPGraph →
((♯‘𝐹) = 2
→ (𝑃‘0) ≠
(𝑃‘(♯‘𝐹))))) |
| 73 | 72 | imp 406 |
. . . . 5
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ 𝐺 ∈ USPGraph) →
((♯‘𝐹) = 2
→ (𝑃‘0) ≠
(𝑃‘(♯‘𝐹)))) |
| 74 | 73 | necon2d 2963 |
. . . 4
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ 𝐺 ∈ USPGraph) → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (♯‘𝐹) ≠ 2)) |
| 75 | 74 | impancom 451 |
. . 3
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ USPGraph → (♯‘𝐹) ≠ 2)) |
| 76 | 1, 75 | syl 17 |
. 2
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐺 ∈ USPGraph → (♯‘𝐹) ≠ 2)) |
| 77 | 76 | impcom 407 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹(Circuits‘𝐺)𝑃) → (♯‘𝐹) ≠ 2) |