Step | Hyp | Ref
| Expression |
1 | | umgrupgr 27473 |
. . . 4
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UPGraph) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐺 ∈ UPGraph) |
3 | | simp1 1135 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
4 | 3 | adantl 482 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
5 | | simpr3 1195 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉) |
6 | | s3wwlks2on.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
7 | 6 | s3wwlks2on 28321 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
8 | 2, 4, 5, 7 | syl3anc 1370 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
9 | | eqid 2738 |
. . . . . . . 8
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
10 | 6, 9 | upgr2wlk 28036 |
. . . . . . 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 481 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) ↔ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})))) |
13 | | s3fv0 14604 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
14 | 13 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
15 | | s3fv1 14605 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
16 | 15 | 3ad2ant2 1133 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
17 | 14, 16 | preq12d 4677 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} = {𝐴, 𝐵}) |
18 | 17 | eqeq2d 2749 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ↔
((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵})) |
19 | | s3fv2 14606 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
20 | 19 | 3ad2ant3 1134 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
21 | 16, 20 | preq12d 4677 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)} = {𝐵, 𝐶}) |
22 | 21 | eqeq2d 2749 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)} ↔
((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) |
23 | 18, 22 | anbi12d 631 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)}) ↔
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) |
24 | 23 | adantl 482 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)}) ↔
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) |
25 | 24 | 3anbi3d 1441 |
. . . . . 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 27474 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UHGraph) |
27 | 9 | uhgrfun 27436 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
28 | | fdmrn 6632 |
. . . . . . . . . . . 12
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) |
29 | | simpr 485 |
. . . . . . . . . . . . . . . . 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 10969 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V |
32 | 31 | prid1 4698 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
{0, 1} |
33 | | fzo0to2pr 13472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0..^2) =
{0, 1} |
34 | 32, 33 | eleqtrri 2838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
(0..^2) |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) → 0
∈ (0..^2)) |
36 | 30, 35 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
(𝑓‘0) ∈ dom
(iEdg‘𝐺)) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(𝑓‘0) ∈ dom
(iEdg‘𝐺)) |
38 | 29, 37 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺)) |
39 | | 1ex 10971 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
V |
40 | 39 | prid2 4699 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
{0, 1} |
41 | 40, 33 | eleqtrri 2838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
(0..^2) |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) → 1
∈ (0..^2)) |
43 | 30, 42 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
(𝑓‘1) ∈ dom
(iEdg‘𝐺)) |
44 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(𝑓‘1) ∈ dom
(iEdg‘𝐺)) |
45 | 29, 44 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)) |
46 | 38, 45 | jca 512 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺)) →
(((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
47 | 46 | ex 413 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) →
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶ran
(iEdg‘𝐺) →
(((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
48 | 47 | 3ad2ant1 1132 |
. . . . . . . . . . . . 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 216 |
. . . . . . . . . . 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 407 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
53 | | eqcom 2745 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
54 | 53 | biimpi 215 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
55 | 54 | adantr 481 |
. . . . . . . . . . . . 13
⊢
((((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
56 | 55 | 3ad2ant3 1134 |
. . . . . . . . . . . 12
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
57 | 56 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → {𝐴, 𝐵} = ((iEdg‘𝐺)‘(𝑓‘0))) |
58 | | usgrwwlks2on.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (Edg‘𝐺) |
59 | | edgval 27419 |
. . . . . . . . . . . . 13
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
60 | 58, 59 | eqtri 2766 |
. . . . . . . . . . . 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 2833 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐴, 𝐵} ∈ 𝐸 ↔ ((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺))) |
63 | | eqcom 2745 |
. . . . . . . . . . . . . . 15
⊢
(((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶} ↔ {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
64 | 63 | biimpi 215 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶} → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
65 | 64 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
66 | 65 | 3ad2ant3 1134 |
. . . . . . . . . . . 12
⊢ ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
67 | 66 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → {𝐵, 𝐶} = ((iEdg‘𝐺)‘(𝑓‘1))) |
68 | 67, 61 | eleq12d 2833 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐵, 𝐶} ∈ 𝐸 ↔ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺))) |
69 | 62, 68 | anbi12d 631 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ↔ (((iEdg‘𝐺)‘(𝑓‘0)) ∈ ran (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘(𝑓‘1)) ∈ ran (iEdg‘𝐺)))) |
70 | 52, 69 | mpbird 256 |
. . . . . . . 8
⊢ ((𝐺 ∈ UMGraph ∧ (𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶}))) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) |
71 | 70 | ex 413 |
. . . . . . 7
⊢ (𝐺 ∈ UMGraph → ((𝑓:(0..^2)⟶dom
(iEdg‘𝐺) ∧
〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
72 | 71 | adantr 481 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ 〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {𝐴, 𝐵} ∧ ((iEdg‘𝐺)‘(𝑓‘1)) = {𝐵, 𝐶})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
73 | 25, 72 | sylbid 239 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓:(0..^2)⟶dom (iEdg‘𝐺) ∧ 〈“𝐴𝐵𝐶”〉:(0...2)⟶𝑉 ∧ (((iEdg‘𝐺)‘(𝑓‘0)) = {(〈“𝐴𝐵𝐶”〉‘0), (〈“𝐴𝐵𝐶”〉‘1)} ∧
((iEdg‘𝐺)‘(𝑓‘1)) = {(〈“𝐴𝐵𝐶”〉‘1), (〈“𝐴𝐵𝐶”〉‘2)})) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
74 | 12, 73 | sylbid 239 |
. . . 4
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
75 | 74 | exlimdv 1936 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
76 | 58 | umgr2wlk 28314 |
. . . . . . 7
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
77 | | wlklenvp1 27985 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1)) |
78 | | oveq1 7282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = (2 + 1)) |
79 | | 2p1e3 12115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 + 1) =
3 |
80 | 78, 79 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑓) =
2 → ((♯‘𝑓)
+ 1) = 3) |
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑓)
= 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((♯‘𝑓) + 1) = 3) |
82 | 77, 81 | sylan9eq 2798 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (♯‘𝑝) = 3) |
83 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 = (𝑝‘0) ↔ (𝑝‘0) = 𝐴) |
84 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 = (𝑝‘1) ↔ (𝑝‘1) = 𝐵) |
85 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐶 = (𝑝‘2) ↔ (𝑝‘2) = 𝐶) |
86 | 83, 84, 85 | 3anbi123i 1154 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
87 | 86 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑓)
= 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
89 | 88 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶)) |
90 | 82, 89 | jca 512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝐴 ∧ (𝑝‘1) = 𝐵 ∧ (𝑝‘2) = 𝐶))) |
91 | 6 | wlkpwrd 27984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉) |
92 | 80 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑓) =
2 → ((♯‘𝑝)
= ((♯‘𝑓) + 1)
↔ (♯‘𝑝) =
3)) |
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = ((♯‘𝑓) + 1) ↔
(♯‘𝑝) =
3)) |
94 | | simp1 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉) |
95 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝑝) =
3 → (0..^(♯‘𝑝)) = (0..^3)) |
96 | | fzo0to3tp 13473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (0..^3) =
{0, 1, 2} |
97 | 95, 96 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝑝) =
3 → (0..^(♯‘𝑝)) = {0, 1, 2}) |
98 | 31 | tpid1 4704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 0 ∈
{0, 1, 2} |
99 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → (0 ∈
(0..^(♯‘𝑝))
↔ 0 ∈ {0, 1, 2})) |
100 | 98, 99 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → 0 ∈
(0..^(♯‘𝑝))) |
101 | | wrdsymbcl 14230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 0 ∈ (0..^(♯‘𝑝))) → (𝑝‘0) ∈ 𝑉) |
102 | 100, 101 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘0) ∈ 𝑉) |
103 | 39 | tpid2 4706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 1 ∈
{0, 1, 2} |
104 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → (1 ∈
(0..^(♯‘𝑝))
↔ 1 ∈ {0, 1, 2})) |
105 | 103, 104 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → 1 ∈
(0..^(♯‘𝑝))) |
106 | | wrdsymbcl 14230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 1 ∈ (0..^(♯‘𝑝))) → (𝑝‘1) ∈ 𝑉) |
107 | 105, 106 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘1) ∈ 𝑉) |
108 | | 2ex 12050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 2 ∈
V |
109 | 108 | tpid3 4709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 2 ∈
{0, 1, 2} |
110 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → (2 ∈
(0..^(♯‘𝑝))
↔ 2 ∈ {0, 1, 2})) |
111 | 109, 110 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((0..^(♯‘𝑝)) = {0, 1, 2} → 2 ∈
(0..^(♯‘𝑝))) |
112 | | wrdsymbcl 14230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑝 ∈ Word 𝑉 ∧ 2 ∈ (0..^(♯‘𝑝))) → (𝑝‘2) ∈ 𝑉) |
113 | 111, 112 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → (𝑝‘2) ∈ 𝑉) |
114 | 102, 107,
113 | 3jca 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑝 ∈ Word 𝑉 ∧ (0..^(♯‘𝑝)) = {0, 1, 2}) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
115 | 97, 114 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
116 | 115 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉)) |
117 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐴 = (𝑝‘0) → (𝐴 ∈ 𝑉 ↔ (𝑝‘0) ∈ 𝑉)) |
118 | 117 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐴 ∈ 𝑉 ↔ (𝑝‘0) ∈ 𝑉)) |
119 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵 = (𝑝‘1) → (𝐵 ∈ 𝑉 ↔ (𝑝‘1) ∈ 𝑉)) |
120 | 119 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐵 ∈ 𝑉 ↔ (𝑝‘1) ∈ 𝑉)) |
121 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐶 = (𝑝‘2) → (𝐶 ∈ 𝑉 ↔ (𝑝‘2) ∈ 𝑉)) |
122 | 121 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝐶 ∈ 𝑉 ↔ (𝑝‘2) ∈ 𝑉)) |
123 | 118, 120,
122 | 3anbi123d 1435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))) |
124 | 123 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ↔ ((𝑝‘0) ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ (𝑝‘2) ∈ 𝑉))) |
125 | 116, 124 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
126 | 94, 125 | jca 512 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = 3 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
127 | 126 | 3exp 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 ∈ Word 𝑉 → ((♯‘𝑝) = 3 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = 3 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
129 | 93, 128 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑓) = 2) → ((♯‘𝑝) = ((♯‘𝑓) + 1) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
130 | 129 | impancom 452 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = ((♯‘𝑓) + 1)) → ((♯‘𝑓) = 2 → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))))) |
131 | 130 | impd 411 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ Word 𝑉 ∧ (♯‘𝑝) = ((♯‘𝑓) + 1)) → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
132 | 91, 77, 131 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)))) |
133 | 132 | imp 407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑝 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
134 | | eqwrds3 14676 |
. . . . . . . . . . . . . . . . . . 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 256 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑝 = 〈“𝐴𝐵𝐶”〉) |
137 | 136 | breq2d 5086 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)𝑝 ↔ 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
138 | 137 | biimpd 228 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)𝑝 → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
139 | 138 | ex 413 |
. . . . . . . . . . . . . 14
⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝 → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉))) |
140 | 139 | pm2.43a 54 |
. . . . . . . . . . . . 13
⊢ (𝑓(Walks‘𝐺)𝑝 → (((♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉)) |
141 | 140 | 3impib 1115 |
. . . . . . . . . . . 12
⊢ ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉) |
142 | 141 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉) |
143 | | simpr2 1194 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (♯‘𝑓) = 2) |
144 | 142, 143 | jca 512 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2)) |
145 | 144 | ex 413 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
146 | 145 | exlimdv 1936 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
147 | 146 | eximdv 1920 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
148 | 76, 147 | syl5com 31 |
. . . . . 6
⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
149 | 148 | 3expib 1121 |
. . . . 5
⊢ (𝐺 ∈ UMGraph → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2)))) |
150 | 149 | com23 86 |
. . . 4
⊢ (𝐺 ∈ UMGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2)))) |
151 | 150 | imp 407 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) |
152 | 75, 151 | impbid 211 |
. 2
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |
153 | 8, 152 | bitrd 278 |
1
⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) |