Step |
Hyp |
Ref |
Expression |
1 |
|
ntrnei.o |
|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) ) |
2 |
|
ntrnei.f |
|- F = ( ~P B O B ) |
3 |
|
ntrnei.r |
|- ( ph -> I F N ) |
4 |
|
ntrneifv.s |
|- ( ph -> S e. ~P B ) |
5 |
|
dfin5 |
|- ( B i^i ( I ` S ) ) = { x e. B | x e. ( I ` S ) } |
6 |
1 2 3
|
ntrneiiex |
|- ( ph -> I e. ( ~P B ^m ~P B ) ) |
7 |
|
elmapi |
|- ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B ) |
8 |
6 7
|
syl |
|- ( ph -> I : ~P B --> ~P B ) |
9 |
8 4
|
ffvelrnd |
|- ( ph -> ( I ` S ) e. ~P B ) |
10 |
9
|
elpwid |
|- ( ph -> ( I ` S ) C_ B ) |
11 |
|
sseqin2 |
|- ( ( I ` S ) C_ B <-> ( B i^i ( I ` S ) ) = ( I ` S ) ) |
12 |
10 11
|
sylib |
|- ( ph -> ( B i^i ( I ` S ) ) = ( I ` S ) ) |
13 |
3
|
adantr |
|- ( ( ph /\ x e. B ) -> I F N ) |
14 |
|
simpr |
|- ( ( ph /\ x e. B ) -> x e. B ) |
15 |
4
|
adantr |
|- ( ( ph /\ x e. B ) -> S e. ~P B ) |
16 |
1 2 13 14 15
|
ntrneiel |
|- ( ( ph /\ x e. B ) -> ( x e. ( I ` S ) <-> S e. ( N ` x ) ) ) |
17 |
16
|
rabbidva |
|- ( ph -> { x e. B | x e. ( I ` S ) } = { x e. B | S e. ( N ` x ) } ) |
18 |
5 12 17
|
3eqtr3a |
|- ( ph -> ( I ` S ) = { x e. B | S e. ( N ` x ) } ) |