| Step |
Hyp |
Ref |
Expression |
| 1 |
|
upgr1wlkd.p |
|- P = <" X Y "> |
| 2 |
|
upgr1wlkd.f |
|- F = <" J "> |
| 3 |
|
upgr1wlkd.x |
|- ( ph -> X e. ( Vtx ` G ) ) |
| 4 |
|
upgr1wlkd.y |
|- ( ph -> Y e. ( Vtx ` G ) ) |
| 5 |
|
upgr1wlkd.j |
|- ( ph -> ( ( iEdg ` G ) ` J ) = { X , Y } ) |
| 6 |
|
ssid |
|- { X , Y } C_ { X , Y } |
| 7 |
|
sseq2 |
|- ( ( ( iEdg ` G ) ` J ) = { X , Y } -> ( { X , Y } C_ ( ( iEdg ` G ) ` J ) <-> { X , Y } C_ { X , Y } ) ) |
| 8 |
7
|
adantl |
|- ( ( ( ph /\ X =/= Y ) /\ ( ( iEdg ` G ) ` J ) = { X , Y } ) -> ( { X , Y } C_ ( ( iEdg ` G ) ` J ) <-> { X , Y } C_ { X , Y } ) ) |
| 9 |
6 8
|
mpbiri |
|- ( ( ( ph /\ X =/= Y ) /\ ( ( iEdg ` G ) ` J ) = { X , Y } ) -> { X , Y } C_ ( ( iEdg ` G ) ` J ) ) |
| 10 |
5 9
|
mpidan |
|- ( ( ph /\ X =/= Y ) -> { X , Y } C_ ( ( iEdg ` G ) ` J ) ) |