| 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 | | simplr 788 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 USGrph 𝐸) |
| 6 | 2, 3 | constr3trllem1 26178 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹 ∈ Word dom 𝐸) |
| 7 | 5, 6 | sylan 487 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹 ∈ Word dom 𝐸) |
| 8 | 2, 3 | constr3trllem2 26179 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → Fun ◡𝐹) |
| 9 | 5, 8 | sylan 487 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → Fun ◡𝐹) |
| 10 | 7, 9 | jca 553 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹)) |
| 11 | 2, 3 | constr3trllem3 26180 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
| 12 | 11 | ad2antlr 759 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
| 13 | 2, 3 | constr3trllem5 26182 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 14 | 5, 13 | sylan 487 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
| 15 | 10, 12, 14 | 3jca 1235 |
. . . . . . . 8
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
| 16 | 15 | ex 449 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 17 | | istrl 26067 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 18 | 17 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
| 19 | 16, 18 | sylibrd 248 |
. . . . . 6
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Trails 𝐸)𝑃)) |
| 20 | 19 | ex 449 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝑉 USGrph 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Trails 𝐸)𝑃))) |
| 21 | 20 | ex 449 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Trails 𝐸)𝑃)))) |
| 22 | 4, 21 | mpan2 703 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Trails 𝐸)𝑃)))) |
| 23 | 1, 22 | mpcom 37 |
. 2
⊢ (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → 𝐹(𝑉 Trails 𝐸)𝑃))) |
| 24 | 23 | 3imp 1249 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹(𝑉 Trails 𝐸)𝑃) |
