Step | Hyp | Ref
| Expression |
1 | | usgrupgr 26077 |
. . . . 5
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph
) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2622 |
. . . . . 6
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
4 | 2, 3 | upgrf1istrl 26600 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝐺 ∈ USGraph → (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
6 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ 𝐹 = 𝐹) |
7 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
8 | | fzo0to2pr 12553 |
. . . . . . . . . . . . 13
⊢ (0..^2) =
{0, 1} |
9 | 7, 8 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
10 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ dom (iEdg‘𝐺) =
dom (iEdg‘𝐺)) |
11 | 6, 9, 10 | f1eq123d 6131 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ↔ 𝐹:{0, 1}–1-1→dom (iEdg‘𝐺))) |
12 | 9 | raleqdv 3144 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 2
→ (∀𝑖 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
13 | | 2wlklem 26563 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
{0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
14 | 12, 13 | syl6bb 276 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 2
→ (∀𝑖 ∈
(0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
15 | 11, 14 | anbi12d 747 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ ((𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
16 | 15 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
((𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
17 | | c0ex 10034 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
18 | | 1ex 10035 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
V |
19 | 17, 18 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ (0 ∈
V ∧ 1 ∈ V) |
20 | | 0ne1 11088 |
. . . . . . . . . . . . 13
⊢ 0 ≠
1 |
21 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ {0, 1} =
{0, 1} |
22 | 21 | f12dfv 6529 |
. . . . . . . . . . . . 13
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ 0 ≠ 1) → (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ↔ (𝐹:{0, 1}⟶dom (iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
23 | 19, 20, 22 | mp2an 708 |
. . . . . . . . . . . 12
⊢ (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ↔ (𝐹:{0, 1}⟶dom (iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1))) |
24 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
25 | 3, 24 | usgrf1oedg 26099 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→(Edg‘𝐺)) |
26 | | f1of1 6136 |
. . . . . . . . . . . . . 14
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺)) |
27 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) → 𝐹:{0, 1}⟶dom
(iEdg‘𝐺)) |
28 | 17 | prid1 4297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
{0, 1} |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) → 0
∈ {0, 1}) |
30 | 27, 29 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
(𝐹‘0) ∈ dom
(iEdg‘𝐺)) |
31 | 18 | prid2 4298 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
{0, 1} |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) → 1
∈ {0, 1}) |
33 | 27, 32 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
(𝐹‘1) ∈ dom
(iEdg‘𝐺)) |
34 | 30, 33 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
((𝐹‘0) ∈ dom
(iEdg‘𝐺) ∧ (𝐹‘1) ∈ dom
(iEdg‘𝐺))) |
35 | 34 | anim2i 593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺) ∧ 𝐹:{0, 1}⟶dom (iEdg‘𝐺)) → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺) ∧ ((𝐹‘0) ∈ dom (iEdg‘𝐺) ∧ (𝐹‘1) ∈ dom (iEdg‘𝐺)))) |
36 | 35 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺)) → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺) ∧ ((𝐹‘0) ∈ dom (iEdg‘𝐺) ∧ (𝐹‘1) ∈ dom (iEdg‘𝐺)))) |
37 | | f1veqaeq 6514 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺) ∧ ((𝐹‘0) ∈ dom (iEdg‘𝐺) ∧ (𝐹‘1) ∈ dom (iEdg‘𝐺))) → (((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → (𝐹‘0) = (𝐹‘1))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → (𝐹‘0) = (𝐹‘1))) |
39 | 38 | necon3d 2815 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺)) → ((𝐹‘0) ≠ (𝐹‘1) → ((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)))) |
40 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) |
41 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) |
42 | 40, 41 | neeq12d 2855 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)) ↔ {(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)})) |
43 | | preq1 4268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)}) |
44 | | prcom 4267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {(𝑃‘2), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} |
45 | 43, 44 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)}) |
46 | 45 | necon3i 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) ≠ (𝑃‘2)) |
47 | 42, 46 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)) → (𝑃‘0) ≠ (𝑃‘2))) |
48 | 47 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2))) |
49 | 48 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢
(((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)) → (𝐺 ∈ USGraph → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))) |
50 | 39, 49 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺)) → ((𝐹‘0) ≠ (𝐹‘1) → (𝐺 ∈ USGraph → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2))))) |
51 | 50 | expcom 451 |
. . . . . . . . . . . . . . . 16
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺) → (𝐹:{0, 1}⟶dom (iEdg‘𝐺) → ((𝐹‘0) ≠ (𝐹‘1) → (𝐺 ∈ USGraph → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))))) |
52 | 51 | impd 447 |
. . . . . . . . . . . . . . 15
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺) → ((𝐹:{0, 1}⟶dom (iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1)) → (𝐺 ∈ USGraph → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2))))) |
53 | 52 | com23 86 |
. . . . . . . . . . . . . 14
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺) → (𝐺 ∈ USGraph → ((𝐹:{0, 1}⟶dom (iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2))))) |
54 | 26, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) → (𝐺 ∈ USGraph → ((𝐹:{0, 1}⟶dom (iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2))))) |
55 | 25, 54 | mpcom 38 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1)) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))) |
56 | 23, 55 | syl5bi 232 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))) |
57 | 56 | impd 447 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → ((𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) |
58 | 57 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
((𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) |
59 | 16, 58 | sylbid 230 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
((𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃‘0) ≠ (𝑃‘2))) |
60 | 59 | com12 32 |
. . . . . . 7
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝑃‘0) ≠ (𝑃‘2))) |
61 | 60 | 3adant2 1080 |
. . . . . 6
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝑃‘0) ≠ (𝑃‘2))) |
62 | 61 | expdcom 455 |
. . . . 5
⊢ (𝐺 ∈ USGraph →
((#‘𝐹) = 2 →
((𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃‘0) ≠ (𝑃‘2)))) |
63 | 62 | com23 86 |
. . . 4
⊢ (𝐺 ∈ USGraph → ((𝐹:(0..^(#‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘2)))) |
64 | 5, 63 | sylbid 230 |
. . 3
⊢ (𝐺 ∈ USGraph → (𝐹(Trails‘𝐺)𝑃 → ((#‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘2)))) |
65 | 64 | com23 86 |
. 2
⊢ (𝐺 ∈ USGraph →
((#‘𝐹) = 2 →
(𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2)))) |
66 | 65 | imp 445 |
1
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
(𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2))) |