Proof of Theorem 2pthon
Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑖 ∈ V |
2 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑗 ∈ V |
3 | 1, 2 | pm3.2i 470 |
. . . . . . . 8
⊢ (𝑖 ∈ V ∧ 𝑗 ∈ V) |
4 | | eqid 2610 |
. . . . . . . 8
⊢ {〈0,
𝑖〉, 〈1, 𝑗〉} = {〈0, 𝑖〉, 〈1, 𝑗〉} |
5 | | eqid 2610 |
. . . . . . . 8
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
6 | 3, 4, 5 | constr2trl 26129 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶}) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉})) |
7 | 6 | 3adant3 1074 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶}) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉})) |
8 | 7 | imp 444 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) |
9 | | trliswlk 26069 |
. . . . 5
⊢
({〈0, 𝑖〉,
〈1, 𝑗〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) |
11 | | c0ex 9913 |
. . . . . . . . 9
⊢ 0 ∈
V |
12 | 11 | jctl 562 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (0 ∈ V ∧ 𝐴 ∈ 𝑉)) |
13 | 12 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (0 ∈ V ∧ 𝐴 ∈ 𝑉)) |
14 | | 0ne1 10965 |
. . . . . . . 8
⊢ 0 ≠
1 |
15 | | 0ne2 11116 |
. . . . . . . 8
⊢ 0 ≠
2 |
16 | 14, 15 | pm3.2i 470 |
. . . . . . 7
⊢ (0 ≠ 1
∧ 0 ≠ 2) |
17 | | fvtp1g 6368 |
. . . . . . 7
⊢ (((0
∈ V ∧ 𝐴 ∈
𝑉) ∧ (0 ≠ 1 ∧ 0
≠ 2)) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) = 𝐴) |
18 | 13, 16, 17 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) = 𝐴) |
19 | 18 | 3ad2ant2 1076 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) = 𝐴) |
20 | 19 | adantr 480 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) = 𝐴) |
21 | | ax-1ne0 9884 |
. . . . . . . . 9
⊢ 1 ≠
0 |
22 | 21 | nesymi 2839 |
. . . . . . . 8
⊢ ¬ 0
= 1 |
23 | 11, 1 | opth1 4870 |
. . . . . . . . 9
⊢ (〈0,
𝑖〉 = 〈1, 𝑗〉 → 0 =
1) |
24 | 23 | necon3bi 2808 |
. . . . . . . 8
⊢ (¬ 0
= 1 → 〈0, 𝑖〉
≠ 〈1, 𝑗〉) |
25 | 22, 24 | ax-mp 5 |
. . . . . . 7
⊢ 〈0,
𝑖〉 ≠ 〈1, 𝑗〉 |
26 | | opex 4859 |
. . . . . . . 8
⊢ 〈0,
𝑖〉 ∈
V |
27 | | opex 4859 |
. . . . . . . 8
⊢ 〈1,
𝑗〉 ∈
V |
28 | | hashprgOLD 13044 |
. . . . . . . 8
⊢
((〈0, 𝑖〉
∈ V ∧ 〈1, 𝑗〉 ∈ V) → (〈0, 𝑖〉 ≠ 〈1, 𝑗〉 ↔ (#‘{〈0,
𝑖〉, 〈1, 𝑗〉}) = 2)) |
29 | 26, 27, 28 | mp2an 704 |
. . . . . . 7
⊢ (〈0,
𝑖〉 ≠ 〈1, 𝑗〉 ↔ (#‘{〈0,
𝑖〉, 〈1, 𝑗〉}) = 2) |
30 | 25, 29 | mpbi 219 |
. . . . . 6
⊢
(#‘{〈0, 𝑖〉, 〈1, 𝑗〉}) = 2 |
31 | 30 | fveq2i 6106 |
. . . . 5
⊢
({〈0, 𝐴〉,
〈1, 𝐵〉, 〈2,
𝐶〉}‘(#‘{〈0, 𝑖〉, 〈1, 𝑗〉})) = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2) |
32 | | 2z 11286 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
33 | 32 | jctl 562 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → (2 ∈ ℤ ∧ 𝐶 ∈ 𝑉)) |
34 | 33 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (2 ∈ ℤ ∧ 𝐶 ∈ 𝑉)) |
35 | | 1ne2 11117 |
. . . . . . . . 9
⊢ 1 ≠
2 |
36 | 15, 35 | pm3.2i 470 |
. . . . . . . 8
⊢ (0 ≠ 2
∧ 1 ≠ 2) |
37 | | fvtp3g 6370 |
. . . . . . . 8
⊢ (((2
∈ ℤ ∧ 𝐶
∈ 𝑉) ∧ (0 ≠ 2
∧ 1 ≠ 2)) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2) = 𝐶) |
38 | 34, 36, 37 | sylancl 693 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2) = 𝐶) |
39 | 38 | 3ad2ant2 1076 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2) = 𝐶) |
40 | 39 | adantr 480 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2) = 𝐶) |
41 | 31, 40 | syl5eq 2656 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘(#‘{〈0, 𝑖〉, 〈1, 𝑗〉})) = 𝐶) |
42 | | simpl1 1057 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) |
43 | | prex 4836 |
. . . . . . . 8
⊢ {〈0,
𝑖〉, 〈1, 𝑗〉} ∈
V |
44 | | tpex 6855 |
. . . . . . . 8
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈
V |
45 | 43, 44 | pm3.2i 470 |
. . . . . . 7
⊢
({〈0, 𝑖〉,
〈1, 𝑗〉} ∈ V
∧ {〈0, 𝐴〉,
〈1, 𝐵〉, 〈2,
𝐶〉} ∈
V) |
46 | 45 | a1i 11 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → ({〈0, 𝑖〉, 〈1, 𝑗〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈
V)) |
47 | | 3simpb 1052 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
48 | 47 | 3ad2ant2 1076 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
49 | 48 | adantr 480 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
50 | 42, 46, 49 | 3jca 1235 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉, 〈1, 𝑗〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
51 | | iswlkon 26062 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉, 〈1, 𝑗〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 WalkOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ↔ ({〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) = 𝐴 ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘(#‘{〈0, 𝑖〉, 〈1, 𝑗〉})) = 𝐶))) |
52 | 50, 51 | syl 17 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → ({〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 WalkOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ↔ ({〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) = 𝐴 ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘(#‘{〈0, 𝑖〉, 〈1, 𝑗〉})) = 𝐶))) |
53 | 10, 20, 41, 52 | mpbir3and 1238 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 WalkOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) |
54 | 3, 4, 5 | constr2pth 26131 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶}) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Paths 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉})) |
55 | 54 | imp 444 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Paths 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) |
56 | | ispthon 26106 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉, 〈1, 𝑗〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ↔ ({〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 WalkOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Paths 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}))) |
57 | 50, 56 | syl 17 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → ({〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ↔ ({〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 WalkOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ {〈0, 𝑖〉, 〈1, 𝑗〉} (𝑉 Paths 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}))) |
58 | 53, 55, 57 | mpbir2and 959 |
. 2
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶})) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) |
59 | 58 | ex 449 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑖 ≠ 𝑗 ∧ (𝐸‘𝑖) = {𝐴, 𝐵} ∧ (𝐸‘𝑗) = {𝐵, 𝐶}) → {〈0, 𝑖〉, 〈1, 𝑗〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉})) |