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 |
|
dfss3 |
|- ( ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. ( ( I ` s ) i^i ( I ` t ) ) x e. ( I ` ( s i^i t ) ) ) |
5 |
1 2 3
|
ntrneiiex |
|- ( ph -> I e. ( ~P B ^m ~P B ) ) |
6 |
|
elmapi |
|- ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B ) |
7 |
5 6
|
syl |
|- ( ph -> I : ~P B --> ~P B ) |
8 |
7
|
ffvelrnda |
|- ( ( ph /\ s e. ~P B ) -> ( I ` s ) e. ~P B ) |
9 |
8
|
elpwid |
|- ( ( ph /\ s e. ~P B ) -> ( I ` s ) C_ B ) |
10 |
|
ssinss1 |
|- ( ( I ` s ) C_ B -> ( ( I ` s ) i^i ( I ` t ) ) C_ B ) |
11 |
9 10
|
syl |
|- ( ( ph /\ s e. ~P B ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ B ) |
12 |
11
|
adantr |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` s ) i^i ( I ` t ) ) C_ B ) |
13 |
|
ralss |
|- ( ( ( I ` s ) i^i ( I ` t ) ) C_ B -> ( A. x e. ( ( I ` s ) i^i ( I ` t ) ) x e. ( I ` ( s i^i t ) ) <-> A. x e. B ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) ) ) |
14 |
12 13
|
syl |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. ( ( I ` s ) i^i ( I ` t ) ) x e. ( I ` ( s i^i t ) ) <-> A. x e. B ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) ) ) |
15 |
|
elin |
|- ( x e. ( ( I ` s ) i^i ( I ` t ) ) <-> ( x e. ( I ` s ) /\ x e. ( I ` t ) ) ) |
16 |
3
|
ad3antrrr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> I F N ) |
17 |
|
simpr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> x e. B ) |
18 |
|
simpllr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s e. ~P B ) |
19 |
1 2 16 17 18
|
ntrneiel |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) ) |
20 |
|
simplr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t e. ~P B ) |
21 |
1 2 16 17 20
|
ntrneiel |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` t ) <-> t e. ( N ` x ) ) ) |
22 |
19 21
|
anbi12d |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( x e. ( I ` s ) /\ x e. ( I ` t ) ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) |
23 |
15 22
|
syl5bb |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( ( I ` s ) i^i ( I ` t ) ) <-> ( s e. ( N ` x ) /\ t e. ( N ` x ) ) ) ) |
24 |
1 2 3
|
ntrneibex |
|- ( ph -> B e. _V ) |
25 |
24
|
ad3antrrr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> B e. _V ) |
26 |
18
|
elpwid |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s C_ B ) |
27 |
|
ssinss1 |
|- ( s C_ B -> ( s i^i t ) C_ B ) |
28 |
26 27
|
syl |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( s i^i t ) C_ B ) |
29 |
25 28
|
sselpwd |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( s i^i t ) e. ~P B ) |
30 |
1 2 16 17 29
|
ntrneiel |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` ( s i^i t ) ) <-> ( s i^i t ) e. ( N ` x ) ) ) |
31 |
23 30
|
imbi12d |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) <-> ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) ) |
32 |
31
|
ralbidva |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( x e. ( ( I ` s ) i^i ( I ` t ) ) -> x e. ( I ` ( s i^i t ) ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) ) |
33 |
14 32
|
bitrd |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. ( ( I ` s ) i^i ( I ` t ) ) x e. ( I ` ( s i^i t ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) ) |
34 |
4 33
|
syl5bb |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) ) |
35 |
34
|
ralbidva |
|- ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) ) |
36 |
|
ralcom |
|- ( A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) <-> A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) |
37 |
35 36
|
bitrdi |
|- ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) ) |
38 |
37
|
ralbidva |
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. s e. ~P B A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) ) |
39 |
|
ralcom |
|- ( A. s e. ~P B A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) |
40 |
38 39
|
bitrdi |
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ t e. ( N ` x ) ) -> ( s i^i t ) e. ( N ` x ) ) ) ) |