Step |
Hyp |
Ref |
Expression |
1 |
|
crctprop |
⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
2 |
|
istrl |
⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) ) |
3 |
|
uspgrupgr |
⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph ) |
4 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
5 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
6 |
4 5
|
upgriswlk |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) ) |
7 |
|
preq2 |
⊢ ( ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } ) |
8 |
|
prcom |
⊢ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } |
9 |
7 8
|
eqtrdi |
⊢ ( ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ 0 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) |
10 |
9
|
eqcoms |
⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) |
11 |
10
|
eqeq2d |
⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) |
12 |
11
|
anbi2d |
⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) ) |
13 |
12
|
ad2antrr |
⊢ ( ( ( ( 𝑃 ‘ 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 |
⊢ ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) ) |
15 |
4 5
|
uspgrf |
⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
16 |
15
|
adantl |
⊢ ( ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
17 |
16
|
adantl |
⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
18 |
17
|
adantr |
⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
19 |
|
df-f1 |
⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ Fun ◡ 𝐹 ) ) |
20 |
19
|
simplbi2 |
⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) → ( Fun ◡ 𝐹 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) ) |
21 |
|
wrdf |
⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom ( iEdg ‘ 𝐺 ) ) |
22 |
20 21
|
syl11 |
⊢ ( Fun ◡ 𝐹 → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) ) |
23 |
22
|
adantr |
⊢ ( ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) ) |
24 |
23
|
adantl |
⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) ) |
25 |
24
|
imp |
⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom ( iEdg ‘ 𝐺 ) ) |
26 |
|
2nn |
⊢ 2 ∈ ℕ |
27 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ 2 ∈ ℕ ) |
28 |
26 27
|
mpbir |
⊢ 0 ∈ ( 0 ..^ 2 ) |
29 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
30 |
|
1lt2 |
⊢ 1 < 2 |
31 |
|
elfzo0 |
⊢ ( 1 ∈ ( 0 ..^ 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2 ) ) |
32 |
29 26 30 31
|
mpbir3an |
⊢ 1 ∈ ( 0 ..^ 2 ) |
33 |
28 32
|
pm3.2i |
⊢ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) |
34 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) ) |
35 |
34
|
eleq2d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 0 ∈ ( 0 ..^ 2 ) ) ) |
36 |
34
|
eleq2d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 1 ∈ ( 0 ..^ 2 ) ) ) |
37 |
35 36
|
anbi12d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) ) ) |
38 |
33 37
|
mpbiri |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) |
39 |
38
|
ad2antrr |
⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) |
40 |
|
f1cofveqaeq |
⊢ ( ( ( ( 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 |
⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → 0 = 1 ) ) |
42 |
|
0ne1 |
⊢ 0 ≠ 1 |
43 |
|
eqneqall |
⊢ ( 0 = 1 → ( 0 ≠ 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
44 |
41 42 43
|
syl6mpi |
⊢ ( ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
45 |
44
|
adantll |
⊢ ( ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
46 |
14 45
|
syl5 |
⊢ ( ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
47 |
13 46
|
sylbid |
⊢ ( ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
48 |
47
|
expimpd |
⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ∧ ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
49 |
48
|
ex |
⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) → ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
50 |
|
2a1 |
⊢ ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) → ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
51 |
49 50
|
pm2.61ine |
⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
52 |
|
fzo0to2pr |
⊢ ( 0 ..^ 2 ) = { 0 , 1 } |
53 |
34 52
|
eqtrdi |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } ) |
54 |
53
|
raleqdv |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ∀ 𝑘 ∈ { 0 , 1 } ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) |
55 |
|
2wlklem |
⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
56 |
54 55
|
bitrdi |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) |
57 |
56
|
anbi2d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) ) |
58 |
|
fveq2 |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 2 ) ) |
59 |
58
|
neeq2d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) |
60 |
57 59
|
imbi12d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) ) ) |
61 |
60
|
adantr |
⊢ ( ( ( ♯ ‘ 𝐹 ) = 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 |
⊢ ( ( ( ♯ ‘ 𝐹 ) = 2 ∧ ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
63 |
62
|
ex |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) |
64 |
63
|
com13 |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( ( Fun ◡ 𝐹 ∧ 𝐺 ∈ USPGraph ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) |
65 |
64
|
expd |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( Fun ◡ 𝐹 → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) ) |
66 |
65
|
3adant2 |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( Fun ◡ 𝐹 → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) ) |
67 |
6 66
|
syl6bi |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( Fun ◡ 𝐹 → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) ) ) |
68 |
67
|
impd |
⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) ) |
69 |
68
|
com23 |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐺 ∈ USPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) ) |
70 |
3 69
|
mpcom |
⊢ ( 𝐺 ∈ USPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) |
71 |
70
|
com12 |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) |
72 |
2 71
|
sylbi |
⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ USPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) |
73 |
72
|
imp |
⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐺 ∈ USPGraph ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
74 |
73
|
necon2d |
⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐺 ∈ USPGraph ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ≠ 2 ) ) |
75 |
74
|
impancom |
⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐺 ∈ USPGraph → ( ♯ ‘ 𝐹 ) ≠ 2 ) ) |
76 |
1 75
|
syl |
⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ USPGraph → ( ♯ ‘ 𝐹 ) ≠ 2 ) ) |
77 |
76
|
impcom |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 2 ) |