Metamath Proof Explorer

Theorem cusgrfilem3

Description: Lemma 3 for cusgrfi . (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 11-Nov-2020)

Ref Expression
Hypotheses cusgrfi.v 
|- V = ( Vtx ` G )
cusgrfi.p 
|- P = { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) }
cusgrfi.f 
|- F = ( x e. ( V \ { N } ) |-> { x , N } )
Assertion cusgrfilem3 
|- ( N e. V -> ( V e. Fin <-> P e. Fin ) )

Proof

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 ) )