Step |
Hyp |
Ref |
Expression |
1 |
|
umgr2adedgwlk.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
2 |
|
umgr2adedgwlk.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
3 |
|
umgr2adedgwlk.f |
⊢ 𝐹 = 〈“ 𝐽 𝐾 ”〉 |
4 |
|
umgr2adedgwlk.p |
⊢ 𝑃 = 〈“ 𝐴 𝐵 𝐶 ”〉 |
5 |
|
umgr2adedgwlk.g |
⊢ ( 𝜑 → 𝐺 ∈ UMGraph ) |
6 |
|
umgr2adedgwlk.a |
⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) |
7 |
|
umgr2adedgwlk.j |
⊢ ( 𝜑 → ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } ) |
8 |
|
umgr2adedgwlk.k |
⊢ ( 𝜑 → ( 𝐼 ‘ 𝐾 ) = { 𝐵 , 𝐶 } ) |
9 |
|
umgr2adedgspth.n |
⊢ ( 𝜑 → 𝐴 ≠ 𝐶 ) |
10 |
|
3anass |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐺 ∈ UMGraph ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ) |
11 |
5 6 10
|
sylanbrc |
⊢ ( 𝜑 → ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) |
12 |
1
|
umgr2adedgwlklem |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
13 |
11 12
|
syl |
⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
14 |
13
|
simprd |
⊢ ( 𝜑 → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
15 |
13
|
simpld |
⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) |
16 |
|
ssid |
⊢ { 𝐴 , 𝐵 } ⊆ { 𝐴 , 𝐵 } |
17 |
16 7
|
sseqtrrid |
⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ) |
18 |
|
ssid |
⊢ { 𝐵 , 𝐶 } ⊆ { 𝐵 , 𝐶 } |
19 |
18 8
|
sseqtrrid |
⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) |
20 |
17 19
|
jca |
⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) ) |
21 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
22 |
|
fveq2 |
⊢ ( 𝐾 = 𝐽 → ( 𝐼 ‘ 𝐾 ) = ( 𝐼 ‘ 𝐽 ) ) |
23 |
22
|
eqcoms |
⊢ ( 𝐽 = 𝐾 → ( 𝐼 ‘ 𝐾 ) = ( 𝐼 ‘ 𝐽 ) ) |
24 |
23
|
eqeq1d |
⊢ ( 𝐽 = 𝐾 → ( ( 𝐼 ‘ 𝐾 ) = { 𝐵 , 𝐶 } ↔ ( 𝐼 ‘ 𝐽 ) = { 𝐵 , 𝐶 } ) ) |
25 |
|
eqtr2 |
⊢ ( ( ( 𝐼 ‘ 𝐽 ) = { 𝐵 , 𝐶 } ∧ ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } ) → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) |
26 |
25
|
ex |
⊢ ( ( 𝐼 ‘ 𝐽 ) = { 𝐵 , 𝐶 } → ( ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) ) |
27 |
24 26
|
syl6bi |
⊢ ( 𝐽 = 𝐾 → ( ( 𝐼 ‘ 𝐾 ) = { 𝐵 , 𝐶 } → ( ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) ) ) |
28 |
27
|
com13 |
⊢ ( ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } → ( ( 𝐼 ‘ 𝐾 ) = { 𝐵 , 𝐶 } → ( 𝐽 = 𝐾 → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) ) ) |
29 |
7 8 28
|
sylc |
⊢ ( 𝜑 → ( 𝐽 = 𝐾 → { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ) ) |
30 |
|
eqcom |
⊢ ( { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ) |
31 |
|
prcom |
⊢ { 𝐵 , 𝐶 } = { 𝐶 , 𝐵 } |
32 |
31
|
eqeq2i |
⊢ ( { 𝐴 , 𝐵 } = { 𝐵 , 𝐶 } ↔ { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } ) |
33 |
30 32
|
bitri |
⊢ ( { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } ) |
34 |
21 1
|
umgrpredgv |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) |
35 |
34
|
simpld |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) |
36 |
35
|
ex |
⊢ ( 𝐺 ∈ UMGraph → ( { 𝐴 , 𝐵 } ∈ 𝐸 → 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) |
37 |
21 1
|
umgrpredgv |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
38 |
37
|
simprd |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) |
39 |
38
|
ex |
⊢ ( 𝐺 ∈ UMGraph → ( { 𝐵 , 𝐶 } ∈ 𝐸 → 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
40 |
36 39
|
anim12d |
⊢ ( 𝐺 ∈ UMGraph → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
41 |
5 6 40
|
sylc |
⊢ ( 𝜑 → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
42 |
|
preqr1g |
⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } → 𝐴 = 𝐶 ) ) |
43 |
41 42
|
syl |
⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } → 𝐴 = 𝐶 ) ) |
44 |
|
eqneqall |
⊢ ( 𝐴 = 𝐶 → ( 𝐴 ≠ 𝐶 → 𝐽 ≠ 𝐾 ) ) |
45 |
43 9 44
|
syl6ci |
⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } → 𝐽 ≠ 𝐾 ) ) |
46 |
33 45
|
syl5bi |
⊢ ( 𝜑 → ( { 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } → 𝐽 ≠ 𝐾 ) ) |
47 |
29 46
|
syld |
⊢ ( 𝜑 → ( 𝐽 = 𝐾 → 𝐽 ≠ 𝐾 ) ) |
48 |
|
neqne |
⊢ ( ¬ 𝐽 = 𝐾 → 𝐽 ≠ 𝐾 ) |
49 |
47 48
|
pm2.61d1 |
⊢ ( 𝜑 → 𝐽 ≠ 𝐾 ) |
50 |
4 3 14 15 20 21 2 49 9
|
2spthd |
⊢ ( 𝜑 → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ) |