| Step | Hyp | Ref
| Expression |
| 1 | | frgrhash2wsp.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | fusgreg2wsp.m |
. . . . . 6
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}) |
| 3 | 1, 2 | fusgreg2wsplem 30352 |
. . . . 5
⊢ (𝑁 ∈ 𝑉 → (𝑧 ∈ (𝑀‘𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁))) |
| 4 | 3 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑀‘𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁))) |
| 5 | 1 | wspthsnwspthsnon 29936 |
. . . . . . 7
⊢ (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)) |
| 6 | | fusgrusgr 29339 |
. . . . . . . . . 10
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈
USGraph) |
| 7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝐺 ∈ USGraph) |
| 8 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 9 | 1, 8 | usgr2wspthon 29985 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) |
| 10 | 7, 9 | sylan 580 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) |
| 11 | 10 | 2rexbidva 3220 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) |
| 12 | 5, 11 | bitrid 283 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) |
| 13 | 12 | anbi1d 631 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁))) |
| 14 | | 19.41vv 1950 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁)) |
| 15 | | velsn 4642 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ {〈“𝑥𝑁𝑦”〉} ↔ 𝑧 = 〈“𝑥𝑁𝑦”〉) |
| 16 | 15 | bicomi 224 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈“𝑥𝑁𝑦”〉 ↔ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉}) |
| 17 | 16 | anbi2i 623 |
. . . . . . . . . 10
⊢ ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉})) |
| 18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉}))) |
| 19 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) → 𝑁 ∈ 𝑉) |
| 20 | | anass 468 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ (𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) |
| 21 | | ancom 460 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ (𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ ((𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = 〈“𝑥𝑚𝑦”〉)) |
| 22 | | an12 645 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥 ≠ 𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) |
| 23 | | nesym 2997 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑦 = 𝑥) |
| 24 | | prcom 4732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑚, 𝑦} = {𝑦, 𝑚} |
| 25 | 24 | eleq1i 2832 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑚, 𝑦} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑚} ∈ (Edg‘𝐺)) |
| 26 | 23, 25 | anbi12ci 629 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ≠ 𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) ↔ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) |
| 27 | 26 | anbi2i 623 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥 ≠ 𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))) |
| 28 | 22, 27 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))) |
| 29 | 28 | anbi1i 624 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = 〈“𝑥𝑚𝑦”〉) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑚𝑦”〉)) |
| 30 | 20, 21, 29 | 3bitri 297 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑚𝑦”〉)) |
| 31 | | preq2 4734 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁}) |
| 32 | 31 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺))) |
| 33 | | preq2 4734 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 𝑁 → {𝑦, 𝑚} = {𝑦, 𝑁}) |
| 34 | 33 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑁 → ({𝑦, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺))) |
| 35 | 34 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑁 → (({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))) |
| 36 | 32, 35 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))) |
| 37 | | s3eq2 14909 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑁 → 〈“𝑥𝑚𝑦”〉 = 〈“𝑥𝑁𝑦”〉) |
| 38 | 37 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑁 → (𝑧 = 〈“𝑥𝑚𝑦”〉 ↔ 𝑧 = 〈“𝑥𝑁𝑦”〉)) |
| 39 | 36, 38 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑁 → ((({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑚𝑦”〉) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉))) |
| 40 | 30, 39 | bitrid 283 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑁 → (((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉))) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ 𝑚 = 𝑁) → (((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉))) |
| 42 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 〈“𝑥𝑚𝑦”〉 → (𝑧‘1) = (〈“𝑥𝑚𝑦”〉‘1)) |
| 43 | | s3fv1 14931 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ V →
(〈“𝑥𝑚𝑦”〉‘1) = 𝑚) |
| 44 | 43 | elv 3485 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈“𝑥𝑚𝑦”〉‘1) = 𝑚 |
| 45 | 42, 44 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 〈“𝑥𝑚𝑦”〉 → (𝑧‘1) = 𝑚) |
| 46 | 45 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈“𝑥𝑚𝑦”〉 → ((𝑧‘1) = 𝑁 ↔ 𝑚 = 𝑁)) |
| 47 | 46 | biimpd 229 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈“𝑥𝑚𝑦”〉 → ((𝑧‘1) = 𝑁 → 𝑚 = 𝑁)) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) → ((𝑧‘1) = 𝑁 → 𝑚 = 𝑁)) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝑧‘1) = 𝑁 → 𝑚 = 𝑁)) |
| 50 | 49 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ((𝑧‘1) = 𝑁 → (((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁)) |
| 51 | 50 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) → (((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁)) |
| 52 | 51 | imp 406 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → 𝑚 = 𝑁) |
| 53 | 19, 41, 52 | rspcebdv 3616 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) → (∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉))) |
| 54 | 53 | pm5.32da 579 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉)))) |
| 55 | | an32 646 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) |
| 56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))) |
| 57 | | usgrumgr 29198 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UMGraph) |
| 58 | 1, 8 | umgrpredgv 29157 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
| 59 | 58 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → 𝑥 ∈ 𝑉) |
| 60 | 59 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 ∈ UMGraph → ({𝑥, 𝑁} ∈ (Edg‘𝐺) → 𝑥 ∈ 𝑉)) |
| 61 | 1, 8 | umgrpredgv 29157 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝑦 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) |
| 62 | 61 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → 𝑦 ∈ 𝑉) |
| 63 | 62 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑦, 𝑁} ∈ (Edg‘𝐺) → (𝐺 ∈ UMGraph → 𝑦 ∈ 𝑉)) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → (𝐺 ∈ UMGraph → 𝑦 ∈ 𝑉)) |
| 65 | 64 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 ∈ UMGraph → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ 𝑉)) |
| 66 | 60, 65 | anim12d 609 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ UMGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
| 67 | 6, 57, 66 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ FinUSGraph →
(({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
| 69 | 68 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
| 71 | 70 | impcom 407 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉)) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) |
| 72 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈“𝑥𝑁𝑦”〉 → (𝑧‘1) = (〈“𝑥𝑁𝑦”〉‘1)) |
| 73 | 72 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉) → (𝑧‘1) = (〈“𝑥𝑁𝑦”〉‘1)) |
| 74 | | s3fv1 14931 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ 𝑉 → (〈“𝑥𝑁𝑦”〉‘1) = 𝑁) |
| 75 | 74 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (〈“𝑥𝑁𝑦”〉‘1) = 𝑁) |
| 76 | 73, 75 | sylan9eqr 2799 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉)) → (𝑧‘1) = 𝑁) |
| 77 | 71, 76 | jca 511 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉)) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) |
| 78 | 77 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁))) |
| 79 | 78 | pm4.71rd 562 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉) ↔ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉)))) |
| 80 | 54, 56, 79 | 3bitr4d 311 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = 〈“𝑥𝑁𝑦”〉))) |
| 81 | 8 | nbusgreledg 29370 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺))) |
| 82 | 6, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FinUSGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺))) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺))) |
| 84 | | eldif 3961 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥})) |
| 85 | 8 | nbusgreledg 29370 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺))) |
| 86 | 6, 85 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ FinUSGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺))) |
| 87 | 86 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺))) |
| 88 | | velsn 4642 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥) |
| 89 | 88 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)) |
| 90 | 89 | notbid 318 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥)) |
| 91 | 87, 90 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))) |
| 92 | 84, 91 | bitrid 283 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))) |
| 93 | 83, 92 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))) |
| 94 | 93 | anbi1d 631 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉}) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉}))) |
| 95 | 18, 80, 94 | 3bitr4d 311 |
. . . . . . . 8
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉}))) |
| 96 | 95 | 2exbidv 1924 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥∃𝑦(((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥∃𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉}))) |
| 97 | 14, 96 | bitr3id 285 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥∃𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉}))) |
| 98 | | r2ex 3196 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) |
| 99 | 98 | anbi1i 624 |
. . . . . 6
⊢
((∃𝑥 ∈
𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁)) |
| 100 | | r2ex 3196 |
. . . . . 6
⊢
(∃𝑥 ∈
(𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {〈“𝑥𝑁𝑦”〉} ↔ ∃𝑥∃𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉})) |
| 101 | 97, 99, 100 | 3bitr4g 314 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = 〈“𝑥𝑚𝑦”〉 ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {〈“𝑥𝑁𝑦”〉})) |
| 102 | | vex 3484 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
| 103 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑝 = 𝑧 → (𝑝 ∈ {〈“𝑥𝑁𝑦”〉} ↔ 𝑧 ∈ {〈“𝑥𝑁𝑦”〉})) |
| 104 | 103 | 2rexbidv 3222 |
. . . . . . . 8
⊢ (𝑝 = 𝑧 → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {〈“𝑥𝑁𝑦”〉} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {〈“𝑥𝑁𝑦”〉})) |
| 105 | 102, 104 | elab 3679 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {〈“𝑥𝑁𝑦”〉}} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {〈“𝑥𝑁𝑦”〉}) |
| 106 | 105 | bicomi 224 |
. . . . . 6
⊢
(∃𝑥 ∈
(𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {〈“𝑥𝑁𝑦”〉} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {〈“𝑥𝑁𝑦”〉}}) |
| 107 | 106 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {〈“𝑥𝑁𝑦”〉} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {〈“𝑥𝑁𝑦”〉}})) |
| 108 | 13, 101, 107 | 3bitrd 305 |
. . . 4
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {〈“𝑥𝑁𝑦”〉}})) |
| 109 | 4, 108 | bitrd 279 |
. . 3
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑀‘𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {〈“𝑥𝑁𝑦”〉}})) |
| 110 | 109 | eqrdv 2735 |
. 2
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {〈“𝑥𝑁𝑦”〉}}) |
| 111 | | dfiunv2 5035 |
. 2
⊢ ∪ 𝑥 ∈ (𝐺 NeighbVtx 𝑁)∪ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){〈“𝑥𝑁𝑦”〉} = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {〈“𝑥𝑁𝑦”〉}} |
| 112 | 110, 111 | eqtr4di 2795 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = ∪
𝑥 ∈ (𝐺 NeighbVtx 𝑁)∪ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){〈“𝑥𝑁𝑦”〉}) |