Proof of Theorem constr2pth
Step | Hyp | Ref
| Expression |
1 | | 2trlY.i |
. . . . . 6
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) |
2 | | 2trlY.f |
. . . . . 6
⊢ 𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} |
3 | | 2trlY.p |
. . . . . 6
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
4 | 1, 2, 3 | constr2trl 26129 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → 𝐹(𝑉 Trails 𝐸)𝑃)) |
5 | 4 | 3adant3 1074 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → 𝐹(𝑉 Trails 𝐸)𝑃)) |
6 | 5 | imp 444 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → 𝐹(𝑉 Trails 𝐸)𝑃) |
7 | 3 | 2pthlem1 26125 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → Fun ◡(𝑃 ↾ (1..^2))) |
8 | 1, 2 | 2trllemA 26080 |
. . . . . . 7
⊢
(#‘𝐹) =
2 |
9 | | oveq2 6557 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (1..^(#‘𝐹)) =
(1..^2)) |
10 | 9 | reseq2d 5317 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ (𝑃 ↾
(1..^(#‘𝐹))) = (𝑃 ↾
(1..^2))) |
11 | 10 | cnveqd 5220 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ ◡(𝑃 ↾ (1..^(#‘𝐹))) = ◡(𝑃 ↾ (1..^2))) |
12 | 11 | funeqd 5825 |
. . . . . . 7
⊢
((#‘𝐹) = 2
→ (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ↔ Fun ◡(𝑃 ↾ (1..^2)))) |
13 | 8, 12 | ax-mp 5 |
. . . . . 6
⊢ (Fun
◡(𝑃 ↾ (1..^(#‘𝐹))) ↔ Fun ◡(𝑃 ↾ (1..^2))) |
14 | 7, 13 | sylibr 223 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
15 | 14 | 3ad2ant2 1076 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
16 | 15 | adantr 480 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
17 | 3 | 2pthlem2 26126 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ((𝑃 “ {0, 2}) ∩ (𝑃 “ (1..^2))) =
∅) |
18 | | preq2 4213 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 2
→ {0, (#‘𝐹)} =
{0, 2}) |
19 | 18 | imaeq2d 5385 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (𝑃 “ {0,
(#‘𝐹)}) = (𝑃 “ {0,
2})) |
20 | 9 | imaeq2d 5385 |
. . . . . . . . . 10
⊢
((#‘𝐹) = 2
→ (𝑃 “
(1..^(#‘𝐹))) = (𝑃 “
(1..^2))) |
21 | 19, 20 | ineq12d 3777 |
. . . . . . . . 9
⊢
((#‘𝐹) = 2
→ ((𝑃 “ {0,
(#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ((𝑃 “ {0, 2}) ∩ (𝑃 “ (1..^2)))) |
22 | 21 | eqeq1d 2612 |
. . . . . . . 8
⊢
((#‘𝐹) = 2
→ (((𝑃 “ {0,
(#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ ↔ ((𝑃 “ {0, 2}) ∩ (𝑃 “ (1..^2))) =
∅)) |
23 | 8, 22 | ax-mp 5 |
. . . . . . 7
⊢ (((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ ↔ ((𝑃 “ {0, 2}) ∩ (𝑃 “ (1..^2))) =
∅) |
24 | 17, 23 | sylibr 223 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
25 | 24 | 3adantr2 1214 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
26 | 25 | 3adant1 1072 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
27 | 26 | adantr 480 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
28 | | prex 4836 |
. . . . . . . . 9
⊢ {〈0,
𝐼〉, 〈1, 𝐽〉} ∈
V |
29 | 2, 28 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐹 ∈ V |
30 | | tpex 6855 |
. . . . . . . . 9
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈
V |
31 | 3, 30 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑃 ∈ V |
32 | 29, 31 | pm3.2i 470 |
. . . . . . 7
⊢ (𝐹 ∈ V ∧ 𝑃 ∈ V) |
33 | 32 | jctr 563 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
34 | 33 | 3ad2ant1 1075 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
35 | 34 | adantr 480 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
36 | | ispth 26098 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
37 | 35, 36 | syl 17 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
38 | 6, 16, 27, 37 | mpbir3and 1238 |
. 2
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ (𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → 𝐹(𝑉 Paths 𝐸)𝑃) |
39 | 38 | ex 449 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝐼 ≠ 𝐽 ∧ (𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → 𝐹(𝑉 Paths 𝐸)𝑃)) |