Proof of Theorem constr3pth
Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | | constr3cycl.f |
. . . . 5
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
3 | | constr3cycl.p |
. . . . 5
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
4 | 2, 3 | constr3lem1 26173 |
. . . 4
⊢ (𝐹 ∈ V ∧ 𝑃 ∈ V) |
5 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) → 𝑉 USGrph 𝐸) |
6 | 5 | ad2antrr 758 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝑉 USGrph 𝐸) |
7 | | simplr 788 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
8 | | simpr 476 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
9 | 2, 3 | constr3trl 26187 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹(𝑉 Trails 𝐸)𝑃) |
10 | 6, 7, 8, 9 | syl3anc 1318 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹(𝑉 Trails 𝐸)𝑃) |
11 | | 3cycl3dv 26170 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) |
12 | 11 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴))) |
13 | 12 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴))) |
14 | 13 | imp 444 |
. . . . . . . . . . 11
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) |
15 | 14 | simp2d 1067 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐵 ≠ 𝐶) |
16 | 2, 3 | constr3pthlem2 26184 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
17 | 7, 15, 16 | syl2anc 691 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |
18 | 2, 3 | constr3pthlem3 26185 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
19 | 7, 14, 18 | syl2anc 691 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
20 | 10, 17, 19 | 3jca 1235 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅)) |
21 | 20 | ex 449 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
22 | | ispth 26098 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
23 | 22 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) |
24 | 21, 23 | sylibrd 248 |
. . . . . 6
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Paths 𝐸)𝑃)) |
25 | 24 | ex 449 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Paths 𝐸)𝑃))) |
26 | 25 | ex 449 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Paths 𝐸)𝑃)))) |
27 | 4, 26 | mpan2 703 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Paths 𝐸)𝑃)))) |
28 | 1, 27 | mpcom 37 |
. 2
⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Paths 𝐸)𝑃))) |
29 | 28 | 3imp 1249 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹(𝑉 Paths 𝐸)𝑃) |