Step |
Hyp |
Ref |
Expression |
1 |
|
acsdrscl.f |
|- F = ( mrCls ` C ) |
2 |
|
fveq2 |
|- ( s = S -> ( F ` s ) = ( F ` S ) ) |
3 |
|
pweq |
|- ( s = S -> ~P s = ~P S ) |
4 |
3
|
ineq1d |
|- ( s = S -> ( ~P s i^i Fin ) = ( ~P S i^i Fin ) ) |
5 |
4
|
imaeq2d |
|- ( s = S -> ( F " ( ~P s i^i Fin ) ) = ( F " ( ~P S i^i Fin ) ) ) |
6 |
5
|
unieqd |
|- ( s = S -> U. ( F " ( ~P s i^i Fin ) ) = U. ( F " ( ~P S i^i Fin ) ) ) |
7 |
2 6
|
eqeq12d |
|- ( s = S -> ( ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) <-> ( F ` S ) = U. ( F " ( ~P S i^i Fin ) ) ) ) |
8 |
|
isacs3lem |
|- ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) ) |
9 |
1
|
isacs4lem |
|- ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) -> ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) ) |
10 |
1
|
isacs5lem |
|- ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) ) |
11 |
8 9 10
|
3syl |
|- ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) ) |
12 |
11
|
simprd |
|- ( C e. ( ACS ` X ) -> A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) |
13 |
12
|
adantr |
|- ( ( C e. ( ACS ` X ) /\ S C_ X ) -> A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) |
14 |
|
elfvdm |
|- ( C e. ( ACS ` X ) -> X e. dom ACS ) |
15 |
|
elpw2g |
|- ( X e. dom ACS -> ( S e. ~P X <-> S C_ X ) ) |
16 |
14 15
|
syl |
|- ( C e. ( ACS ` X ) -> ( S e. ~P X <-> S C_ X ) ) |
17 |
16
|
biimpar |
|- ( ( C e. ( ACS ` X ) /\ S C_ X ) -> S e. ~P X ) |
18 |
7 13 17
|
rspcdva |
|- ( ( C e. ( ACS ` X ) /\ S C_ X ) -> ( F ` S ) = U. ( F " ( ~P S i^i Fin ) ) ) |