Proof of Theorem 1pthon
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢ {〈0,
𝑖〉} = {〈0, 𝑖〉} |
2 | | eqid 2610 |
. . . . 5
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉} = {〈0, 𝐴〉, 〈1, 𝐵〉} |
3 | 1, 2 | constr1trl 26118 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → {〈0, 𝑖〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉}) |
4 | | trliswlk 26069 |
. . . 4
⊢
({〈0, 𝑖〉}
(𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} → {〈0, 𝑖〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉}) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → {〈0, 𝑖〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉}) |
6 | | c0ex 9913 |
. . . . 5
⊢ 0 ∈
V |
7 | 6 | a1i 11 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 0 ∈ V) |
8 | | simp2l 1080 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 𝐴 ∈ 𝑉) |
9 | | 0ne1 10965 |
. . . . 5
⊢ 0 ≠
1 |
10 | 9 | a1i 11 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 0 ≠ 1) |
11 | | fvpr1g 6363 |
. . . 4
⊢ ((0
∈ V ∧ 𝐴 ∈
𝑉 ∧ 0 ≠ 1) →
({〈0, 𝐴〉,
〈1, 𝐵〉}‘0)
= 𝐴) |
12 | 7, 8, 10, 11 | syl3anc 1318 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴) |
13 | | 1ex 9914 |
. . . . 5
⊢ 1 ∈
V |
14 | 13 | a1i 11 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 1 ∈ V) |
15 | | simp2r 1081 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → 𝐵 ∈ 𝑉) |
16 | | opex 4859 |
. . . . . 6
⊢ 〈0,
𝑖〉 ∈
V |
17 | | hashsng 13020 |
. . . . . 6
⊢ (〈0,
𝑖〉 ∈ V →
(#‘{〈0, 𝑖〉}) = 1) |
18 | 16, 17 | ax-mp 5 |
. . . . 5
⊢
(#‘{〈0, 𝑖〉}) = 1 |
19 | | fveq2 6103 |
. . . . . 6
⊢
((#‘{〈0, 𝑖〉}) = 1 → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘(#‘{〈0,
𝑖〉})) = ({〈0,
𝐴〉, 〈1, 𝐵〉}‘1)) |
20 | | fvpr2g 6364 |
. . . . . 6
⊢ ((1
∈ V ∧ 𝐵 ∈
𝑉 ∧ 0 ≠ 1) →
({〈0, 𝐴〉,
〈1, 𝐵〉}‘1)
= 𝐵) |
21 | 19, 20 | sylan9eq 2664 |
. . . . 5
⊢
(((#‘{〈0, 𝑖〉}) = 1 ∧ (1 ∈ V ∧ 𝐵 ∈ 𝑉 ∧ 0 ≠ 1)) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘(#‘{〈0,
𝑖〉})) = 𝐵) |
22 | 18, 21 | mpan 702 |
. . . 4
⊢ ((1
∈ V ∧ 𝐵 ∈
𝑉 ∧ 0 ≠ 1) →
({〈0, 𝐴〉,
〈1, 𝐵〉}‘(#‘{〈0, 𝑖〉})) = 𝐵) |
23 | 14, 15, 10, 22 | syl3anc 1318 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘(#‘{〈0, 𝑖〉})) = 𝐵) |
24 | 5, 12, 23 | 3jca 1235 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → ({〈0, 𝑖〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴 ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘(#‘{〈0, 𝑖〉})) = 𝐵)) |
25 | 1, 2 | 1pthonlem1 26119 |
. . . 4
⊢ Fun ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ (1..^(#‘{〈0,
𝑖〉}))) |
26 | 25 | a1i 11 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → Fun ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ (1..^(#‘{〈0,
𝑖〉})))) |
27 | 1, 2 | 1pthonlem2 26120 |
. . . 4
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} “
{0, (#‘{〈0, 𝑖〉})}) ∩ ({〈0, 𝐴〉, 〈1, 𝐵〉} “ (1..^(#‘{〈0,
𝑖〉})))) =
∅ |
28 | 27 | a1i 11 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (({〈0, 𝐴〉, 〈1, 𝐵〉} “ {0, (#‘{〈0, 𝑖〉})}) ∩ ({〈0,
𝐴〉, 〈1, 𝐵〉} “
(1..^(#‘{〈0, 𝑖〉})))) = ∅) |
29 | 3, 26, 28 | 3jca 1235 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → ({〈0, 𝑖〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ Fun ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ (1..^(#‘{〈0,
𝑖〉}))) ∧
(({〈0, 𝐴〉,
〈1, 𝐵〉} “
{0, (#‘{〈0, 𝑖〉})}) ∩ ({〈0, 𝐴〉, 〈1, 𝐵〉} “ (1..^(#‘{〈0,
𝑖〉})))) =
∅)) |
30 | | simp1 1054 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) |
31 | | snex 4835 |
. . . . 5
⊢ {〈0,
𝑖〉} ∈
V |
32 | | prex 4836 |
. . . . 5
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉} ∈
V |
33 | 31, 32 | pm3.2i 470 |
. . . 4
⊢
({〈0, 𝑖〉}
∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ V) |
34 | 33 | a1i 11 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → ({〈0, 𝑖〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉} ∈
V)) |
35 | | simp2 1055 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
36 | | ispthon 26106 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({〈0, 𝑖〉} (𝐴(𝑉 PathOn 𝐸)𝐵){〈0, 𝐴〉, 〈1, 𝐵〉} ↔ ({〈0, 𝑖〉} (𝐴(𝑉 WalkOn 𝐸)𝐵){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ {〈0, 𝑖〉} (𝑉 Paths 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉}))) |
37 | | iswlkon 26062 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({〈0, 𝑖〉} (𝐴(𝑉 WalkOn 𝐸)𝐵){〈0, 𝐴〉, 〈1, 𝐵〉} ↔ ({〈0, 𝑖〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴 ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘(#‘{〈0, 𝑖〉})) = 𝐵))) |
38 | | ispth 26098 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ V)) →
({〈0, 𝑖〉} (𝑉 Paths 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ↔ ({〈0, 𝑖〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ Fun ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ (1..^(#‘{〈0,
𝑖〉}))) ∧
(({〈0, 𝐴〉,
〈1, 𝐵〉} “
{0, (#‘{〈0, 𝑖〉})}) ∩ ({〈0, 𝐴〉, 〈1, 𝐵〉} “ (1..^(#‘{〈0,
𝑖〉})))) =
∅))) |
39 | 38 | 3adant3 1074 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({〈0, 𝑖〉} (𝑉 Paths 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ↔ ({〈0, 𝑖〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ Fun ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ (1..^(#‘{〈0,
𝑖〉}))) ∧
(({〈0, 𝐴〉,
〈1, 𝐵〉} “
{0, (#‘{〈0, 𝑖〉})}) ∩ ({〈0, 𝐴〉, 〈1, 𝐵〉} “ (1..^(#‘{〈0,
𝑖〉})))) =
∅))) |
40 | 37, 39 | anbi12d 743 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (({〈0, 𝑖〉} (𝐴(𝑉 WalkOn 𝐸)𝐵){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ {〈0, 𝑖〉} (𝑉 Paths 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉}) ↔ (({〈0, 𝑖〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴 ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘(#‘{〈0, 𝑖〉})) = 𝐵) ∧ ({〈0, 𝑖〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ Fun ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ (1..^(#‘{〈0,
𝑖〉}))) ∧
(({〈0, 𝐴〉,
〈1, 𝐵〉} “
{0, (#‘{〈0, 𝑖〉})}) ∩ ({〈0, 𝐴〉, 〈1, 𝐵〉} “ (1..^(#‘{〈0,
𝑖〉})))) =
∅)))) |
41 | 36, 40 | bitrd 267 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ({〈0, 𝑖〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉} ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({〈0, 𝑖〉} (𝐴(𝑉 PathOn 𝐸)𝐵){〈0, 𝐴〉, 〈1, 𝐵〉} ↔ (({〈0, 𝑖〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴 ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘(#‘{〈0, 𝑖〉})) = 𝐵) ∧ ({〈0, 𝑖〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ Fun ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ (1..^(#‘{〈0,
𝑖〉}))) ∧
(({〈0, 𝐴〉,
〈1, 𝐵〉} “
{0, (#‘{〈0, 𝑖〉})}) ∩ ({〈0, 𝐴〉, 〈1, 𝐵〉} “ (1..^(#‘{〈0,
𝑖〉})))) =
∅)))) |
42 | 30, 34, 35, 41 | syl3anc 1318 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → ({〈0, 𝑖〉} (𝐴(𝑉 PathOn 𝐸)𝐵){〈0, 𝐴〉, 〈1, 𝐵〉} ↔ (({〈0, 𝑖〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴 ∧ ({〈0, 𝐴〉, 〈1, 𝐵〉}‘(#‘{〈0, 𝑖〉})) = 𝐵) ∧ ({〈0, 𝑖〉} (𝑉 Trails 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉} ∧ Fun ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ (1..^(#‘{〈0,
𝑖〉}))) ∧
(({〈0, 𝐴〉,
〈1, 𝐵〉} “
{0, (#‘{〈0, 𝑖〉})}) ∩ ({〈0, 𝐴〉, 〈1, 𝐵〉} “ (1..^(#‘{〈0,
𝑖〉})))) =
∅)))) |
43 | 24, 29, 42 | mpbir2and 959 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐸‘𝑖) = {𝐴, 𝐵}) → {〈0, 𝑖〉} (𝐴(𝑉 PathOn 𝐸)𝐵){〈0, 𝐴〉, 〈1, 𝐵〉}) |