Step |
Hyp |
Ref |
Expression |
1 |
|
upgr1e.v |
|- V = ( Vtx ` G ) |
2 |
|
upgr1e.a |
|- ( ph -> A e. X ) |
3 |
|
upgr1e.b |
|- ( ph -> B e. V ) |
4 |
|
upgr1e.c |
|- ( ph -> C e. V ) |
5 |
|
upgr1e.e |
|- ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } ) |
6 |
|
prex |
|- { B , C } e. _V |
7 |
6
|
snid |
|- { B , C } e. { { B , C } } |
8 |
7
|
a1i |
|- ( ph -> { B , C } e. { { B , C } } ) |
9 |
2 8
|
fsnd |
|- ( ph -> { <. A , { B , C } >. } : { A } --> { { B , C } } ) |
10 |
3 4
|
prssd |
|- ( ph -> { B , C } C_ V ) |
11 |
10 1
|
sseqtrdi |
|- ( ph -> { B , C } C_ ( Vtx ` G ) ) |
12 |
6
|
elpw |
|- ( { B , C } e. ~P ( Vtx ` G ) <-> { B , C } C_ ( Vtx ` G ) ) |
13 |
11 12
|
sylibr |
|- ( ph -> { B , C } e. ~P ( Vtx ` G ) ) |
14 |
13 3
|
upgr1elem |
|- ( ph -> { { B , C } } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) |
15 |
9 14
|
fssd |
|- ( ph -> { <. A , { B , C } >. } : { A } --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) |
16 |
15
|
ffdmd |
|- ( ph -> { <. A , { B , C } >. } : dom { <. A , { B , C } >. } --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) |
17 |
5
|
dmeqd |
|- ( ph -> dom ( iEdg ` G ) = dom { <. A , { B , C } >. } ) |
18 |
5 17
|
feq12d |
|- ( ph -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } <-> { <. A , { B , C } >. } : dom { <. A , { B , C } >. } --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) ) |
19 |
16 18
|
mpbird |
|- ( ph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) |
20 |
1
|
1vgrex |
|- ( B e. V -> G e. _V ) |
21 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
22 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
23 |
21 22
|
isupgr |
|- ( G e. _V -> ( G e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) ) |
24 |
3 20 23
|
3syl |
|- ( ph -> ( G e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) ) |
25 |
19 24
|
mpbird |
|- ( ph -> G e. UPGraph ) |