Step | Hyp | Ref
| Expression |
1 | | usgrav 25867 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
2 | | el2pthsot 26408 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑦 ∈ 𝑉 ∃𝑥 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑝 = 〈𝑦, 𝑥, 𝑧〉 ∧ ∃𝑓∃𝑞(𝑓(𝑉 SPaths 𝐸)𝑞 ∧ (#‘𝑓) = 2 ∧ (𝑦 = (𝑞‘0) ∧ 𝑥 = (𝑞‘1) ∧ 𝑧 = (𝑞‘2)))))) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑦 ∈ 𝑉 ∃𝑥 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑝 = 〈𝑦, 𝑥, 𝑧〉 ∧ ∃𝑓∃𝑞(𝑓(𝑉 SPaths 𝐸)𝑞 ∧ (#‘𝑓) = 2 ∧ (𝑦 = (𝑞‘0) ∧ 𝑥 = (𝑞‘1) ∧ 𝑧 = (𝑞‘2)))))) |
4 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
5 | 4 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
6 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
7 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
8 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉) |
9 | 5, 7, 8 | 3jca 1235 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) |
10 | | ot2ndg 7074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (2nd
‘(1st ‘〈𝑦, 𝑥, 𝑧〉)) = 𝑥) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → (2nd
‘(1st ‘〈𝑦, 𝑥, 𝑧〉)) = 𝑥) |
12 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → 〈𝑦, 𝑥, 𝑧〉 = 〈𝑦, 𝑥, 𝑧〉) |
13 | | otel3xp 5077 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑦, 𝑥, 𝑧〉 = 〈𝑦, 𝑥, 𝑧〉 ∧ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 〈𝑦, 𝑥, 𝑧〉 ∈ ((𝑉 × 𝑉) × 𝑉)) |
14 | 12, 9, 13 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → 〈𝑦, 𝑥, 𝑧〉 ∈ ((𝑉 × 𝑉) × 𝑉)) |
15 | 11, 14 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → ((2nd
‘(1st ‘〈𝑦, 𝑥, 𝑧〉)) = 𝑥 ∧ 〈𝑦, 𝑥, 𝑧〉 ∈ ((𝑉 × 𝑉) × 𝑉))) |
16 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 〈𝑦, 𝑥, 𝑧〉 → (1st ‘𝑝) = (1st
‘〈𝑦, 𝑥, 𝑧〉)) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 〈𝑦, 𝑥, 𝑧〉 → (2nd
‘(1st ‘𝑝)) = (2nd ‘(1st
‘〈𝑦, 𝑥, 𝑧〉))) |
18 | 17 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 〈𝑦, 𝑥, 𝑧〉 → ((2nd
‘(1st ‘𝑝)) = 𝑥 ↔ (2nd
‘(1st ‘〈𝑦, 𝑥, 𝑧〉)) = 𝑥)) |
19 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 〈𝑦, 𝑥, 𝑧〉 → (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ↔ 〈𝑦, 𝑥, 𝑧〉 ∈ ((𝑉 × 𝑉) × 𝑉))) |
20 | 18, 19 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 〈𝑦, 𝑥, 𝑧〉 → (((2nd
‘(1st ‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)) ↔ ((2nd
‘(1st ‘〈𝑦, 𝑥, 𝑧〉)) = 𝑥 ∧ 〈𝑦, 𝑥, 𝑧〉 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
21 | 15, 20 | syl5ibr 235 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 〈𝑦, 𝑥, 𝑧〉 → ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → ((2nd
‘(1st ‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 = 〈𝑦, 𝑥, 𝑧〉 ∧ ∃𝑓∃𝑞(𝑓(𝑉 SPaths 𝐸)𝑞 ∧ (#‘𝑓) = 2 ∧ (𝑦 = (𝑞‘0) ∧ 𝑥 = (𝑞‘1) ∧ 𝑧 = (𝑞‘2)))) → ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → ((2nd
‘(1st ‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
23 | 22 | com12 32 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) ∧ 𝑧 ∈ 𝑉) → ((𝑝 = 〈𝑦, 𝑥, 𝑧〉 ∧ ∃𝑓∃𝑞(𝑓(𝑉 SPaths 𝐸)𝑞 ∧ (#‘𝑓) = 2 ∧ (𝑦 = (𝑞‘0) ∧ 𝑥 = (𝑞‘1) ∧ 𝑧 = (𝑞‘2)))) → ((2nd
‘(1st ‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
24 | 23 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → (∃𝑧 ∈ 𝑉 (𝑝 = 〈𝑦, 𝑥, 𝑧〉 ∧ ∃𝑓∃𝑞(𝑓(𝑉 SPaths 𝐸)𝑞 ∧ (#‘𝑓) = 2 ∧ (𝑦 = (𝑞‘0) ∧ 𝑥 = (𝑞‘1) ∧ 𝑧 = (𝑞‘2)))) → ((2nd
‘(1st ‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
25 | 24 | reximdva 3000 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) → (∃𝑥 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑝 = 〈𝑦, 𝑥, 𝑧〉 ∧ ∃𝑓∃𝑞(𝑓(𝑉 SPaths 𝐸)𝑞 ∧ (#‘𝑓) = 2 ∧ (𝑦 = (𝑞‘0) ∧ 𝑥 = (𝑞‘1) ∧ 𝑧 = (𝑞‘2)))) → ∃𝑥 ∈ 𝑉 ((2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
26 | | r19.41v 3070 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝑉 ((2nd
‘(1st ‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)) ↔ (∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉))) |
27 | 25, 26 | syl6ib 240 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑦 ∈ 𝑉) → (∃𝑥 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑝 = 〈𝑦, 𝑥, 𝑧〉 ∧ ∃𝑓∃𝑞(𝑓(𝑉 SPaths 𝐸)𝑞 ∧ (#‘𝑓) = 2 ∧ (𝑦 = (𝑞‘0) ∧ 𝑥 = (𝑞‘1) ∧ 𝑧 = (𝑞‘2)))) → (∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
28 | 27 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (∃𝑦 ∈ 𝑉 ∃𝑥 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑝 = 〈𝑦, 𝑥, 𝑧〉 ∧ ∃𝑓∃𝑞(𝑓(𝑉 SPaths 𝐸)𝑞 ∧ (#‘𝑓) = 2 ∧ (𝑦 = (𝑞‘0) ∧ 𝑥 = (𝑞‘1) ∧ 𝑧 = (𝑞‘2)))) → (∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
29 | 3, 28 | sylbid 229 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → (𝑝 ∈ (𝑉 2SPathsOt 𝐸) → (∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
30 | 29 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑝 ∈ (𝑉 2SPathsOt 𝐸) → (∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)))) |
31 | 30 | pm4.71rd 665 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ↔ ((∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)))) |
32 | | anass 679 |
. . . . . . . . 9
⊢ (((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥) ↔ (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥))) |
33 | 32 | bicomi 213 |
. . . . . . . 8
⊢ ((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥)) ↔ ((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥)) |
34 | 33 | rexbii 3023 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝑉 (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥)) ↔ ∃𝑥 ∈ 𝑉 ((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥)) |
35 | | ancom 465 |
. . . . . . . 8
⊢ (((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)) ∧ ∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥) ↔ (∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)))) |
36 | | r19.42v 3073 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑉 ((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥) ↔ ((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)) ∧ ∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥)) |
37 | | anass 679 |
. . . . . . . 8
⊢
(((∃𝑥 ∈
𝑉 (2nd
‘(1st ‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)) ↔ (∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)))) |
38 | 35, 36, 37 | 3bitr4i 291 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝑉 ((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸)) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥) ↔ ((∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸))) |
39 | 34, 38 | bitri 263 |
. . . . . 6
⊢
(∃𝑥 ∈
𝑉 (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥)) ↔ ((∃𝑥 ∈ 𝑉 (2nd ‘(1st
‘𝑝)) = 𝑥 ∧ 𝑝 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑝 ∈ (𝑉 2SPathsOt 𝐸))) |
40 | 31, 39 | syl6bbr 277 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑥 ∈ 𝑉 (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥)))) |
41 | | simpr 476 |
. . . . . . . . 9
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
42 | | 3xpexg 6859 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ V) |
43 | | rabexg 4739 |
. . . . . . . . . . 11
⊢ (((𝑉 × 𝑉) × 𝑉) ∈ V → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} ∈ V) |
44 | 42, 43 | syl 17 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} ∈ V) |
45 | 44 | ad3antlr 763 |
. . . . . . . . 9
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑥 ∈ 𝑉) → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} ∈ V) |
46 | | eqeq2 2621 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → ((2nd
‘(1st ‘𝑡)) = 𝑎 ↔ (2nd
‘(1st ‘𝑡)) = 𝑥)) |
47 | 46 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎) ↔ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥))) |
48 | 47 | rabbidv 3164 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎)} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)}) |
49 | | usgreghash2spot.m |
. . . . . . . . . 10
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎)}) |
50 | 48, 49 | fvmptg 6189 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑉 ∧ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} ∈ V) → (𝑀‘𝑥) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)}) |
51 | 41, 45, 50 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑥 ∈ 𝑉) → (𝑀‘𝑥) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)}) |
52 | 51 | eleq2d 2673 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑥 ∈ 𝑉) → (𝑝 ∈ (𝑀‘𝑥) ↔ 𝑝 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)})) |
53 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑡 = 𝑝 → (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ↔ 𝑝 ∈ (𝑉 2SPathsOt 𝐸))) |
54 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑝 → (1st ‘𝑡) = (1st ‘𝑝)) |
55 | 54 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑝 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑝))) |
56 | 55 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑡 = 𝑝 → ((2nd
‘(1st ‘𝑡)) = 𝑥 ↔ (2nd
‘(1st ‘𝑝)) = 𝑥)) |
57 | 53, 56 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑡 = 𝑝 → ((𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥) ↔ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥))) |
58 | 57 | elrab 3331 |
. . . . . . 7
⊢ (𝑝 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑥)} ↔ (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥))) |
59 | 52, 58 | syl6rbb 276 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑥 ∈ 𝑉) → ((𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥)) ↔ 𝑝 ∈ (𝑀‘𝑥))) |
60 | 59 | rexbidva 3031 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (∃𝑥 ∈ 𝑉 (𝑝 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑝)) = 𝑥)) ↔ ∃𝑥 ∈ 𝑉 𝑝 ∈ (𝑀‘𝑥))) |
61 | 40, 60 | bitrd 267 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑥 ∈ 𝑉 𝑝 ∈ (𝑀‘𝑥))) |
62 | | eliun 4460 |
. . . 4
⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝑉 (𝑀‘𝑥) ↔ ∃𝑥 ∈ 𝑉 𝑝 ∈ (𝑀‘𝑥)) |
63 | 61, 62 | syl6bbr 277 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑝 ∈ (𝑉 2SPathsOt 𝐸) ↔ 𝑝 ∈ ∪
𝑥 ∈ 𝑉 (𝑀‘𝑥))) |
64 | 63 | eqrdv 2608 |
. 2
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑉 2SPathsOt 𝐸) = ∪
𝑥 ∈ 𝑉 (𝑀‘𝑥)) |
65 | 64 | ex 449 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 2SPathsOt 𝐸) = ∪
𝑥 ∈ 𝑉 (𝑀‘𝑥))) |