Step |
Hyp |
Ref |
Expression |
1 |
|
acsficld.1 |
|- ( ph -> A e. ( ACS ` X ) ) |
2 |
|
acsficld.2 |
|- N = ( mrCls ` A ) |
3 |
|
acsficld.3 |
|- ( ph -> S C_ X ) |
4 |
1 2 3
|
acsficld |
|- ( ph -> ( N ` S ) = U. ( N " ( ~P S i^i Fin ) ) ) |
5 |
4
|
eleq2d |
|- ( ph -> ( Y e. ( N ` S ) <-> Y e. U. ( N " ( ~P S i^i Fin ) ) ) ) |
6 |
1
|
acsmred |
|- ( ph -> A e. ( Moore ` X ) ) |
7 |
|
funmpt |
|- Fun ( z e. ~P X |-> |^| { w e. A | z C_ w } ) |
8 |
2
|
mrcfval |
|- ( A e. ( Moore ` X ) -> N = ( z e. ~P X |-> |^| { w e. A | z C_ w } ) ) |
9 |
8
|
funeqd |
|- ( A e. ( Moore ` X ) -> ( Fun N <-> Fun ( z e. ~P X |-> |^| { w e. A | z C_ w } ) ) ) |
10 |
7 9
|
mpbiri |
|- ( A e. ( Moore ` X ) -> Fun N ) |
11 |
|
eluniima |
|- ( Fun N -> ( Y e. U. ( N " ( ~P S i^i Fin ) ) <-> E. x e. ( ~P S i^i Fin ) Y e. ( N ` x ) ) ) |
12 |
6 10 11
|
3syl |
|- ( ph -> ( Y e. U. ( N " ( ~P S i^i Fin ) ) <-> E. x e. ( ~P S i^i Fin ) Y e. ( N ` x ) ) ) |
13 |
5 12
|
bitrd |
|- ( ph -> ( Y e. ( N ` S ) <-> E. x e. ( ~P S i^i Fin ) Y e. ( N ` x ) ) ) |