Step |
Hyp |
Ref |
Expression |
1 |
|
acsdrscl.f |
|- F = ( mrCls ` C ) |
2 |
|
unifpw |
|- U. ( ~P s i^i Fin ) = s |
3 |
2
|
fveq2i |
|- ( F ` U. ( ~P s i^i Fin ) ) = ( F ` s ) |
4 |
|
vex |
|- s e. _V |
5 |
|
fpwipodrs |
|- ( s e. _V -> ( toInc ` ( ~P s i^i Fin ) ) e. Dirset ) |
6 |
4 5
|
mp1i |
|- ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( toInc ` ( ~P s i^i Fin ) ) e. Dirset ) |
7 |
|
fveq2 |
|- ( t = ( ~P s i^i Fin ) -> ( toInc ` t ) = ( toInc ` ( ~P s i^i Fin ) ) ) |
8 |
7
|
eleq1d |
|- ( t = ( ~P s i^i Fin ) -> ( ( toInc ` t ) e. Dirset <-> ( toInc ` ( ~P s i^i Fin ) ) e. Dirset ) ) |
9 |
|
unieq |
|- ( t = ( ~P s i^i Fin ) -> U. t = U. ( ~P s i^i Fin ) ) |
10 |
9
|
fveq2d |
|- ( t = ( ~P s i^i Fin ) -> ( F ` U. t ) = ( F ` U. ( ~P s i^i Fin ) ) ) |
11 |
|
imaeq2 |
|- ( t = ( ~P s i^i Fin ) -> ( F " t ) = ( F " ( ~P s i^i Fin ) ) ) |
12 |
11
|
unieqd |
|- ( t = ( ~P s i^i Fin ) -> U. ( F " t ) = U. ( F " ( ~P s i^i Fin ) ) ) |
13 |
10 12
|
eqeq12d |
|- ( t = ( ~P s i^i Fin ) -> ( ( F ` U. t ) = U. ( F " t ) <-> ( F ` U. ( ~P s i^i Fin ) ) = U. ( F " ( ~P s i^i Fin ) ) ) ) |
14 |
8 13
|
imbi12d |
|- ( t = ( ~P s i^i Fin ) -> ( ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) <-> ( ( toInc ` ( ~P s i^i Fin ) ) e. Dirset -> ( F ` U. ( ~P s i^i Fin ) ) = U. ( F " ( ~P s i^i Fin ) ) ) ) ) |
15 |
|
simplr |
|- ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) |
16 |
|
inss1 |
|- ( ~P s i^i Fin ) C_ ~P s |
17 |
|
elpwi |
|- ( s e. ~P X -> s C_ X ) |
18 |
17
|
sspwd |
|- ( s e. ~P X -> ~P s C_ ~P X ) |
19 |
18
|
adantl |
|- ( ( C e. ( Moore ` X ) /\ s e. ~P X ) -> ~P s C_ ~P X ) |
20 |
16 19
|
sstrid |
|- ( ( C e. ( Moore ` X ) /\ s e. ~P X ) -> ( ~P s i^i Fin ) C_ ~P X ) |
21 |
|
vpwex |
|- ~P s e. _V |
22 |
21
|
inex1 |
|- ( ~P s i^i Fin ) e. _V |
23 |
22
|
elpw |
|- ( ( ~P s i^i Fin ) e. ~P ~P X <-> ( ~P s i^i Fin ) C_ ~P X ) |
24 |
20 23
|
sylibr |
|- ( ( C e. ( Moore ` X ) /\ s e. ~P X ) -> ( ~P s i^i Fin ) e. ~P ~P X ) |
25 |
24
|
adantlr |
|- ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( ~P s i^i Fin ) e. ~P ~P X ) |
26 |
14 15 25
|
rspcdva |
|- ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( ( toInc ` ( ~P s i^i Fin ) ) e. Dirset -> ( F ` U. ( ~P s i^i Fin ) ) = U. ( F " ( ~P s i^i Fin ) ) ) ) |
27 |
6 26
|
mpd |
|- ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( F ` U. ( ~P s i^i Fin ) ) = U. ( F " ( ~P s i^i Fin ) ) ) |
28 |
3 27
|
eqtr3id |
|- ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) |
29 |
28
|
ralrimiva |
|- ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) -> A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) |
30 |
29
|
ex |
|- ( C e. ( Moore ` X ) -> ( A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) -> A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) ) |
31 |
30
|
imdistani |
|- ( ( 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 ) ) ) ) |