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 |
|
dfss2 |
|- ( ( I ` s ) C_ ( I ` t ) <-> A. x ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) |
5 |
4
|
imbi2i |
|- ( ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> ( s C_ t -> A. x ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) |
6 |
|
19.21v |
|- ( A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> ( s C_ t -> A. x ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) |
7 |
5 6
|
bitr4i |
|- ( ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) |
8 |
|
ax-1 |
|- ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) -> ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) |
9 |
|
simpll |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ph ) |
10 |
1 2 3
|
ntrneiiex |
|- ( ph -> I e. ( ~P B ^m ~P B ) ) |
11 |
|
elmapi |
|- ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B ) |
12 |
9 10 11
|
3syl |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> I : ~P B --> ~P B ) |
13 |
|
simplr |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> s e. ~P B ) |
14 |
12 13
|
ffvelrnd |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) e. ~P B ) |
15 |
14
|
elpwid |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) C_ B ) |
16 |
15
|
sselda |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. ( I ` s ) ) -> x e. B ) |
17 |
16
|
pm2.24d |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. ( I ` s ) ) -> ( -. x e. B -> x e. ( I ` t ) ) ) |
18 |
17
|
ex |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( x e. ( I ` s ) -> ( -. x e. B -> x e. ( I ` t ) ) ) ) |
19 |
18
|
com23 |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( -. x e. B -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) |
20 |
19
|
a1dd |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( -. x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) |
21 |
|
idd |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) |
22 |
20 21
|
jad |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) |
23 |
8 22
|
impbid2 |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) ) |
24 |
23
|
albidv |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) ) |
25 |
|
df-ral |
|- ( A. x e. B ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x ( x e. B -> ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) |
26 |
24 25
|
bitr4di |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x e. B ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) ) ) |
27 |
3
|
ad3antrrr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> I F N ) |
28 |
|
simpr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> x e. B ) |
29 |
|
simpllr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s e. ~P B ) |
30 |
1 2 27 28 29
|
ntrneiel |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) ) |
31 |
|
simplr |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t e. ~P B ) |
32 |
1 2 27 28 31
|
ntrneiel |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` t ) <-> t e. ( N ` x ) ) ) |
33 |
30 32
|
imbi12d |
|- ( ( ( ( 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 ) ) ) ) |
34 |
33
|
imbi2d |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> ( s C_ t -> ( s e. ( N ` x ) -> t e. ( N ` x ) ) ) ) ) |
35 |
|
impexp |
|- ( ( ( s C_ t /\ s e. ( N ` x ) ) -> t e. ( N ` x ) ) <-> ( s C_ t -> ( s e. ( N ` x ) -> t e. ( N ` x ) ) ) ) |
36 |
|
ancomst |
|- ( ( ( s C_ t /\ s e. ( N ` x ) ) -> t e. ( N ` x ) ) <-> ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) |
37 |
35 36
|
bitr3i |
|- ( ( s C_ t -> ( s e. ( N ` x ) -> t e. ( N ` x ) ) ) <-> ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) |
38 |
34 37
|
bitrdi |
|- ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) ) |
39 |
38
|
ralbidva |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) ) |
40 |
26 39
|
bitrd |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x ( s C_ t -> ( x e. ( I ` s ) -> x e. ( I ` t ) ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) ) |
41 |
7 40
|
syl5bb |
|- ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) ) |
42 |
41
|
ralbidva |
|- ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) ) |
43 |
|
ralcom |
|- ( A. t e. ~P B A. x e. B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) <-> A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) |
44 |
42 43
|
bitrdi |
|- ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) ) |
45 |
44
|
ralbidva |
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. s e. ~P B A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) ) |
46 |
|
ralcom |
|- ( A. s e. ~P B A. x e. B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) |
47 |
45 46
|
bitrdi |
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( s C_ t -> ( I ` s ) C_ ( I ` t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s e. ( N ` x ) /\ s C_ t ) -> t e. ( N ` x ) ) ) ) |