Metamath Proof Explorer

Theorem cusgrfilem2

Description: Lemma 2 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 cusgrfilem2 
|- ( N e. V -> F : ( V \ { N } ) -1-1-onto-> P )

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 eldifi 
 |-  ( x e. ( V \ { N } ) -> x e. V )
5 id 
 |-  ( N e. V -> N e. V )
6 prelpwi 
 |-  ( ( x e. V /\ N e. V ) -> { x , N } e. ~P V )
7 4 5 6 syl2anr 
 |-  ( ( N e. V /\ x e. ( V \ { N } ) ) -> { x , N } e. ~P V )
8 4 adantl 
 |-  ( ( N e. V /\ x e. ( V \ { N } ) ) -> x e. V )
9 eldifsni 
 |-  ( x e. ( V \ { N } ) -> x =/= N )
10 9 adantl 
 |-  ( ( N e. V /\ x e. ( V \ { N } ) ) -> x =/= N )
11 eqidd 
 |-  ( ( N e. V /\ x e. ( V \ { N } ) ) -> { x , N } = { x , N } )
12 10 11 jca 
 |-  ( ( N e. V /\ x e. ( V \ { N } ) ) -> ( x =/= N /\ { x , N } = { x , N } ) )
13 id 
 |-  ( x e. V -> x e. V )
14 neeq1 
 |-  ( a = x -> ( a =/= N <-> x =/= N ) )
15 preq1 
 |-  ( a = x -> { a , N } = { x , N } )
16 15 eqeq2d 
 |-  ( a = x -> ( { x , N } = { a , N } <-> { x , N } = { x , N } ) )
17 14 16 anbi12d 
 |-  ( a = x -> ( ( a =/= N /\ { x , N } = { a , N } ) <-> ( x =/= N /\ { x , N } = { x , N } ) ) )
18 17 adantl 
 |-  ( ( x e. V /\ a = x ) -> ( ( a =/= N /\ { x , N } = { a , N } ) <-> ( x =/= N /\ { x , N } = { x , N } ) ) )
19 13 18 rspcedv 
 |-  ( x e. V -> ( ( x =/= N /\ { x , N } = { x , N } ) -> E. a e. V ( a =/= N /\ { x , N } = { a , N } ) ) )
20 8 12 19 sylc 
 |-  ( ( N e. V /\ x e. ( V \ { N } ) ) -> E. a e. V ( a =/= N /\ { x , N } = { a , N } ) )
21 2 eleq2i 
 |-  ( { x , N } e. P <-> { x , N } e. { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) } )
22 eqeq1 
 |-  ( v = { x , N } -> ( v = { a , N } <-> { x , N } = { a , N } ) )
23 22 anbi2d 
 |-  ( v = { x , N } -> ( ( a =/= N /\ v = { a , N } ) <-> ( a =/= N /\ { x , N } = { a , N } ) ) )
24 23 rexbidv 
 |-  ( v = { x , N } -> ( E. a e. V ( a =/= N /\ v = { a , N } ) <-> E. a e. V ( a =/= N /\ { x , N } = { a , N } ) ) )
25 eqeq1 
 |-  ( x = v -> ( x = { a , N } <-> v = { a , N } ) )
26 25 anbi2d 
 |-  ( x = v -> ( ( a =/= N /\ x = { a , N } ) <-> ( a =/= N /\ v = { a , N } ) ) )
27 26 rexbidv 
 |-  ( x = v -> ( E. a e. V ( a =/= N /\ x = { a , N } ) <-> E. a e. V ( a =/= N /\ v = { a , N } ) ) )
28 27 cbvrabv 
 |-  { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) } = { v e. ~P V | E. a e. V ( a =/= N /\ v = { a , N } ) }
29 24 28 elrab2 
 |-  ( { x , N } e. { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) } <-> ( { x , N } e. ~P V /\ E. a e. V ( a =/= N /\ { x , N } = { a , N } ) ) )
30 21 29 bitri 
 |-  ( { x , N } e. P <-> ( { x , N } e. ~P V /\ E. a e. V ( a =/= N /\ { x , N } = { a , N } ) ) )
31 7 20 30 sylanbrc 
 |-  ( ( N e. V /\ x e. ( V \ { N } ) ) -> { x , N } e. P )
32 31 ralrimiva 
 |-  ( N e. V -> A. x e. ( V \ { N } ) { x , N } e. P )
33 simpl 
 |-  ( ( a =/= N /\ e = { a , N } ) -> a =/= N )
34 33 anim2i 
 |-  ( ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) -> ( a e. V /\ a =/= N ) )
35 34 adantl 
 |-  ( ( ( N e. V /\ e e. ~P V ) /\ ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) ) -> ( a e. V /\ a =/= N ) )
36 eldifsn 
 |-  ( a e. ( V \ { N } ) <-> ( a e. V /\ a =/= N ) )
37 35 36 sylibr 
 |-  ( ( ( N e. V /\ e e. ~P V ) /\ ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) ) -> a e. ( V \ { N } ) )
38 eqeq1 
 |-  ( e = { a , N } -> ( e = { x , N } <-> { a , N } = { x , N } ) )
39 38 adantl 
 |-  ( ( a =/= N /\ e = { a , N } ) -> ( e = { x , N } <-> { a , N } = { x , N } ) )
40 39 ad2antlr 
 |-  ( ( ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) /\ x e. ( V \ { N } ) ) -> ( e = { x , N } <-> { a , N } = { x , N } ) )
41 vex 
 |-  a e. _V
42 vex 
 |-  x e. _V
43 41 42 preqr1 
 |-  ( { a , N } = { x , N } -> a = x )
44 43 equcomd 
 |-  ( { a , N } = { x , N } -> x = a )
45 40 44 syl6bi 
 |-  ( ( ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) /\ x e. ( V \ { N } ) ) -> ( e = { x , N } -> x = a ) )
46 45 adantll 
 |-  ( ( ( ( N e. V /\ e e. ~P V ) /\ ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) ) /\ x e. ( V \ { N } ) ) -> ( e = { x , N } -> x = a ) )
47 15 equcoms 
 |-  ( x = a -> { a , N } = { x , N } )
48 47 eqeq2d 
 |-  ( x = a -> ( e = { a , N } <-> e = { x , N } ) )
49 48 biimpcd 
 |-  ( e = { a , N } -> ( x = a -> e = { x , N } ) )
50 49 adantl 
 |-  ( ( a =/= N /\ e = { a , N } ) -> ( x = a -> e = { x , N } ) )
51 50 adantl 
 |-  ( ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) -> ( x = a -> e = { x , N } ) )
52 51 ad2antlr 
 |-  ( ( ( ( N e. V /\ e e. ~P V ) /\ ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) ) /\ x e. ( V \ { N } ) ) -> ( x = a -> e = { x , N } ) )
53 46 52 impbid 
 |-  ( ( ( ( N e. V /\ e e. ~P V ) /\ ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) ) /\ x e. ( V \ { N } ) ) -> ( e = { x , N } <-> x = a ) )
54 53 ralrimiva 
 |-  ( ( ( N e. V /\ e e. ~P V ) /\ ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) ) -> A. x e. ( V \ { N } ) ( e = { x , N } <-> x = a ) )
55 37 54 jca 
 |-  ( ( ( N e. V /\ e e. ~P V ) /\ ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) ) -> ( a e. ( V \ { N } ) /\ A. x e. ( V \ { N } ) ( e = { x , N } <-> x = a ) ) )
56 55 ex 
 |-  ( ( N e. V /\ e e. ~P V ) -> ( ( a e. V /\ ( a =/= N /\ e = { a , N } ) ) -> ( a e. ( V \ { N } ) /\ A. x e. ( V \ { N } ) ( e = { x , N } <-> x = a ) ) ) )
57 56 reximdv2 
 |-  ( ( N e. V /\ e e. ~P V ) -> ( E. a e. V ( a =/= N /\ e = { a , N } ) -> E. a e. ( V \ { N } ) A. x e. ( V \ { N } ) ( e = { x , N } <-> x = a ) ) )
58 57 expimpd 
 |-  ( N e. V -> ( ( e e. ~P V /\ E. a e. V ( a =/= N /\ e = { a , N } ) ) -> E. a e. ( V \ { N } ) A. x e. ( V \ { N } ) ( e = { x , N } <-> x = a ) ) )
59 eqeq1 
 |-  ( x = e -> ( x = { a , N } <-> e = { a , N } ) )
60 59 anbi2d 
 |-  ( x = e -> ( ( a =/= N /\ x = { a , N } ) <-> ( a =/= N /\ e = { a , N } ) ) )
61 60 rexbidv 
 |-  ( x = e -> ( E. a e. V ( a =/= N /\ x = { a , N } ) <-> E. a e. V ( a =/= N /\ e = { a , N } ) ) )
62 61 2 elrab2 
 |-  ( e e. P <-> ( e e. ~P V /\ E. a e. V ( a =/= N /\ e = { a , N } ) ) )
63 reu6 
 |-  ( E! x e. ( V \ { N } ) e = { x , N } <-> E. a e. ( V \ { N } ) A. x e. ( V \ { N } ) ( e = { x , N } <-> x = a ) )
64 58 62 63 3imtr4g 
 |-  ( N e. V -> ( e e. P -> E! x e. ( V \ { N } ) e = { x , N } ) )
65 64 ralrimiv 
 |-  ( N e. V -> A. e e. P E! x e. ( V \ { N } ) e = { x , N } )
66 3 f1ompt 
 |-  ( F : ( V \ { N } ) -1-1-onto-> P <-> ( A. x e. ( V \ { N } ) { x , N } e. P /\ A. e e. P E! x e. ( V \ { N } ) e = { x , N } ) )
67 32 65 66 sylanbrc 
 |-  ( N e. V -> F : ( V \ { N } ) -1-1-onto-> P )