Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | | el2wlkonotot 26400 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
3 | 2 | 3adantr2 1214 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
4 | 1, 3 | sylan 487 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
5 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
6 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑝 ∈ V |
7 | 5, 6 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ V ∧ 𝑝 ∈ V) |
8 | | is2wlk 26095 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V)) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})))) |
9 | 1, 7, 8 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})))) |
10 | | preq12 4214 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1)) → {𝐴, 𝐵} = {(𝑝‘0), (𝑝‘1)}) |
11 | 10 | 3adant3 1074 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → {𝐴, 𝐵} = {(𝑝‘0), (𝑝‘1)}) |
12 | 11 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ↔ (𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)})) |
13 | | preq12 4214 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → {𝐵, 𝐶} = {(𝑝‘1), (𝑝‘2)}) |
14 | 13 | 3adant1 1072 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → {𝐵, 𝐶} = {(𝑝‘1), (𝑝‘2)}) |
15 | 14 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝐸‘(𝑓‘1)) = {𝐵, 𝐶} ↔ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})) |
16 | 12, 15 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶}) ↔ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)}))) |
17 | 16 | bicomd 212 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)}) ↔ ((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶}))) |
18 | 17 | 3anbi3d 1397 |
. . . . . . . . . . . 12
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})) ↔ (𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶})))) |
19 | | usgrafun 25878 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
20 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
V |
21 | 20 | prid1 4241 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
{0, 1} |
22 | | fzo0to2pr 12420 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0..^2) =
{0, 1} |
23 | 21, 22 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
(0..^2) |
24 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓:(0..^2)⟶dom 𝐸 ∧ 0 ∈ (0..^2)) →
(𝑓‘0) ∈ dom
𝐸) |
25 | 23, 24 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (𝑓‘0) ∈ dom 𝐸) |
26 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
𝐸 ∧ (𝑓‘0) ∈ dom 𝐸) → (𝐸‘(𝑓‘0)) ∈ ran 𝐸) |
27 | 25, 26 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (𝐸‘(𝑓‘0)) ∈ ran 𝐸) |
28 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} → ((𝐸‘(𝑓‘0)) ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)) |
29 | 27, 28 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → ((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} → {𝐴, 𝐵} ∈ ran 𝐸)) |
30 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
V |
31 | 30 | prid2 4242 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
{0, 1} |
32 | 31, 22 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
(0..^2) |
33 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓:(0..^2)⟶dom 𝐸 ∧ 1 ∈ (0..^2)) →
(𝑓‘1) ∈ dom
𝐸) |
34 | 32, 33 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (𝑓‘1) ∈ dom 𝐸) |
35 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
𝐸 ∧ (𝑓‘1) ∈ dom 𝐸) → (𝐸‘(𝑓‘1)) ∈ ran 𝐸) |
36 | 34, 35 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (𝐸‘(𝑓‘1)) ∈ ran 𝐸) |
37 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸‘(𝑓‘1)) = {𝐵, 𝐶} → ((𝐸‘(𝑓‘1)) ∈ ran 𝐸 ↔ {𝐵, 𝐶} ∈ ran 𝐸)) |
38 | 36, 37 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → ((𝐸‘(𝑓‘1)) = {𝐵, 𝐶} → {𝐵, 𝐶} ∈ ran 𝐸)) |
39 | 29, 38 | anim12d 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶}) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
40 | 19, 39 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → (((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶}) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
41 | 40 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑓:(0..^2)⟶dom 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶}) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) |
42 | 41 | expcom 450 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶}) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))) |
43 | 42 | com24 93 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶}) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))) |
44 | 43 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝑓:(0..^2)⟶dom 𝐸 → (𝑝:(0...2)⟶𝑉 → (((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶}) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))))) |
45 | 44 | 3imp 1249 |
. . . . . . . . . . . 12
⊢ ((𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝑓‘1)) = {𝐵, 𝐶})) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) |
46 | 18, 45 | syl6bi 242 |
. . . . . . . . . . 11
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))) |
47 | 46 | com14 94 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → ((𝑓:(0..^2)⟶dom 𝐸 ∧ 𝑝:(0...2)⟶𝑉 ∧ ((𝐸‘(𝑓‘0)) = {(𝑝‘0), (𝑝‘1)} ∧ (𝐸‘(𝑓‘1)) = {(𝑝‘1), (𝑝‘2)})) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))) |
48 | 9, 47 | sylbid 229 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))) |
49 | 48 | com14 94 |
. . . . . . . 8
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))))) |
50 | 49 | expdcom 454 |
. . . . . . 7
⊢ (𝑓(𝑉 Walks 𝐸)𝑝 → ((#‘𝑓) = 2 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))))) |
51 | 50 | 3imp 1249 |
. . . . . 6
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) |
52 | 51 | com13 86 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) |
53 | 52 | imp 444 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
54 | 53 | exlimdvv 1849 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
55 | | usg2wlk 26145 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
56 | 55 | 3expib 1260 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
57 | 56 | adantr 480 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
58 | 54, 57 | impbid 201 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
59 | 4, 58 | bitrd 267 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |