Step | Hyp | Ref
| Expression |
1 | | usgr2pthspth 40968 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
(𝐹(PathS‘𝐺)𝑃 ↔ 𝐹(SPathS‘𝐺)𝑃)) |
2 | | usgrupgr 40412 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph
) |
3 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
𝐺 ∈ UPGraph
) |
4 | | sPthis1wlk 40934 |
. . . . . . . . . . . 12
⊢ (𝐹(SPathS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
5 | | wlkv 40815 |
. . . . . . . . . . . . 13
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
6 | | 3simpc 1053 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹(SPathS‘𝐺)𝑃 → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
9 | 3, 8 | anim12i 588 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) ∧
𝐹(SPathS‘𝐺)𝑃) → (𝐺 ∈ UPGraph ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
10 | | 3anass 1035 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ↔ (𝐺 ∈ UPGraph ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
11 | 9, 10 | sylibr 223 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) ∧
𝐹(SPathS‘𝐺)𝑃) → (𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
12 | | issPth 40930 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) |
13 | | usgr2pthlem.v |
. . . . . . . . . . . . . . 15
⊢ 𝑉 = (Vtx‘𝐺) |
14 | | usgr2pthlem.i |
. . . . . . . . . . . . . . 15
⊢ 𝐼 = (iEdg‘𝐺) |
15 | 13, 14 | upgrf1istrl 40911 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(TrailS‘𝐺)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
16 | 15 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃) ↔ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃))) |
17 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
(0..^2)) |
18 | | f1eq2 6010 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((0..^(#‘𝐹)) =
(0..^2) → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ↔ 𝐹:(0..^2)–1-1→dom 𝐼)) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ↔ 𝐹:(0..^2)–1-1→dom 𝐼)) |
20 | 19 | biimpd 218 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 → 𝐹:(0..^2)–1-1→dom 𝐼)) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
(𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 → 𝐹:(0..^2)–1-1→dom 𝐼)) |
22 | 21 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → 𝐹:(0..^2)–1-1→dom 𝐼)) |
23 | 22 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → 𝐹:(0..^2)–1-1→dom 𝐼)) |
24 | 23 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃)) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → 𝐹:(0..^2)–1-1→dom 𝐼)) |
25 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐹) = 2
→ (0...(#‘𝐹)) =
(0...2)) |
26 | 25 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...2)⟶𝑉)) |
27 | | df-f1 5809 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃:(0...2)–1-1→𝑉 ↔ (𝑃:(0...2)⟶𝑉 ∧ Fun ◡𝑃)) |
28 | 27 | simplbi2 653 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃:(0...2)⟶𝑉 → (Fun ◡𝑃 → 𝑃:(0...2)–1-1→𝑉)) |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 2
→ (𝑃:(0...2)⟶𝑉 → (Fun ◡𝑃 → 𝑃:(0...2)–1-1→𝑉))) |
30 | 26, 29 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 2
→ (𝑃:(0...(#‘𝐹))⟶𝑉 → (Fun ◡𝑃 → 𝑃:(0...2)–1-1→𝑉))) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
(𝑃:(0...(#‘𝐹))⟶𝑉 → (Fun ◡𝑃 → 𝑃:(0...2)–1-1→𝑉))) |
32 | 31 | com3l 87 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (Fun ◡𝑃 → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → 𝑃:(0...2)–1-1→𝑉))) |
33 | 32 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (Fun ◡𝑃 → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → 𝑃:(0...2)–1-1→𝑉))) |
34 | 33 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → 𝑃:(0...2)–1-1→𝑉)) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃)) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → 𝑃:(0...2)–1-1→𝑉)) |
36 | 13, 14 | usgr2pthlem 40969 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))) |
37 | 36 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃)) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))) |
38 | 24, 35, 37 | 3jcad 1236 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃)) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) |
39 | 38 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))) |
40 | 16, 39 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))) |
41 | 12, 40 | sylbid 229 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(SPathS‘𝐺)𝑃 → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))) |
42 | 41 | com23 84 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
(𝐹(SPathS‘𝐺)𝑃 → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))) |
43 | 42 | impd 446 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) ∧
𝐹(SPathS‘𝐺)𝑃) → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) |
44 | 11, 43 | mpcom 37 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) ∧
𝐹(SPathS‘𝐺)𝑃) → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))) |
45 | 44 | ex 449 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
(𝐹(SPathS‘𝐺)𝑃 → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) |
46 | 1, 45 | sylbid 229 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧
(#‘𝐹) = 2) →
(𝐹(PathS‘𝐺)𝑃 → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) |
47 | 46 | ex 449 |
. . . . 5
⊢ (𝐺 ∈ USGraph →
((#‘𝐹) = 2 →
(𝐹(PathS‘𝐺)𝑃 → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))) |
48 | 47 | com13 86 |
. . . 4
⊢ (𝐹(PathS‘𝐺)𝑃 → ((#‘𝐹) = 2 → (𝐺 ∈ USGraph → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))) |
49 | 48 | imp 444 |
. . 3
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2) → (𝐺 ∈ USGraph → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) |
50 | 49 | com12 32 |
. 2
⊢ (𝐺 ∈ USGraph → ((𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2) → (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) |
51 | | 2nn0 11186 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
52 | | f1f 6014 |
. . . . . 6
⊢ (𝐹:(0..^2)–1-1→dom 𝐼 → 𝐹:(0..^2)⟶dom 𝐼) |
53 | | fnfzo0hash 13091 |
. . . . . 6
⊢ ((2
∈ ℕ0 ∧ 𝐹:(0..^2)⟶dom 𝐼) → (#‘𝐹) = 2) |
54 | 51, 52, 53 | sylancr 694 |
. . . . 5
⊢ (𝐹:(0..^2)–1-1→dom 𝐼 → (#‘𝐹) = 2) |
55 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 =
(#‘𝐹) → (0..^2)
= (0..^(#‘𝐹))) |
56 | 55 | eqcoms 2618 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 2
→ (0..^2) = (0..^(#‘𝐹))) |
57 | | f1eq2 6010 |
. . . . . . . . . . . . . . . . 17
⊢ ((0..^2)
= (0..^(#‘𝐹)) →
(𝐹:(0..^2)–1-1→dom 𝐼 ↔ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^2)–1-1→dom 𝐼 ↔ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼)) |
59 | 58 | biimpd 218 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^2)–1-1→dom 𝐼 → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼)) |
60 | 59 | imp 444 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼) |
62 | 61 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼) |
63 | | f1f 6014 |
. . . . . . . . . . . . . . 15
⊢ (𝑃:(0...2)–1-1→𝑉 → 𝑃:(0...2)⟶𝑉) |
64 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 =
(#‘𝐹) → (0...2)
= (0...(#‘𝐹))) |
65 | 64 | eqcoms 2618 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 2
→ (0...2) = (0...(#‘𝐹))) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) → (0...2) = (0...(#‘𝐹))) |
67 | 66 | feq2d 5944 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) → (𝑃:(0...2)⟶𝑉 ↔ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
68 | 63, 67 | syl5ib 233 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) → (𝑃:(0...2)–1-1→𝑉 → 𝑃:(0...(#‘𝐹))⟶𝑉)) |
69 | 68 | imp 444 |
. . . . . . . . . . . . 13
⊢
((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
70 | 69 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
71 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃‘0) = 𝑥 ↔ 𝑥 = (𝑃‘0)) |
72 | 71 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃‘0) = 𝑥 → 𝑥 = (𝑃‘0)) |
73 | 72 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → 𝑥 = (𝑃‘0)) |
74 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃‘1) = 𝑦 ↔ 𝑦 = (𝑃‘1)) |
75 | 74 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃‘1) = 𝑦 → 𝑦 = (𝑃‘1)) |
76 | 75 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → 𝑦 = (𝑃‘1)) |
77 | 73, 76 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → {𝑥, 𝑦} = {(𝑃‘0), (𝑃‘1)}) |
78 | 77 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
79 | 78 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} → (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
80 | 79 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} → (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}) → (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
82 | 81 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)}) |
83 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃‘2) = 𝑧 ↔ 𝑧 = (𝑃‘2)) |
84 | 83 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃‘2) = 𝑧 → 𝑧 = (𝑃‘2)) |
85 | 84 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → 𝑧 = (𝑃‘2)) |
86 | 76, 85 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → {𝑦, 𝑧} = {(𝑃‘1), (𝑃‘2)}) |
87 | 86 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → ((𝐼‘(𝐹‘1)) = {𝑦, 𝑧} ↔ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
88 | 87 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → ((𝐼‘(𝐹‘1)) = {𝑦, 𝑧} → (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
89 | 88 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼‘(𝐹‘1)) = {𝑦, 𝑧} → (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}) → (((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) → (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
91 | 90 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) |
92 | 82, 91 | jca 553 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
93 | 92 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧 ∈
(𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
94 | 93 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦 ∈
(𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
95 | 94 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥 ∈
𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
96 | 95 | a1i13 27 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ (∃𝑥 ∈
𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
97 | | fzo0to2pr 12420 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0..^2) =
{0, 1} |
98 | 17, 97 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 2
→ (0..^(#‘𝐹)) =
{0, 1}) |
99 | 98 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) = 2
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ {0, 1} (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
100 | | 2wlklem 26094 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑖 ∈
{0, 1} (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
101 | 99, 100 | syl6bb 275 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) = 2
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))) |
102 | 101 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 2
→ ((𝐺 ∈ USGraph
→ ∀𝑖 ∈
(0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (𝐺 ∈ USGraph → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) |
103 | 102 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 2
→ ((∃𝑥 ∈
𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ↔ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))))) |
104 | 96, 103 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 2
→ (∃𝑥 ∈
𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
105 | 104 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
106 | 105 | imp 444 |
. . . . . . . . . . . . 13
⊢
(((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) → (𝐺 ∈ USGraph → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
107 | 106 | imp 444 |
. . . . . . . . . . . 12
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
108 | 62, 70, 107 | 3jca 1235 |
. . . . . . . . . . 11
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
109 | 27 | simprbi 479 |
. . . . . . . . . . . . 13
⊢ (𝑃:(0...2)–1-1→𝑉 → Fun ◡𝑃) |
110 | 109 | adantl 481 |
. . . . . . . . . . . 12
⊢
((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) → Fun ◡𝑃) |
111 | 110 | ad2antrr 758 |
. . . . . . . . . . 11
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → Fun ◡𝑃) |
112 | 108, 111 | jca 553 |
. . . . . . . . . 10
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃)) |
113 | 2 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → 𝐺 ∈ UPGraph ) |
114 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢ (0..^2)
∈ V |
115 | | fex 6394 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:(0..^2)⟶dom 𝐼 ∧ (0..^2) ∈ V) →
𝐹 ∈
V) |
116 | 52, 114, 115 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:(0..^2)–1-1→dom 𝐼 → 𝐹 ∈ V) |
117 | 116 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) → 𝐹 ∈ V) |
118 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ (0...2)
∈ V |
119 | | fex 6394 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃:(0...2)⟶𝑉 ∧ (0...2) ∈ V) →
𝑃 ∈
V) |
120 | 63, 118, 119 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝑃:(0...2)–1-1→𝑉 → 𝑃 ∈ V) |
121 | 117, 120 | anim12i 588 |
. . . . . . . . . . . . . 14
⊢
((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
122 | 121 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
123 | 113, 122 | jca 553 |
. . . . . . . . . . . 12
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → (𝐺 ∈ UPGraph ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
124 | 123, 10 | sylibr 223 |
. . . . . . . . . . 11
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → (𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
125 | 12, 16 | bitrd 267 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(SPathS‘𝐺)𝑃 ↔ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃))) |
126 | 124, 125 | syl 17 |
. . . . . . . . . 10
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → (𝐹(SPathS‘𝐺)𝑃 ↔ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ Fun ◡𝑃))) |
127 | 112, 126 | mpbird 246 |
. . . . . . . . 9
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → 𝐹(SPathS‘𝐺)𝑃) |
128 | | simpr 476 |
. . . . . . . . . 10
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → 𝐺 ∈ USGraph ) |
129 | | simp-4l 802 |
. . . . . . . . . 10
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → (#‘𝐹) = 2) |
130 | 128, 129,
1 | syl2anc 691 |
. . . . . . . . 9
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → (𝐹(PathS‘𝐺)𝑃 ↔ 𝐹(SPathS‘𝐺)𝑃)) |
131 | 127, 130 | mpbird 246 |
. . . . . . . 8
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → 𝐹(PathS‘𝐺)𝑃) |
132 | 131, 129 | jca 553 |
. . . . . . 7
⊢
((((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) ∧ 𝐺 ∈ USGraph ) → (𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2)) |
133 | 132 | ex 449 |
. . . . . 6
⊢
(((((#‘𝐹) = 2
∧ 𝐹:(0..^2)–1-1→dom 𝐼) ∧ 𝑃:(0...2)–1-1→𝑉) ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) → (𝐺 ∈ USGraph → (𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2))) |
134 | 133 | exp41 636 |
. . . . 5
⊢
((#‘𝐹) = 2
→ (𝐹:(0..^2)–1-1→dom 𝐼 → (𝑃:(0...2)–1-1→𝑉 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → (𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2)))))) |
135 | 54, 134 | mpcom 37 |
. . . 4
⊢ (𝐹:(0..^2)–1-1→dom 𝐼 → (𝑃:(0...2)–1-1→𝑉 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})) → (𝐺 ∈ USGraph → (𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2))))) |
136 | 135 | 3imp 1249 |
. . 3
⊢ ((𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) → (𝐺 ∈ USGraph → (𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2))) |
137 | 136 | com12 32 |
. 2
⊢ (𝐺 ∈ USGraph → ((𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))) → (𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2))) |
138 | 50, 137 | impbid 201 |
1
⊢ (𝐺 ∈ USGraph → ((𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) |