Step |
Hyp |
Ref |
Expression |
1 |
|
acsdrscl.f |
|- F = ( mrCls ` C ) |
2 |
|
simpll |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> C e. ( Moore ` X ) ) |
3 |
|
elpwi |
|- ( t e. ~P ~P X -> t C_ ~P X ) |
4 |
3
|
ad2antrl |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> t C_ ~P X ) |
5 |
1
|
mrcuni |
|- ( ( C e. ( Moore ` X ) /\ t C_ ~P X ) -> ( F ` U. t ) = ( F ` U. ( F " t ) ) ) |
6 |
2 4 5
|
syl2anc |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F ` U. t ) = ( F ` U. ( F " t ) ) ) |
7 |
1
|
mrcf |
|- ( C e. ( Moore ` X ) -> F : ~P X --> C ) |
8 |
7
|
ffnd |
|- ( C e. ( Moore ` X ) -> F Fn ~P X ) |
9 |
8
|
adantr |
|- ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> F Fn ~P X ) |
10 |
|
simpll |
|- ( ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) /\ ( x C_ y /\ y C_ X ) ) -> C e. ( Moore ` X ) ) |
11 |
|
simprl |
|- ( ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) /\ ( x C_ y /\ y C_ X ) ) -> x C_ y ) |
12 |
|
simprr |
|- ( ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) /\ ( x C_ y /\ y C_ X ) ) -> y C_ X ) |
13 |
10 1 11 12
|
mrcssd |
|- ( ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) /\ ( x C_ y /\ y C_ X ) ) -> ( F ` x ) C_ ( F ` y ) ) |
14 |
|
simprr |
|- ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( toInc ` t ) e. Dirset ) |
15 |
3
|
ad2antrl |
|- ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> t C_ ~P X ) |
16 |
1
|
fvexi |
|- F e. _V |
17 |
16
|
imaex |
|- ( F " t ) e. _V |
18 |
17
|
a1i |
|- ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F " t ) e. _V ) |
19 |
9 13 14 15 18
|
ipodrsima |
|- ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( toInc ` ( F " t ) ) e. Dirset ) |
20 |
19
|
adantlr |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( toInc ` ( F " t ) ) e. Dirset ) |
21 |
|
fveq2 |
|- ( s = ( F " t ) -> ( toInc ` s ) = ( toInc ` ( F " t ) ) ) |
22 |
21
|
eleq1d |
|- ( s = ( F " t ) -> ( ( toInc ` s ) e. Dirset <-> ( toInc ` ( F " t ) ) e. Dirset ) ) |
23 |
|
unieq |
|- ( s = ( F " t ) -> U. s = U. ( F " t ) ) |
24 |
23
|
eleq1d |
|- ( s = ( F " t ) -> ( U. s e. C <-> U. ( F " t ) e. C ) ) |
25 |
22 24
|
imbi12d |
|- ( s = ( F " t ) -> ( ( ( toInc ` s ) e. Dirset -> U. s e. C ) <-> ( ( toInc ` ( F " t ) ) e. Dirset -> U. ( F " t ) e. C ) ) ) |
26 |
|
simplr |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) |
27 |
|
imassrn |
|- ( F " t ) C_ ran F |
28 |
7
|
frnd |
|- ( C e. ( Moore ` X ) -> ran F C_ C ) |
29 |
27 28
|
sstrid |
|- ( C e. ( Moore ` X ) -> ( F " t ) C_ C ) |
30 |
17
|
elpw |
|- ( ( F " t ) e. ~P C <-> ( F " t ) C_ C ) |
31 |
29 30
|
sylibr |
|- ( C e. ( Moore ` X ) -> ( F " t ) e. ~P C ) |
32 |
31
|
ad2antrr |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F " t ) e. ~P C ) |
33 |
25 26 32
|
rspcdva |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( ( toInc ` ( F " t ) ) e. Dirset -> U. ( F " t ) e. C ) ) |
34 |
20 33
|
mpd |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> U. ( F " t ) e. C ) |
35 |
1
|
mrcid |
|- ( ( C e. ( Moore ` X ) /\ U. ( F " t ) e. C ) -> ( F ` U. ( F " t ) ) = U. ( F " t ) ) |
36 |
2 34 35
|
syl2anc |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F ` U. ( F " t ) ) = U. ( F " t ) ) |
37 |
6 36
|
eqtrd |
|- ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F ` U. t ) = U. ( F " t ) ) |
38 |
37
|
exp32 |
|- ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) -> ( t e. ~P ~P X -> ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) ) |
39 |
38
|
ralrimiv |
|- ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) -> A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) |
40 |
39
|
ex |
|- ( C e. ( Moore ` X ) -> ( A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) -> A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) ) |
41 |
40
|
imdistani |
|- ( ( 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 ) ) ) ) |