Step |
Hyp |
Ref |
Expression |
1 |
|
usgrexi.p |
|- P = { x e. ~P V | ( # ` x ) = 2 } |
2 |
|
simpr |
|- ( ( V e. W /\ v e. V ) -> v e. V ) |
3 |
|
eldifi |
|- ( n e. ( V \ { v } ) -> n e. V ) |
4 |
|
prelpwi |
|- ( ( v e. V /\ n e. V ) -> { v , n } e. ~P V ) |
5 |
2 3 4
|
syl2an |
|- ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> { v , n } e. ~P V ) |
6 |
|
eldifsni |
|- ( n e. ( V \ { v } ) -> n =/= v ) |
7 |
6
|
necomd |
|- ( n e. ( V \ { v } ) -> v =/= n ) |
8 |
7
|
adantl |
|- ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> v =/= n ) |
9 |
|
hashprg |
|- ( ( v e. V /\ n e. V ) -> ( v =/= n <-> ( # ` { v , n } ) = 2 ) ) |
10 |
2 3 9
|
syl2an |
|- ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( v =/= n <-> ( # ` { v , n } ) = 2 ) ) |
11 |
8 10
|
mpbid |
|- ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> ( # ` { v , n } ) = 2 ) |
12 |
|
fveqeq2 |
|- ( x = { v , n } -> ( ( # ` x ) = 2 <-> ( # ` { v , n } ) = 2 ) ) |
13 |
|
rnresi |
|- ran ( _I |` P ) = P |
14 |
13 1
|
eqtri |
|- ran ( _I |` P ) = { x e. ~P V | ( # ` x ) = 2 } |
15 |
12 14
|
elrab2 |
|- ( { v , n } e. ran ( _I |` P ) <-> ( { v , n } e. ~P V /\ ( # ` { v , n } ) = 2 ) ) |
16 |
5 11 15
|
sylanbrc |
|- ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> { v , n } e. ran ( _I |` P ) ) |
17 |
|
sseq2 |
|- ( e = { v , n } -> ( { v , n } C_ e <-> { v , n } C_ { v , n } ) ) |
18 |
17
|
adantl |
|- ( ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) /\ e = { v , n } ) -> ( { v , n } C_ e <-> { v , n } C_ { v , n } ) ) |
19 |
|
ssidd |
|- ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> { v , n } C_ { v , n } ) |
20 |
16 18 19
|
rspcedvd |
|- ( ( ( V e. W /\ v e. V ) /\ n e. ( V \ { v } ) ) -> E. e e. ran ( _I |` P ) { v , n } C_ e ) |