Proof of Theorem usg2wotspth
Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | | el2wlkonotot 26400 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
3 | 2 | 3adantr2 1214 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
4 | 1, 3 | sylan 487 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
5 | 4 | 3adant3 1074 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
6 | | simpr1 1060 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑓(𝑉 Walks 𝐸)𝑝) |
7 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
8 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑝 ∈ V |
9 | 7, 8 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ V ∧ 𝑝 ∈ V) |
10 | | is2wlk 26095 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V)) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})))) |
11 | 1, 9, 10 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})))) |
12 | | usgrafun 25878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
13 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
V |
14 | 13 | prid1 4241 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ∈
{0, 1} |
15 | | fzo0to2pr 12420 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0..^2) =
{0, 1} |
16 | 14, 15 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
(0..^2) |
17 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:(0..^2)⟶dom 𝐸 ∧ 0 ∈ (0..^2)) →
(𝑓‘0) ∈ dom
𝐸) |
18 | 16, 17 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (𝑓‘0) ∈ dom 𝐸) |
19 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Fun
𝐸 ∧ (𝑓‘0) ∈ dom 𝐸) → (𝐸‘(𝑓‘0)) ∈ ran 𝐸) |
20 | 18, 19 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (𝐸‘(𝑓‘0)) ∈ ran 𝐸) |
21 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} → ((𝐸‘(𝑓‘0)) ∈ ran 𝐸 ↔ {(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸)) |
22 | 20, 21 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} → {(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸)) |
23 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 1 ∈
V |
24 | 23 | prid2 4242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
{0, 1} |
25 | 24, 15 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
(0..^2) |
26 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:(0..^2)⟶dom 𝐸 ∧ 1 ∈ (0..^2)) →
(𝑓‘1) ∈ dom
𝐸) |
27 | 25, 26 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (𝑓‘1) ∈ dom 𝐸) |
28 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Fun
𝐸 ∧ (𝑓‘1) ∈ dom 𝐸) → (𝐸‘(𝑓‘1)) ∈ ran 𝐸) |
29 | 27, 28 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (𝐸‘(𝑓‘1)) ∈ ran 𝐸) |
30 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)} → ((𝐸‘(𝑓‘1)) ∈ ran 𝐸 ↔ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) |
31 | 29, 30 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → ((𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)} → {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) |
32 | 22, 31 | anim12d 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)}) → ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸))) |
33 | 12, 32 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)}) → ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸))) |
34 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑝:(0...2)⟶𝑉) |
35 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸) → (𝑝‘0) ≠ (𝑝‘1)) |
36 | 35 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑉 USGrph 𝐸 → ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 → (𝑝‘0) ≠ (𝑝‘1))) |
37 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸) → (𝑝‘1) ≠ (𝑝‘2)) |
38 | 37 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑉 USGrph 𝐸 → ({(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸 → (𝑝‘1) ≠ (𝑝‘2))) |
39 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((𝑝‘0) ≠
(𝑝‘1) ∧ (𝑝‘1) ≠ (𝑝‘2)) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ∧ 𝐴 ≠ 𝐶) → (𝑝‘0) ≠ (𝑝‘1)) |
40 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐶 = (𝑝‘2)) → 𝐴 = (𝑝‘0)) |
41 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐶 = (𝑝‘2)) → 𝐶 = (𝑝‘2)) |
42 | 40, 41 | neeq12d 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 ↔ (𝑝‘0) ≠ (𝑝‘2))) |
43 | 42 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 → (𝑝‘0) ≠ (𝑝‘2))) |
44 | 43 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 → (𝑝‘0) ≠ (𝑝‘2))) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘1) ≠ (𝑝‘2)) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝐴 ≠ 𝐶 → (𝑝‘0) ≠ (𝑝‘2))) |
46 | 45 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((𝑝‘0) ≠
(𝑝‘1) ∧ (𝑝‘1) ≠ (𝑝‘2)) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ∧ 𝐴 ≠ 𝐶) → (𝑝‘0) ≠ (𝑝‘2)) |
47 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((𝑝‘0) ≠
(𝑝‘1) ∧ (𝑝‘1) ≠ (𝑝‘2)) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ∧ 𝐴 ≠ 𝐶) → (𝑝‘1) ≠ (𝑝‘2)) |
48 | 39, 46, 47 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝑝‘0) ≠
(𝑝‘1) ∧ (𝑝‘1) ≠ (𝑝‘2)) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ∧ 𝐴 ≠ 𝐶) → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2))) |
49 | 48 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘1) ≠ (𝑝‘2)) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2))))) |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑉 USGrph 𝐸 → (((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘1) ≠ (𝑝‘2)) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2)))))) |
51 | 36, 38, 50 | syl2and 499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑉 USGrph 𝐸 → (({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2)))))) |
52 | 51 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2))))) |
53 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2))))) |
54 | 53 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2))))) |
55 | 54 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) ∧ 𝐴 ≠ 𝐶) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2)))) |
56 | 55 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2))) |
57 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (0...2) =
(0...2) |
58 | 57 | f13idfv 12662 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝:(0...2)–1-1→𝑉 ↔ (𝑝:(0...2)⟶𝑉 ∧ ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2)))) |
59 | 34, 56, 58 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑝:(0...2)–1-1→𝑉) |
60 | | df-f1 5809 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝:(0...2)–1-1→𝑉 ↔ (𝑝:(0...2)⟶𝑉 ∧ Fun ◡𝑝)) |
61 | 59, 60 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝:(0...2)⟶𝑉 ∧ Fun ◡𝑝)) |
62 | 61 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → Fun ◡𝑝) |
63 | 62 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑉 USGrph 𝐸 ∧ ({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸)) ∧ 𝑝:(0...2)⟶𝑉) → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝))) |
64 | 63 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 USGrph 𝐸 → (({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸) → (𝑝:(0...2)⟶𝑉 → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝))))) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (({(𝑝‘0), (𝑝‘1)} ∈ ran 𝐸 ∧ {(𝑝‘1), (𝑝‘2)} ∈ ran 𝐸) → (𝑝:(0...2)⟶𝑉 → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝))))) |
66 | 33, 65 | syld 46 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)}) → (𝑝:(0...2)⟶𝑉 → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝))))) |
67 | 66 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (𝑉 USGrph 𝐸 → (((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)}) → (𝑝:(0...2)⟶𝑉 → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝)))))) |
68 | 67 | com24 93 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (𝑝:(0...2)⟶𝑉 → (((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)}) → (𝑉 USGrph 𝐸 → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝)))))) |
69 | 68 | 3imp 1249 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})) → (𝑉 USGrph 𝐸 → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝)))) |
70 | 69 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → ((𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})) → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝)))) |
71 | 11, 70 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ (𝑉 USGrph 𝐸 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → (𝐴 ≠ 𝐶 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → Fun ◡𝑝)))) |
72 | 71 | com14 94 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → (𝐴 ≠ 𝐶 → (𝑉 USGrph 𝐸 → Fun ◡𝑝)))) |
73 | 72 | com12 32 |
. . . . . . . . . . . 12
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ≠ 𝐶 → (𝑉 USGrph 𝐸 → Fun ◡𝑝)))) |
74 | 73 | 3impia 1253 |
. . . . . . . . . . 11
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝐴 ≠ 𝐶 → (𝑉 USGrph 𝐸 → Fun ◡𝑝))) |
75 | 74 | com13 86 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝐴 ≠ 𝐶 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → Fun ◡𝑝))) |
76 | 75 | a1d 25 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ≠ 𝐶 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → Fun ◡𝑝)))) |
77 | 76 | 3imp 1249 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → Fun ◡𝑝)) |
78 | 77 | imp 444 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → Fun ◡𝑝) |
79 | | wlkdvspth 26138 |
. . . . . . 7
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ Fun ◡𝑝) → 𝑓(𝑉 SPaths 𝐸)𝑝) |
80 | 6, 78, 79 | syl2anc 691 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑓(𝑉 SPaths 𝐸)𝑝) |
81 | | simpr2 1061 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (#‘𝑓) = 2) |
82 | | simpr3 1062 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) |
83 | 80, 81, 82 | 3jca 1235 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) ∧ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
84 | 83 | ex 449 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
85 | | spthispth 26103 |
. . . . . 6
⊢ (𝑓(𝑉 SPaths 𝐸)𝑝 → 𝑓(𝑉 Paths 𝐸)𝑝) |
86 | | pthistrl 26102 |
. . . . . 6
⊢ (𝑓(𝑉 Paths 𝐸)𝑝 → 𝑓(𝑉 Trails 𝐸)𝑝) |
87 | | trliswlk 26069 |
. . . . . 6
⊢ (𝑓(𝑉 Trails 𝐸)𝑝 → 𝑓(𝑉 Walks 𝐸)𝑝) |
88 | 85, 86, 87 | 3syl 18 |
. . . . 5
⊢ (𝑓(𝑉 SPaths 𝐸)𝑝 → 𝑓(𝑉 Walks 𝐸)𝑝) |
89 | 88 | 3anim1i 1241 |
. . . 4
⊢ ((𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
90 | 84, 89 | impbid1 214 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ↔ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
91 | 90 | 2exbidv 1839 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ↔ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
92 | 5, 91 | bitrd 267 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |