| Step |
Hyp |
Ref |
Expression |
| 1 |
|
usgrupgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph ) |
| 2 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 3 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
| 4 |
2 3
|
upgrf1istrl |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ) |
| 5 |
1 4
|
syl |
⊢ ( 𝐺 ∈ USGraph → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ) |
| 6 |
|
eqidd |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → 𝐹 = 𝐹 ) |
| 7 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) ) |
| 8 |
|
fzo0to2pr |
⊢ ( 0 ..^ 2 ) = { 0 , 1 } |
| 9 |
7 8
|
eqtrdi |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } ) |
| 10 |
|
eqidd |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 ) ) |
| 11 |
6 9 10
|
f1eq123d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ↔ 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ) ) |
| 12 |
9
|
raleqdv |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ { 0 , 1 } ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) |
| 13 |
|
2wlklem |
⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 14 |
12 13
|
bitrdi |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) |
| 15 |
11 14
|
anbi12d |
⊢ ( ( ♯ ‘ 𝐹 ) = 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 |
⊢ ( ( 𝐺 ∈ 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 |
⊢ 0 ∈ V |
| 18 |
|
1ex |
⊢ 1 ∈ V |
| 19 |
17 18
|
pm3.2i |
⊢ ( 0 ∈ V ∧ 1 ∈ V ) |
| 20 |
|
0ne1 |
⊢ 0 ≠ 1 |
| 21 |
|
eqid |
⊢ { 0 , 1 } = { 0 , 1 } |
| 22 |
21
|
f12dfv |
⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ 0 ≠ 1 ) → ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ↔ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) ) ) |
| 23 |
19 20 22
|
mp2an |
⊢ ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ↔ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) ) |
| 24 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
| 25 |
3 24
|
usgrf1oedg |
⊢ ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) ) |
| 26 |
|
f1of1 |
⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) |
| 27 |
|
id |
⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ) |
| 28 |
17
|
prid1 |
⊢ 0 ∈ { 0 , 1 } |
| 29 |
28
|
a1i |
⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → 0 ∈ { 0 , 1 } ) |
| 30 |
27 29
|
ffvelrnd |
⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → ( 𝐹 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) ) |
| 31 |
18
|
prid2 |
⊢ 1 ∈ { 0 , 1 } |
| 32 |
31
|
a1i |
⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → 1 ∈ { 0 , 1 } ) |
| 33 |
27 32
|
ffvelrnd |
⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → ( 𝐹 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) ) |
| 34 |
30 33
|
jca |
⊢ ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) → ( ( 𝐹 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) |
| 35 |
34
|
anim1ci |
⊢ ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ∧ ( ( 𝐹 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) ) |
| 36 |
|
f1veqaeq |
⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ∧ ( ( 𝐹 ‘ 0 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 1 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) ) ) |
| 37 |
35 36
|
syl |
⊢ ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) ) ) |
| 38 |
37
|
necon3d |
⊢ ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( Edg ‘ 𝐺 ) ) → ( ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) ) ) |
| 39 |
|
simpl |
⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) |
| 40 |
|
simpr |
⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) |
| 41 |
39 40
|
neeq12d |
⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 42 |
|
preq1 |
⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) |
| 43 |
|
prcom |
⊢ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } |
| 44 |
42 43
|
eqtrdi |
⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) |
| 45 |
44
|
necon3i |
⊢ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) |
| 46 |
41 45
|
syl6bi |
⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
| 47 |
46
|
com12 |
⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
| 48 |
47
|
a1d |
⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) ≠ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝐺 ∈ USGraph → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
| 49 |
38 48
|
syl6 |
⊢ ( ( 𝐹 : { 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 |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( ( 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 |
⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 : { 0 , 1 } ⟶ dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 0 ) ≠ ( 𝐹 ‘ 1 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
| 55 |
23 54
|
syl5bi |
⊢ ( 𝐺 ∈ USGraph → ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
| 56 |
55
|
impd |
⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
| 57 |
56
|
adantr |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 : { 0 , 1 } –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
| 58 |
16 57
|
sylbid |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
| 59 |
58
|
com12 |
⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
| 60 |
59
|
3adant2 |
⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
| 61 |
60
|
expdcom |
⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
| 62 |
61
|
com23 |
⊢ ( 𝐺 ∈ USGraph → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
| 63 |
5 62
|
sylbid |
⊢ ( 𝐺 ∈ USGraph → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
| 64 |
63
|
com23 |
⊢ ( 𝐺 ∈ USGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
| 65 |
64
|
imp |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |