| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cusgrfi.v |
|- V = ( Vtx ` G ) |
| 2 |
|
cusgrfi.p |
|- P = { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) } |
| 3 |
|
cusgrfi.f |
|- F = ( x e. ( V \ { N } ) |-> { x , N } ) |
| 4 |
|
diffi |
|- ( V e. Fin -> ( V \ { N } ) e. Fin ) |
| 5 |
|
simpr |
|- ( ( N e. V /\ -. V e. Fin ) -> -. V e. Fin ) |
| 6 |
|
snfi |
|- { N } e. Fin |
| 7 |
|
difinf |
|- ( ( -. V e. Fin /\ { N } e. Fin ) -> -. ( V \ { N } ) e. Fin ) |
| 8 |
5 6 7
|
sylancl |
|- ( ( N e. V /\ -. V e. Fin ) -> -. ( V \ { N } ) e. Fin ) |
| 9 |
8
|
ex |
|- ( N e. V -> ( -. V e. Fin -> -. ( V \ { N } ) e. Fin ) ) |
| 10 |
9
|
con4d |
|- ( N e. V -> ( ( V \ { N } ) e. Fin -> V e. Fin ) ) |
| 11 |
4 10
|
impbid2 |
|- ( N e. V -> ( V e. Fin <-> ( V \ { N } ) e. Fin ) ) |
| 12 |
1
|
fvexi |
|- V e. _V |
| 13 |
12
|
difexi |
|- ( V \ { N } ) e. _V |
| 14 |
|
mptexg |
|- ( ( V \ { N } ) e. _V -> ( x e. ( V \ { N } ) |-> { x , N } ) e. _V ) |
| 15 |
13 14
|
mp1i |
|- ( N e. V -> ( x e. ( V \ { N } ) |-> { x , N } ) e. _V ) |
| 16 |
3 15
|
eqeltrid |
|- ( N e. V -> F e. _V ) |
| 17 |
1 2 3
|
cusgrfilem2 |
|- ( N e. V -> F : ( V \ { N } ) -1-1-onto-> P ) |
| 18 |
|
f1oeq1 |
|- ( f = F -> ( f : ( V \ { N } ) -1-1-onto-> P <-> F : ( V \ { N } ) -1-1-onto-> P ) ) |
| 19 |
16 17 18
|
spcedv |
|- ( N e. V -> E. f f : ( V \ { N } ) -1-1-onto-> P ) |
| 20 |
|
bren |
|- ( ( V \ { N } ) ~~ P <-> E. f f : ( V \ { N } ) -1-1-onto-> P ) |
| 21 |
19 20
|
sylibr |
|- ( N e. V -> ( V \ { N } ) ~~ P ) |
| 22 |
|
enfi |
|- ( ( V \ { N } ) ~~ P -> ( ( V \ { N } ) e. Fin <-> P e. Fin ) ) |
| 23 |
21 22
|
syl |
|- ( N e. V -> ( ( V \ { N } ) e. Fin <-> P e. Fin ) ) |
| 24 |
11 23
|
bitrd |
|- ( N e. V -> ( V e. Fin <-> P e. Fin ) ) |