Step |
Hyp |
Ref |
Expression |
1 |
|
isnacs.f |
|- F = ( mrCls ` C ) |
2 |
|
elfvex |
|- ( C e. ( NoeACS ` X ) -> X e. _V ) |
3 |
|
elfvex |
|- ( C e. ( ACS ` X ) -> X e. _V ) |
4 |
3
|
adantr |
|- ( ( C e. ( ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) -> X e. _V ) |
5 |
|
fveq2 |
|- ( x = X -> ( ACS ` x ) = ( ACS ` X ) ) |
6 |
|
pweq |
|- ( x = X -> ~P x = ~P X ) |
7 |
6
|
ineq1d |
|- ( x = X -> ( ~P x i^i Fin ) = ( ~P X i^i Fin ) ) |
8 |
7
|
rexeqdv |
|- ( x = X -> ( E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g ) <-> E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) ) ) |
9 |
8
|
ralbidv |
|- ( x = X -> ( A. s e. c E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g ) <-> A. s e. c E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) ) ) |
10 |
5 9
|
rabeqbidv |
|- ( x = X -> { c e. ( ACS ` x ) | A. s e. c E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g ) } = { c e. ( ACS ` X ) | A. s e. c E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) } ) |
11 |
|
df-nacs |
|- NoeACS = ( x e. _V |-> { c e. ( ACS ` x ) | A. s e. c E. g e. ( ~P x i^i Fin ) s = ( ( mrCls ` c ) ` g ) } ) |
12 |
|
fvex |
|- ( ACS ` X ) e. _V |
13 |
12
|
rabex |
|- { c e. ( ACS ` X ) | A. s e. c E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) } e. _V |
14 |
10 11 13
|
fvmpt |
|- ( X e. _V -> ( NoeACS ` X ) = { c e. ( ACS ` X ) | A. s e. c E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) } ) |
15 |
14
|
eleq2d |
|- ( X e. _V -> ( C e. ( NoeACS ` X ) <-> C e. { c e. ( ACS ` X ) | A. s e. c E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) } ) ) |
16 |
|
fveq2 |
|- ( c = C -> ( mrCls ` c ) = ( mrCls ` C ) ) |
17 |
16 1
|
eqtr4di |
|- ( c = C -> ( mrCls ` c ) = F ) |
18 |
17
|
fveq1d |
|- ( c = C -> ( ( mrCls ` c ) ` g ) = ( F ` g ) ) |
19 |
18
|
eqeq2d |
|- ( c = C -> ( s = ( ( mrCls ` c ) ` g ) <-> s = ( F ` g ) ) ) |
20 |
19
|
rexbidv |
|- ( c = C -> ( E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) <-> E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) ) |
21 |
20
|
raleqbi1dv |
|- ( c = C -> ( A. s e. c E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) <-> A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) ) |
22 |
21
|
elrab |
|- ( C e. { c e. ( ACS ` X ) | A. s e. c E. g e. ( ~P X i^i Fin ) s = ( ( mrCls ` c ) ` g ) } <-> ( C e. ( ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) ) |
23 |
15 22
|
bitrdi |
|- ( X e. _V -> ( C e. ( NoeACS ` X ) <-> ( C e. ( ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) ) ) |
24 |
2 4 23
|
pm5.21nii |
|- ( C e. ( NoeACS ` X ) <-> ( C e. ( ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) ) |