| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | usgrupgr 29202 | . . . . 5
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UPGraph) | 
| 2 |  | eqid 2737 | . . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 3 |  | eqid 2737 | . . . . . 6
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) | 
| 4 | 2, 3 | upgrf1istrl 29721 | . . . . 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 7439 | . . . . . . . . . . . . 13
⊢
((♯‘𝐹) =
2 → (0..^(♯‘𝐹)) = (0..^2)) | 
| 8 |  | fzo0to2pr 13789 | . . . . . . . . . . . . 13
⊢ (0..^2) =
{0, 1} | 
| 9 | 7, 8 | eqtrdi 2793 | . . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → (0..^(♯‘𝐹)) = {0, 1}) | 
| 10 |  | eqidd 2738 | . . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → dom (iEdg‘𝐺)
= dom (iEdg‘𝐺)) | 
| 11 | 6, 9, 10 | f1eq123d 6840 | . . . . . . . . . . 11
⊢
((♯‘𝐹) =
2 → (𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ↔ 𝐹:{0, 1}–1-1→dom (iEdg‘𝐺))) | 
| 12 | 9 | raleqdv 3326 | . . . . . . . . . . . 12
⊢
((♯‘𝐹) =
2 → (∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ {0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | 
| 13 |  | 2wlklem 29685 | . . . . . . . . . . . 12
⊢
(∀𝑖 ∈
{0, 1} ((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) | 
| 14 | 12, 13 | bitrdi 287 | . . . . . . . . . . 11
⊢
((♯‘𝐹) =
2 → (∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) | 
| 15 | 11, 14 | anbi12d 632 | . . . . . . . . . 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 481 | . . . . . . . . 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 11255 | . . . . . . . . . . . . . 14
⊢ 0 ∈
V | 
| 18 |  | 1ex 11257 | . . . . . . . . . . . . . 14
⊢ 1 ∈
V | 
| 19 | 17, 18 | pm3.2i 470 | . . . . . . . . . . . . 13
⊢ (0 ∈
V ∧ 1 ∈ V) | 
| 20 |  | 0ne1 12337 | . . . . . . . . . . . . 13
⊢ 0 ≠
1 | 
| 21 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ {0, 1} =
{0, 1} | 
| 22 | 21 | f12dfv 7293 | . . . . . . . . . . . . 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 29224 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1-onto→(Edg‘𝐺)) | 
| 26 |  | f1of1 6847 | . . . . . . . . . . . . . 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 4762 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
{0, 1} | 
| 29 | 28 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) → 0
∈ {0, 1}) | 
| 30 | 27, 29 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
(𝐹‘0) ∈ dom
(iEdg‘𝐺)) | 
| 31 | 18 | prid2 4763 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
{0, 1} | 
| 32 | 31 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) → 1
∈ {0, 1}) | 
| 33 | 27, 32 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
(𝐹‘1) ∈ dom
(iEdg‘𝐺)) | 
| 34 | 30, 33 | jca 511 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:{0, 1}⟶dom
(iEdg‘𝐺) →
((𝐹‘0) ∈ dom
(iEdg‘𝐺) ∧ (𝐹‘1) ∈ dom
(iEdg‘𝐺))) | 
| 35 | 34 | anim1ci 616 | . . . . . . . . . . . . . . . . . . . 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 7277 | . . . . . . . . . . . . . . . . . . . 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 482 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → ((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) | 
| 40 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 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 4733 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘2), (𝑃‘1)}) | 
| 43 |  | prcom 4732 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ {(𝑃‘2), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)} | 
| 44 | 42, 43 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘2) → {(𝑃‘0), (𝑃‘1)} = {(𝑃‘1), (𝑃‘2)}) | 
| 45 | 44 | necon3i 2973 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ({(𝑃‘0), (𝑃‘1)} ≠ {(𝑃‘1), (𝑃‘2)} → (𝑃‘0) ≠ (𝑃‘2)) | 
| 46 | 41, 45 | biimtrdi 253 | . . . . . . . . . . . . . . . . . . . 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 413 | . . . . . . . . . . . . . . . 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 410 | . . . . . . . . . . . . . . 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 | biimtrid 242 | . . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → (𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) → ((((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝑃‘0) ≠ (𝑃‘2)))) | 
| 56 | 55 | impd 410 | . . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → ((𝐹:{0, 1}–1-1→dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) | 
| 57 | 56 | adantr 480 | . . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧
(♯‘𝐹) = 2)
→ ((𝐹:{0,
1}–1-1→dom (iEdg‘𝐺) ∧ (((iEdg‘𝐺)‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ ((iEdg‘𝐺)‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) → (𝑃‘0) ≠ (𝑃‘2))) | 
| 58 | 16, 57 | sylbid 240 | . . . . . . . 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 1132 | . . . . . 6
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝑃‘0) ≠ (𝑃‘2))) | 
| 61 | 60 | expdcom 414 | . . . . 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 240 | . . 3
⊢ (𝐺 ∈ USGraph → (𝐹(Trails‘𝐺)𝑃 → ((♯‘𝐹) = 2 → (𝑃‘0) ≠ (𝑃‘2)))) | 
| 64 | 63 | com23 86 | . 2
⊢ (𝐺 ∈ USGraph →
((♯‘𝐹) = 2
→ (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2)))) | 
| 65 | 64 | imp 406 | 1
⊢ ((𝐺 ∈ USGraph ∧
(♯‘𝐹) = 2)
→ (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2))) |