Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = ( Vtx ` <. V , { <. A , { B , C } >. } >. ) |
2 |
|
simpllr |
|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> A e. X ) |
3 |
|
simplrl |
|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> B e. V ) |
4 |
|
simpl |
|- ( ( V e. W /\ A e. X ) -> V e. W ) |
5 |
4
|
adantr |
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> V e. W ) |
6 |
|
snex |
|- { <. A , { B , C } >. } e. _V |
7 |
6
|
a1i |
|- ( B =/= C -> { <. A , { B , C } >. } e. _V ) |
8 |
|
opvtxfv |
|- ( ( V e. W /\ { <. A , { B , C } >. } e. _V ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V ) |
9 |
5 7 8
|
syl2an |
|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V ) |
10 |
3 9
|
eleqtrrd |
|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> B e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) ) |
11 |
|
simprr |
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> C e. V ) |
12 |
6
|
a1i |
|- ( ( B e. V /\ C e. V ) -> { <. A , { B , C } >. } e. _V ) |
13 |
4 12 8
|
syl2an |
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( Vtx ` <. V , { <. A , { B , C } >. } >. ) = V ) |
14 |
11 13
|
eleqtrrd |
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> C e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) ) |
15 |
14
|
adantr |
|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> C e. ( Vtx ` <. V , { <. A , { B , C } >. } >. ) ) |
16 |
|
opiedgfv |
|- ( ( V e. W /\ { <. A , { B , C } >. } e. _V ) -> ( iEdg ` <. V , { <. A , { B , C } >. } >. ) = { <. A , { B , C } >. } ) |
17 |
5 7 16
|
syl2an |
|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> ( iEdg ` <. V , { <. A , { B , C } >. } >. ) = { <. A , { B , C } >. } ) |
18 |
|
simpr |
|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> B =/= C ) |
19 |
1 2 10 15 17 18
|
usgr1e |
|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ B =/= C ) -> <. V , { <. A , { B , C } >. } >. e. USGraph ) |
20 |
19
|
ex |
|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( B =/= C -> <. V , { <. A , { B , C } >. } >. e. USGraph ) ) |