Step |
Hyp |
Ref |
Expression |
1 |
|
lppthon.i |
|- I = ( iEdg ` G ) |
2 |
|
eqid |
|- <" A A "> = <" A A "> |
3 |
|
eqid |
|- <" J "> = <" J "> |
4 |
1
|
lpvtx |
|- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> A e. ( Vtx ` G ) ) |
5 |
|
simpl3 |
|- ( ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) /\ A = A ) -> ( I ` J ) = { A } ) |
6 |
|
eqid |
|- A = A |
7 |
|
eqneqall |
|- ( A = A -> ( A =/= A -> { A , A } C_ ( I ` J ) ) ) |
8 |
6 7
|
ax-mp |
|- ( A =/= A -> { A , A } C_ ( I ` J ) ) |
9 |
8
|
adantl |
|- ( ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) /\ A =/= A ) -> { A , A } C_ ( I ` J ) ) |
10 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
11 |
2 3 4 4 5 9 10 1
|
1pthond |
|- ( ( G e. UHGraph /\ J e. dom I /\ ( I ` J ) = { A } ) -> <" J "> ( A ( PathsOn ` G ) A ) <" A A "> ) |