Step | Hyp | Ref
| Expression |
1 | | iswspthn 41047 |
. . . . . . 7
⊢ (𝑝 ∈ (2 WSPathsN 𝐺) ↔ (𝑝 ∈ (2 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑝)) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝐺 ∈ FinUSGraph → (𝑝 ∈ (2 WSPathsN 𝐺) ↔ (𝑝 ∈ (2 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑝))) |
3 | | frgrhash2wsp.v |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
4 | 3 | elwwlks2s3 41169 |
. . . . . . . 8
⊢ (𝑝 ∈ (2 WWalkSN 𝐺) → ∃𝑎 ∈ 𝑉 ∃𝑥 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑝 = 〈“𝑎𝑥𝑐”〉) |
5 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈“𝑎𝑥𝑐”〉 → (𝑝‘1) = (〈“𝑎𝑥𝑐”〉‘1)) |
6 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
7 | | s3fv1 13487 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V →
(〈“𝑎𝑥𝑐”〉‘1) = 𝑥) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(〈“𝑎𝑥𝑐”〉‘1) = 𝑥 |
9 | 5, 8 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈“𝑎𝑥𝑐”〉 → (𝑝‘1) = 𝑥) |
10 | 9 | rexlimivw 3011 |
. . . . . . . . . 10
⊢
(∃𝑐 ∈
𝑉 𝑝 = 〈“𝑎𝑥𝑐”〉 → (𝑝‘1) = 𝑥) |
11 | 10 | reximi 2994 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝑉 ∃𝑐 ∈ 𝑉 𝑝 = 〈“𝑎𝑥𝑐”〉 → ∃𝑥 ∈ 𝑉 (𝑝‘1) = 𝑥) |
12 | 11 | rexlimivw 3011 |
. . . . . . . 8
⊢
(∃𝑎 ∈
𝑉 ∃𝑥 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑝 = 〈“𝑎𝑥𝑐”〉 → ∃𝑥 ∈ 𝑉 (𝑝‘1) = 𝑥) |
13 | 4, 12 | syl 17 |
. . . . . . 7
⊢ (𝑝 ∈ (2 WWalkSN 𝐺) → ∃𝑥 ∈ 𝑉 (𝑝‘1) = 𝑥) |
14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝑝 ∈ (2 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑝) → ∃𝑥 ∈ 𝑉 (𝑝‘1) = 𝑥) |
15 | 2, 14 | syl6bi 242 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph → (𝑝 ∈ (2 WSPathsN 𝐺) → ∃𝑥 ∈ 𝑉 (𝑝‘1) = 𝑥)) |
16 | 15 | pm4.71rd 665 |
. . . 4
⊢ (𝐺 ∈ FinUSGraph → (𝑝 ∈ (2 WSPathsN 𝐺) ↔ (∃𝑥 ∈ 𝑉 (𝑝‘1) = 𝑥 ∧ 𝑝 ∈ (2 WSPathsN 𝐺)))) |
17 | | ancom 465 |
. . . . . . 7
⊢ ((𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑥) ↔ ((𝑝‘1) = 𝑥 ∧ 𝑝 ∈ (2 WSPathsN 𝐺))) |
18 | 17 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑥 ∈
𝑉 (𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑥) ↔ ∃𝑥 ∈ 𝑉 ((𝑝‘1) = 𝑥 ∧ 𝑝 ∈ (2 WSPathsN 𝐺))) |
19 | | r19.41v 3070 |
. . . . . 6
⊢
(∃𝑥 ∈
𝑉 ((𝑝‘1) = 𝑥 ∧ 𝑝 ∈ (2 WSPathsN 𝐺)) ↔ (∃𝑥 ∈ 𝑉 (𝑝‘1) = 𝑥 ∧ 𝑝 ∈ (2 WSPathsN 𝐺))) |
20 | 18, 19 | bitr2i 264 |
. . . . 5
⊢
((∃𝑥 ∈
𝑉 (𝑝‘1) = 𝑥 ∧ 𝑝 ∈ (2 WSPathsN 𝐺)) ↔ ∃𝑥 ∈ 𝑉 (𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑥)) |
21 | 20 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ FinUSGraph →
((∃𝑥 ∈ 𝑉 (𝑝‘1) = 𝑥 ∧ 𝑝 ∈ (2 WSPathsN 𝐺)) ↔ ∃𝑥 ∈ 𝑉 (𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑥))) |
22 | | simpr 476 |
. . . . . . . 8
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
23 | | ovex 6577 |
. . . . . . . . 9
⊢ (2
WSPathsN 𝐺) ∈
V |
24 | 23 | rabex 4740 |
. . . . . . . 8
⊢ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ∈ V |
25 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑥)) |
26 | 25 | rabbidv 3164 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥}) |
27 | | fusgreg2wsp.m |
. . . . . . . . 9
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}) |
28 | 26, 27 | fvmptg 6189 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ∈ V) → (𝑀‘𝑥) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥}) |
29 | 22, 24, 28 | sylancl 693 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑥 ∈ 𝑉) → (𝑀‘𝑥) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥}) |
30 | 29 | eleq2d 2673 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑥 ∈ 𝑉) → (𝑝 ∈ (𝑀‘𝑥) ↔ 𝑝 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥})) |
31 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑤 = 𝑝 → (𝑤‘1) = (𝑝‘1)) |
32 | 31 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑤 = 𝑝 → ((𝑤‘1) = 𝑥 ↔ (𝑝‘1) = 𝑥)) |
33 | 32 | elrab 3331 |
. . . . . 6
⊢ (𝑝 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑥} ↔ (𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑥)) |
34 | 30, 33 | syl6rbb 276 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑥 ∈ 𝑉) → ((𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑥) ↔ 𝑝 ∈ (𝑀‘𝑥))) |
35 | 34 | rexbidva 3031 |
. . . 4
⊢ (𝐺 ∈ FinUSGraph →
(∃𝑥 ∈ 𝑉 (𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑥) ↔ ∃𝑥 ∈ 𝑉 𝑝 ∈ (𝑀‘𝑥))) |
36 | 16, 21, 35 | 3bitrd 293 |
. . 3
⊢ (𝐺 ∈ FinUSGraph → (𝑝 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 𝑝 ∈ (𝑀‘𝑥))) |
37 | | eliun 4460 |
. . 3
⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝑉 (𝑀‘𝑥) ↔ ∃𝑥 ∈ 𝑉 𝑝 ∈ (𝑀‘𝑥)) |
38 | 36, 37 | syl6bbr 277 |
. 2
⊢ (𝐺 ∈ FinUSGraph → (𝑝 ∈ (2 WSPathsN 𝐺) ↔ 𝑝 ∈ ∪
𝑥 ∈ 𝑉 (𝑀‘𝑥))) |
39 | 38 | eqrdv 2608 |
1
⊢ (𝐺 ∈ FinUSGraph → (2
WSPathsN 𝐺) = ∪ 𝑥 ∈ 𝑉 (𝑀‘𝑥)) |