Step | Hyp | Ref
| Expression |
1 | | 2wlkonot3v 26402 |
. . . 4
⊢ (𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉))) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉))) |
3 | | el2wlkonot 26396 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ∃𝑐 ∈ 𝑉 (𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))))) |
4 | | pm3.22 464 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
5 | 4 | anim2i 591 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
6 | | el2wlkonot 26396 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) ↔ ∃𝑑 ∈ 𝑉 (𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2)))))) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) ↔ ∃𝑑 ∈ 𝑉 (𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2)))))) |
8 | 3, 7 | anbi12d 743 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ((𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) ↔ (∃𝑐 ∈ 𝑉 (𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) ∧ ∃𝑑 ∈ 𝑉 (𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2))))))) |
9 | 8 | 3adant3 1074 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) ↔ (∃𝑐 ∈ 𝑉 (𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) ∧ ∃𝑑 ∈ 𝑉 (𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2))))))) |
10 | 5 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
11 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
12 | 11 | ad2antrr 758 |
. . . . . . . . . . 11
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
13 | | el2wlkonotot 26400 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2))))) |
14 | 13 | bicomd 212 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2))) ↔ 〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴))) |
15 | 12, 14 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2))) ↔ 〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴))) |
16 | | 3simpa 1051 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
17 | 16 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
18 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
19 | | el2wlkonotot 26400 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2))))) |
20 | 19 | bicomd 212 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2))) ↔ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
21 | 18, 20 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2))) ↔ 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵))) |
22 | | frg2woteqm 26586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → 𝑑 = 𝑐)) |
23 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 = 〈𝐴, 𝑐, 𝐵〉 → (1st ‘𝑃) = (1st
‘〈𝐴, 𝑐, 𝐵〉)) |
24 | 23 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 = 〈𝐴, 𝑐, 𝐵〉 → (1st
‘(1st ‘𝑃)) = (1st ‘(1st
‘〈𝐴, 𝑐, 𝐵〉))) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (1st
‘(1st ‘𝑃)) = (1st ‘(1st
‘〈𝐴, 𝑐, 𝐵〉))) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (1st
‘(1st ‘𝑃)) = (1st ‘(1st
‘〈𝐴, 𝑐, 𝐵〉))) |
27 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑐 ∈ V |
28 | | ot1stg 7073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑐 ∈ V ∧ 𝐵 ∈ 𝑉) → (1st
‘(1st ‘〈𝐴, 𝑐, 𝐵〉)) = 𝐴) |
29 | 27, 28 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (1st
‘(1st ‘〈𝐴, 𝑐, 𝐵〉)) = 𝐴) |
30 | 29 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (1st
‘(1st ‘〈𝐴, 𝑐, 𝐵〉)) = 𝐴) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (1st
‘(1st ‘〈𝐴, 𝑐, 𝐵〉)) = 𝐴) |
32 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑄 = 〈𝐵, 𝑑, 𝐴〉 → (2nd ‘𝑄) = (2nd
‘〈𝐵, 𝑑, 𝐴〉)) |
33 | 32 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (2nd ‘𝑄) = (2nd
‘〈𝐵, 𝑑, 𝐴〉)) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (2nd ‘𝑄) = (2nd
‘〈𝐵, 𝑑, 𝐴〉)) |
35 | | ot3rdg 7075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴 ∈ 𝑉 → (2nd ‘〈𝐵, 𝑑, 𝐴〉) = 𝐴) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (2nd ‘〈𝐵, 𝑑, 𝐴〉) = 𝐴) |
37 | 36 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (2nd
‘〈𝐵, 𝑑, 𝐴〉) = 𝐴) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (2nd
‘〈𝐵, 𝑑, 𝐴〉) = 𝐴) |
39 | 34, 38 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → 𝐴 = (2nd ‘𝑄)) |
40 | 26, 31, 39 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (1st
‘(1st ‘𝑃)) = (2nd ‘𝑄)) |
41 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃))) |
42 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑄 = 〈𝐵, 𝑑, 𝐴〉 → (1st ‘𝑄) = (1st
‘〈𝐵, 𝑑, 𝐴〉)) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑄 = 〈𝐵, 𝑑, 𝐴〉 → (1st
‘(1st ‘𝑄)) = (1st ‘(1st
‘〈𝐵, 𝑑, 𝐴〉))) |
44 | 43 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (1st
‘(1st ‘𝑄)) = (1st ‘(1st
‘〈𝐵, 𝑑, 𝐴〉))) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (1st
‘(1st ‘𝑄)) = (1st ‘(1st
‘〈𝐵, 𝑑, 𝐴〉))) |
46 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) |
47 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 𝑑 ∈ V |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝑑 ∈ V) |
49 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
50 | 46, 48, 49 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝑑 ∈ V ∧ 𝐴 ∈ 𝑉)) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (𝐵 ∈ 𝑉 ∧ 𝑑 ∈ V ∧ 𝐴 ∈ 𝑉)) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (𝐵 ∈ 𝑉 ∧ 𝑑 ∈ V ∧ 𝐴 ∈ 𝑉)) |
53 | | ot1stg 7073 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑑 ∈ V ∧ 𝐴 ∈ 𝑉) → (1st
‘(1st ‘〈𝐵, 𝑑, 𝐴〉)) = 𝐵) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (1st
‘(1st ‘〈𝐵, 𝑑, 𝐴〉)) = 𝐵) |
55 | | ot3rdg 7075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐵 ∈ 𝑉 → (2nd ‘〈𝐴, 𝑐, 𝐵〉) = 𝐵) |
56 | 55 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (2nd ‘〈𝐴, 𝑐, 𝐵〉) = 𝐵) |
57 | 56 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (2nd
‘〈𝐴, 𝑐, 𝐵〉) = 𝐵) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (2nd
‘〈𝐴, 𝑐, 𝐵〉) = 𝐵) |
59 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → 𝑃 = 〈𝐴, 𝑐, 𝐵〉) |
60 | 59 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → 𝑃 = 〈𝐴, 𝑐, 𝐵〉) |
61 | 60 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → 〈𝐴, 𝑐, 𝐵〉 = 𝑃) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (2nd
‘〈𝐴, 𝑐, 𝐵〉) = (2nd ‘𝑃)) |
63 | 58, 62 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → 𝐵 = (2nd ‘𝑃)) |
64 | 45, 54, 63 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → (1st
‘(1st ‘𝑄)) = (2nd ‘𝑃)) |
65 | 40, 41, 64 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑑 = 𝑐 ∧ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉)) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃))) |
66 | 65 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑐 → ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))) |
67 | 22, 66 | syl6 34 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃))))) |
68 | 67 | expd 451 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
69 | 68 | com14 94 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
70 | 69 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) → (𝑃 = 〈𝐴, 𝑐, 𝐵〉 → (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃))))))) |
71 | 70 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑄 = 〈𝐵, 𝑑, 𝐴〉 → (𝑃 = 〈𝐴, 𝑐, 𝐵〉 → (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))))) |
72 | 71 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) → (𝑄 = 〈𝐵, 𝑑, 𝐴〉 → (𝑃 = 〈𝐴, 𝑐, 𝐵〉 → (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))))) |
73 | 72 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → (𝑄 = 〈𝐵, 𝑑, 𝐴〉 → (𝑃 = 〈𝐴, 𝑐, 𝐵〉 → (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))))) |
74 | 73 | imp31 447 |
. . . . . . . . . . . . 13
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
75 | 21, 74 | sylbid 229 |
. . . . . . . . . . . 12
⊢
(((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) ∧ 𝑃 = 〈𝐴, 𝑐, 𝐵〉) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2))) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
76 | 75 | expimpd 627 |
. . . . . . . . . . 11
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) → ((𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
77 | 76 | com23 84 |
. . . . . . . . . 10
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) → (〈𝐵, 𝑑, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴) → ((𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
78 | 15, 77 | sylbid 229 |
. . . . . . . . 9
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) ∧ 𝑄 = 〈𝐵, 𝑑, 𝐴〉) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2))) → ((𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
79 | 78 | expimpd 627 |
. . . . . . . 8
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) ∧ 𝑑 ∈ 𝑉) → ((𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2)))) → ((𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
80 | 79 | rexlimdva 3013 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) → (∃𝑑 ∈ 𝑉 (𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2)))) → ((𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
81 | 80 | com23 84 |
. . . . . 6
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) ∧ 𝑐 ∈ 𝑉) → ((𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → (∃𝑑 ∈ 𝑉 (𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2)))) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
82 | 81 | rexlimdva 3013 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) → (∃𝑐 ∈ 𝑉 (𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) → (∃𝑑 ∈ 𝑉 (𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2)))) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))))) |
83 | 82 | impd 446 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((∃𝑐 ∈ 𝑉 (𝑃 = 〈𝐴, 𝑐, 𝐵〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑐 = (𝑝‘1) ∧ 𝐵 = (𝑝‘2)))) ∧ ∃𝑑 ∈ 𝑉 (𝑄 = 〈𝐵, 𝑑, 𝐴〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐵 = (𝑝‘0) ∧ 𝑑 = (𝑝‘1) ∧ 𝐴 = (𝑝‘2))))) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃))))) |
84 | 9, 83 | sylbid 229 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑃 ∈ ((𝑉 × 𝑉) × 𝑉)) → ((𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃))))) |
85 | 2, 84 | mpcom 37 |
. 2
⊢ ((𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))) |
86 | 85 | com12 32 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((1st
‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd
‘(1st ‘𝑃)) = (2nd ‘(1st
‘𝑃)) ∧
(1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))) |