Step | Hyp | Ref
| Expression |
1 | | 2pthfrgrarn2 26537 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑚 ∈ 𝑉 (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) |
2 | | frisusgra 26519 |
. . . . . . . . . 10
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
3 | | usgrav 25867 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
5 | 4 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
6 | 5 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
7 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
8 | 7 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
9 | | simpr 476 |
. . . . . . . . 9
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → 𝑚 ∈ 𝑉) |
10 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎)) |
11 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎) → 𝑏 ∈ 𝑉) |
12 | 10, 11 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → 𝑏 ∈ 𝑉) |
13 | 12 | ad2antlr 759 |
. . . . . . . . 9
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → 𝑏 ∈ 𝑉) |
14 | 8, 9, 13 | 3jca 1235 |
. . . . . . . 8
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → (𝑎 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (𝑎 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
16 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏) ∧ 𝑏 ≠ 𝑎) → 𝑎 ≠ 𝑚) |
17 | | necom 2835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ≠ 𝑎 ↔ 𝑎 ≠ 𝑏) |
18 | 17 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ≠ 𝑎 → 𝑎 ≠ 𝑏) |
19 | 18 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏) ∧ 𝑏 ≠ 𝑎) → 𝑎 ≠ 𝑏) |
20 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏) ∧ 𝑏 ≠ 𝑎) → 𝑚 ≠ 𝑏) |
21 | 16, 19, 20 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏) ∧ 𝑏 ≠ 𝑎) → (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏)) |
22 | 21 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏) → (𝑏 ≠ 𝑎 → (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏))) |
23 | 22 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → (𝑏 ≠ 𝑎 → (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏))) |
24 | 23 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑏 ≠ 𝑎 → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏))) |
25 | 24 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎) → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏))) |
26 | 10, 25 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏))) |
27 | 26 | ad2antlr 759 |
. . . . . . . 8
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏))) |
28 | 27 | imp 444 |
. . . . . . 7
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏)) |
29 | | usgraf1o 25887 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
30 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐸‘{𝑎, 𝑚}) = (◡𝐸‘{𝑚, 𝑏}) → (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = (𝐸‘(◡𝐸‘{𝑚, 𝑏}))) |
31 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
32 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → {𝑎, 𝑚} ∈ ran 𝐸) |
33 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝑎, 𝑚} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚}) |
34 | 31, 32, 33 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚}) |
35 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → {𝑚, 𝑏} ∈ ran 𝐸) |
36 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏}) |
37 | 31, 35, 36 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏}) |
38 | 34, 37 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → ((𝐸‘(◡𝐸‘{𝑎, 𝑚})) = (𝐸‘(◡𝐸‘{𝑚, 𝑏})) ↔ {𝑎, 𝑚} = {𝑚, 𝑏})) |
39 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑚, 𝑏} = {𝑏, 𝑚} |
40 | 39 | eqeq2i 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑎, 𝑚} = {𝑚, 𝑏} ↔ {𝑎, 𝑚} = {𝑏, 𝑚}) |
41 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑎 ∈ V |
42 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑏 ∈ V |
43 | 41, 42 | preqr1 4319 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑎, 𝑚} = {𝑏, 𝑚} → 𝑎 = 𝑏) |
44 | 40, 43 | sylbi 206 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑎, 𝑚} = {𝑚, 𝑏} → 𝑎 = 𝑏) |
45 | | nesym 2838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ≠ 𝑎 ↔ ¬ 𝑎 = 𝑏) |
46 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑎 = 𝑏 → (𝑎 = 𝑏 → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
47 | 45, 46 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 ≠ 𝑎 → (𝑎 = 𝑏 → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎) → (𝑎 = 𝑏 → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
49 | 10, 48 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → (𝑎 = 𝑏 → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑎 = 𝑏 → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
51 | 50 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (𝑎 = 𝑏 → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
52 | 44, 51 | syl5 33 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → ({𝑎, 𝑚} = {𝑚, 𝑏} → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
53 | 38, 52 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → ((𝐸‘(◡𝐸‘{𝑎, 𝑚})) = (𝐸‘(◡𝐸‘{𝑚, 𝑏})) → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
54 | 30, 53 | syl5com 31 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐸‘{𝑎, 𝑚}) = (◡𝐸‘{𝑚, 𝑏}) → (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
55 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ↔ ¬ (◡𝐸‘{𝑎, 𝑚}) = (◡𝐸‘{𝑚, 𝑏})) |
56 | 55 | biimpri 217 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(◡𝐸‘{𝑎, 𝑚}) = (◡𝐸‘{𝑚, 𝑏}) → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏})) |
57 | 56 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(◡𝐸‘{𝑎, 𝑚}) = (◡𝐸‘{𝑚, 𝑏}) → (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}))) |
58 | 54, 57 | pm2.61i 175 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → (◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏})) |
59 | 58, 34, 37 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ (((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏})) |
60 | 59 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎}))) → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏}))) |
61 | 60 | expcom 450 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏})))) |
62 | 61 | exp31 628 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ 𝑉 → (𝑎 ∈ 𝑉 → (𝑏 ∈ (𝑉 ∖ {𝑎}) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏})))))) |
63 | 62 | com14 94 |
. . . . . . . . . 10
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → (𝑎 ∈ 𝑉 → (𝑏 ∈ (𝑉 ∖ {𝑎}) → (𝑚 ∈ 𝑉 → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏})))))) |
64 | 2, 29, 63 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → (𝑎 ∈ 𝑉 → (𝑏 ∈ (𝑉 ∖ {𝑎}) → (𝑚 ∈ 𝑉 → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏})))))) |
65 | 64 | imp 444 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) → (𝑏 ∈ (𝑉 ∖ {𝑎}) → (𝑚 ∈ 𝑉 → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏}))))) |
66 | 65 | imp41 617 |
. . . . . . 7
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏})) |
67 | | 2pthon3v 26134 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑎 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏)) ∧ ((◡𝐸‘{𝑎, 𝑚}) ≠ (◡𝐸‘{𝑚, 𝑏}) ∧ (𝐸‘(◡𝐸‘{𝑎, 𝑚})) = {𝑎, 𝑚} ∧ (𝐸‘(◡𝐸‘{𝑚, 𝑏})) = {𝑚, 𝑏})) → ∃𝑓∃𝑝(𝑓(𝑎(𝑉 PathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2)) |
68 | 6, 15, 28, 66, 67 | syl31anc 1321 |
. . . . . 6
⊢
(((((𝑉 FriendGrph
𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏))) → ∃𝑓∃𝑝(𝑓(𝑎(𝑉 PathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2)) |
69 | 68 | ex 449 |
. . . . 5
⊢ ((((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → ((({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ∃𝑓∃𝑝(𝑓(𝑎(𝑉 PathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2))) |
70 | 69 | rexlimdva 3013 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (∃𝑚 ∈ 𝑉 (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ∃𝑓∃𝑝(𝑓(𝑎(𝑉 PathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2))) |
71 | 70 | ralimdva 2945 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑎 ∈ 𝑉) → (∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑚 ∈ 𝑉 (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑓∃𝑝(𝑓(𝑎(𝑉 PathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2))) |
72 | 71 | ralimdva 2945 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑚 ∈ 𝑉 (({𝑎, 𝑚} ∈ ran 𝐸 ∧ {𝑚, 𝑏} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏)) → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑓∃𝑝(𝑓(𝑎(𝑉 PathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2))) |
73 | 1, 72 | mpd 15 |
1
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑓∃𝑝(𝑓(𝑎(𝑉 PathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2)) |