| Step | Hyp | Ref
| Expression |
| 1 | | umgrupgr 29120 |
. . . 4
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UPGraph) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐺 ∈ UPGraph) |
| 3 | | simp1 1137 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
| 4 | 3 | adantl 481 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
| 5 | | simpr3 1197 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉) |
| 6 | | s3wwlks2on.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 7 | 6 | s3wwlks2on 29976 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
| 8 | 2, 4, 5, 7 | syl3anc 1373 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
| 9 | | eqid 2737 |
. . . . . . . 8
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 10 | 6, 9 | upgr2wlk 29686 |
. . . . . . 7
⊢ (𝐺 ∈ UPGraph → ((𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})))) |
| 11 | 1, 10 | syl 17 |
. . . . . 6
⊢ (𝐺 ∈ UMGraph → ((𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})))) |
| 12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})))) |
| 13 | | s3fv0 14930 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
| 14 | 13 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
| 15 | | s3fv1 14931 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
| 16 | 15 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
| 17 | 14, 16 | preq12d 4741 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} = {𝐴, 𝐵}) |
| 18 | 17 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ↔
((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵})) |
| 19 | | s3fv2 14932 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
| 20 | 19 | 3ad2ant3 1136 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
| 21 | 16, 20 | preq12d 4741 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)} = {𝐵, 𝐶}) |
| 22 | 21 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)} ↔
((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) |
| 23 | 18, 22 | anbi12d 632 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)}) ↔
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) |
| 24 | 23 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)}) ↔
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) |
| 25 | 24 | 3anbi3d 1444 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ 〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})) ↔ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})))) |
| 26 | | umgruhgr 29121 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UHGraph) |
| 27 | 9 | uhgrfun 29083 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
| 28 | | fdmrn 6767 |
. . . . . . . . . . . 12
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) |
| 29 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) |
| 30 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) → 𝑓:(0..^2)⟶dom
(iEdg‘𝐺)) |
| 31 | | c0ex 11255 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V |
| 32 | 31 | prid1 4762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
{0, 1} |
| 33 | | fzo0to2pr 13789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0..^2) =
{0, 1} |
| 34 | 32, 33 | eleqtrri 2840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
(0..^2) |
| 35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) → 0
∈ (0..^2)) |
| 36 | 30, 35 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
(𝑓‘0) ∈ dom
(iEdg‘𝐺)) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(𝑓‘0) ∈ dom
(iEdg‘𝐺)) |
| 38 | 29, 37 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺)) |
| 39 | | 1ex 11257 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
V |
| 40 | 39 | prid2 4763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
{0, 1} |
| 41 | 40, 33 | eleqtrri 2840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
(0..^2) |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) → 1
∈ (0..^2)) |
| 43 | 30, 42 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
(𝑓‘1) ∈ dom
(iEdg‘𝐺)) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(𝑓‘1) ∈ dom
(iEdg‘𝐺)) |
| 45 | 29, 44 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)) |
| 46 | 38, 45 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
| 47 | 46 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺) →
(((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
| 48 | 47 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶ran (iEdg‘𝐺) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
| 49 | 48 | com12 32 |
. . . . . . . . . . . 12
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺) →
((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
| 50 | 28, 49 | sylbi 217 |
. . . . . . . . . . 11
⊢ (Fun
(iEdg‘𝐺) →
((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
| 51 | 26, 27, 50 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UMGraph → ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
| 52 | 51 | imp 406 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
| 53 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
| 54 | 53 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
| 55 | 54 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
| 56 | 55 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
| 57 | 56 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
| 58 | | usgrwwlks2on.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (Edg‘𝐺) |
| 59 | | edgval 29066 |
. . . . . . . . . . . . 13
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
| 60 | 58, 59 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ 𝐸 = ran (iEdg‘𝐺) |
| 61 | 60 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → 𝐸 = ran (iEdg‘𝐺)) |
| 62 | 57, 61 | eleq12d 2835 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐴, 𝐵} ∈ 𝐸 ↔ ((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺))) |
| 63 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶} ↔ {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
| 64 | 63 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶} → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
| 65 | 64 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
| 66 | 65 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
| 67 | 66 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
| 68 | 67, 61 | eleq12d 2835 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐵, 𝐶} ∈ 𝐸 ↔ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
| 69 | 62, 68 | anbi12d 632 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
| 70 | 52, 69 | mpbird 257 |
. . . . . . . 8
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) |
| 71 | 70 | ex 412 |
. . . . . . 7
⊢ (𝐺 ∈ UMGraph → ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
| 72 | 71 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ 〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
| 73 | 25, 72 | sylbid 240 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ 〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
| 74 | 12, 73 | sylbid 240 |
. . . 4
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
| 75 | 74 | exlimdv 1933 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
| 76 | 58 | umgr2wlk 29969 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
| 77 | | wlklenvp1 29636 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1)) |
| 78 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = (2 + 1)) |
| 79 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 + 1) =
3 |
| 80 | 78, 79 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = 3) |
| 81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑓)
= 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((♯‘𝑓) + 1) = 3) |
| 82 | 77, 81 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (♯‘𝑝) = 3) |
| 83 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 = (𝑝‘0) ↔ (𝑝‘0) = 𝐴) |
| 84 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 = (𝑝‘1) ↔ (𝑝‘1) = 𝐵) |
| 85 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐶 = (𝑝‘2) ↔ (𝑝‘2) = 𝐶) |
| 86 | 83, 84, 85 | 3anbi123i 1156 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
| 87 | 86 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
| 88 | 87 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑓)
= 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
| 89 | 88 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
| 90 | 82, 89 | jca 511 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶))) |
| 91 | 6 | wlkpwrd 29635 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
| 92 | 80 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑓) =
2 → ((♯‘𝑝)
= ((♯‘𝑓) + 1)
↔ (♯‘𝑝) =
3)) |
| 93 | 92 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = ((♯‘𝑓) + 1) ↔
(♯‘𝑝) =
3)) |
| 94 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉) |
| 95 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝑝) =
3 → (0..^(♯‘𝑝)) = (0..^3)) |
| 96 | | fzo0to3tp 13791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (0..^3) =
{0, 1, 2} |
| 97 | 95, 96 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝑝) =
3 → (0..^(♯‘𝑝)) = {0, 1, 2}) |
| 98 | 31 | tpid1 4768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 0 ∈
{0, 1, 2} |
| 99 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → (0 ∈
(0..^(♯‘𝑝))
↔ 0 ∈ {0, 1, 2})) |
| 100 | 98, 99 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → 0 ∈
(0..^(♯‘𝑝))) |
| 101 | | wrdsymbcl 14565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 0 ∈ (0..^(♯‘𝑝))) → (𝑝‘0) ∈ 𝑉) |
| 102 | 100, 101 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘0) ∈ 𝑉) |
| 103 | 39 | tpid2 4770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 1 ∈
{0, 1, 2} |
| 104 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → (1 ∈
(0..^(♯‘𝑝))
↔ 1 ∈ {0, 1, 2})) |
| 105 | 103, 104 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → 1 ∈
(0..^(♯‘𝑝))) |
| 106 | | wrdsymbcl 14565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 1 ∈ (0..^(♯‘𝑝))) → (𝑝‘1) ∈ 𝑉) |
| 107 | 105, 106 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘1) ∈ 𝑉) |
| 108 | | 2ex 12343 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 2 ∈
V |
| 109 | 108 | tpid3 4773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 2 ∈
{0, 1, 2} |
| 110 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → (2 ∈
(0..^(♯‘𝑝))
↔ 2 ∈ {0, 1, 2})) |
| 111 | 109, 110 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → 2 ∈
(0..^(♯‘𝑝))) |
| 112 | | wrdsymbcl 14565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 2 ∈ (0..^(♯‘𝑝))) → (𝑝‘2) ∈ 𝑉) |
| 113 | 111, 112 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘2) ∈ 𝑉) |
| 114 | 102, 107,
113 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
| 115 | 97, 114 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
| 116 | 115 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
| 117 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐴 = (𝑝‘0) → (𝐴 ∈ 𝑉 ↔ (𝑝‘0) ∈ 𝑉)) |
| 118 | 117 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ∈ 𝑉 ↔ (𝑝‘0) ∈ 𝑉)) |
| 119 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵 = (𝑝‘1) → (𝐵 ∈ 𝑉 ↔ (𝑝‘1) ∈ 𝑉)) |
| 120 | 119 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐵 ∈ 𝑉 ↔ (𝑝‘1) ∈ 𝑉)) |
| 121 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐶 = (𝑝‘2) → (𝐶 ∈ 𝑉 ↔ (𝑝‘2) ∈ 𝑉)) |
| 122 | 121 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐶 ∈ 𝑉 ↔ (𝑝‘2) ∈ 𝑉)) |
| 123 | 118, 120,
122 | 3anbi123d 1438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))) |
| 124 | 123 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))) |
| 125 | 116, 124 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
| 126 | 94, 125 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
| 127 | 126 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 ∈ Word 𝑉 → ((♯‘𝑝) = 3 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
| 128 | 127 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = 3 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
| 129 | 93, 128 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = ((♯‘𝑓) + 1) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
| 130 | 129 | impancom 451 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = ((♯‘𝑓) + 1)) → ((♯‘𝑓) = 2 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
| 131 | 130 | impd 410 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = ((♯‘𝑓) + 1)) → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
| 132 | 91, 77, 131 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
| 133 | 132 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
| 134 | | eqwrds3 15000 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑝 = 〈“𝐴𝐵𝐶”〉 ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)))) |
| 135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝 = 〈“𝐴𝐵𝐶”〉 ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)))) |
| 136 | 90, 135 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑝 = 〈“𝐴𝐵𝐶”〉) |
| 137 | 136 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)𝑝 ↔ 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
| 138 | 137 | biimpd 229 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)𝑝 → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
| 139 | 138 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝 → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉))) |
| 140 | 139 | pm2.43a 54 |
. . . . . . . . . . . . 13
⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
| 141 | 140 | 3impib 1117 |
. . . . . . . . . . . 12
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉) |
| 142 | 141 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉) |
| 143 | | simpr2 1196 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (♯‘𝑓) = 2) |
| 144 | 142, 143 | jca 511 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2)) |
| 145 | 144 | ex 412 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
| 146 | 145 | exlimdv 1933 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
| 147 | 146 | eximdv 1917 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
| 148 | 76, 147 | syl5com 31 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
| 149 | 148 | 3expib 1123 |
. . . . 5
⊢ (𝐺 ∈ UMGraph → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2)))) |
| 150 | 149 | com23 86 |
. . . 4
⊢ (𝐺 ∈ UMGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2)))) |
| 151 | 150 | imp 406 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
| 152 | 75, 151 | impbid 212 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
| 153 | 8, 152 | bitrd 279 |
1
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |