Step | Hyp | Ref
| Expression |
1 | | usgrupgr 27273 |
. . . . 5
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UPGraph) |
2 | | eqid 2737 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2737 |
. . . . . 6
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
4 | 2, 3 | upgrf1istrl 27791 |
. . . . 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 2738 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → 𝐹 = 𝐹) |
7 | | oveq2 7221 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹) =
2 → (0..^(♯‘𝐹)) = (0..^2)) |
8 | | fzo0to2pr 13327 |
. . . . . . . . . . . . 13
⊢ (0..^2) =
{0, 1} |
9 | 7, 8 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → (0..^(♯‘𝐹)) = {0, 1}) |
10 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → dom (iEdg‘𝐺)
= dom (iEdg‘𝐺)) |
11 | 6, 9, 10 | f1eq123d 6653 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
2 → (𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ↔ 𝐹:{0, 1}–1-1→dom (iEdg‘𝐺))) |
12 | 9 | raleqdv 3325 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → (∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
13 | | 2wlklem 27755 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
{0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
14 | 12, 13 | bitrdi 290 |
. . . . . . . . . . 11
⊢
((♯‘𝐹) =
2 → (∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
15 | 11, 14 | anbi12d 634 |
. . . . . . . . . 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 485 |
. . . . . . . . 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 10827 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
18 | | 1ex 10829 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
V |
19 | 17, 18 | pm3.2i 474 |
. . . . . . . . . . . . 13
⊢ (0 ∈
V ∧ 1 ∈ V) |
20 | | 0ne1 11901 |
. . . . . . . . . . . . 13
⊢ 0 ≠
1 |
21 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ {0, 1} =
{0, 1} |
22 | 21 | f12dfv 7084 |
. . . . . . . . . . . . 13
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ 0 ≠ 1) → (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ↔ (𝐹:{0, 1}⟶dom (iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1)))) |
23 | 19, 20, 22 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ↔ (𝐹:{0, 1}⟶dom (iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1))) |
24 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
25 | 3, 24 | usgrf1oedg 27295 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→(Edg‘𝐺)) |
26 | | f1of1 6660 |
. . . . . . . . . . . . . 14
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→(Edg‘𝐺) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺)) |
27 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) → 𝐹:{0, 1}⟶dom
(iEdg‘𝐺)) |
28 | 17 | prid1 4678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
{0, 1} |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) → 0
∈ {0, 1}) |
30 | 27, 29 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
(𝐹‘0) ∈ dom
(iEdg‘𝐺)) |
31 | 18 | prid2 4679 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
{0, 1} |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) → 1
∈ {0, 1}) |
33 | 27, 32 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
(𝐹‘1) ∈ dom
(iEdg‘𝐺)) |
34 | 30, 33 | jca 515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
((𝐹‘0) ∈ dom
(iEdg‘𝐺) ∧ (𝐹‘1) ∈ dom
(iEdg‘𝐺))) |
35 | 34 | anim1ci 619 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺)) → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→(Edg‘𝐺) ∧ ((𝐹‘0) ∈ dom (iEdg‘𝐺) ∧ (𝐹‘1) ∈ dom (iEdg‘𝐺)))) |
36 | | f1veqaeq 7069 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺) ∧ ((𝐹‘0) ∈ dom (iEdg‘𝐺) ∧ (𝐹‘1) ∈ dom (iEdg‘𝐺))) → (((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → (𝐹‘0) = (𝐹‘1))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺)) → (((iEdg‘𝐺)‘(𝐹‘0)) = ((iEdg‘𝐺)‘(𝐹‘1)) → (𝐹‘0) = (𝐹‘1))) |
38 | 37 | necon3d 2961 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺)) → ((𝐹‘0) ≠ (𝐹‘1) → ((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)))) |
39 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) |
40 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) |
41 | 39, 40 | neeq12d 3002 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)) ↔ {(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)})) |
42 | | preq1 4649 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)}) |
43 | | prcom 4648 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {(𝑃‘2), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} |
44 | 42, 43 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)}) |
45 | 44 | necon3i 2973 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) ≠ (𝑃‘2)) |
46 | 41, 45 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)) → (𝑃‘0) ≠ (𝑃‘2))) |
47 | 46 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2))) |
48 | 47 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢
(((iEdg‘𝐺)‘(𝐹‘0)) ≠ ((iEdg‘𝐺)‘(𝐹‘1)) → (𝐺 ∈ USGraph → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))) |
49 | 38, 48 | 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))))) |
50 | 49 | expcom 417 |
. . . . . . . . . . . . . . . 16
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→(Edg‘𝐺) → (𝐹:{0, 1}⟶dom (iEdg‘𝐺) → ((𝐹‘0) ≠ (𝐹‘1) → (𝐺 ∈ USGraph → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))))) |
51 | 50 | impd 414 |
. . . . . . . . . . . . . . 15
⊢
((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 | 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))))) |
53 | 26, 52 | 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))))) |
54 | 25, 53 | mpcom 38 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → ((𝐹:{0, 1}⟶dom
(iEdg‘𝐺) ∧ (𝐹‘0) ≠ (𝐹‘1)) →
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))) |
55 | 23, 54 | syl5bi 245 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))) |
56 | 55 | impd 414 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → ((𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) |
57 | 56 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧
(♯‘𝐹) = 2)
→ ((𝐹:{0,
1}–1-1→dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) |
58 | 16, 57 | sylbid 243 |
. . . . . . . 8
⊢ ((𝐺 ∈ USGraph ∧
(♯‘𝐹) = 2)
→ ((𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃‘0) ≠ (𝑃‘2))) |
59 | 58 | com12 32 |
. . . . . . 7
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝑃‘0) ≠ (𝑃‘2))) |
60 | 59 | 3adant2 1133 |
. . . . . 6
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝑃‘0) ≠ (𝑃‘2))) |
61 | 60 | expdcom 418 |
. . . . 5
⊢ (𝐺 ∈ USGraph →
((♯‘𝐹) = 2
→ ((𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃‘0) ≠ (𝑃‘2)))) |
62 | 61 | com23 86 |
. . . 4
⊢ (𝐺 ∈ USGraph → ((𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((♯‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘2)))) |
63 | 5, 62 | sylbid 243 |
. . 3
⊢ (𝐺 ∈ USGraph → (𝐹(Trails‘𝐺)𝑃 → ((♯‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘2)))) |
64 | 63 | com23 86 |
. 2
⊢ (𝐺 ∈ USGraph →
((♯‘𝐹) = 2
→ (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2)))) |
65 | 64 | imp 410 |
1
⊢ ((𝐺 ∈ USGraph ∧
(♯‘𝐹) = 2)
→ (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2))) |