Step |
Hyp |
Ref |
Expression |
1 |
|
ssrab2 |
|- { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } C_ ~P X |
2 |
1
|
a1i |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } C_ ~P X ) |
3 |
|
pweq |
|- ( s = ( X i^i |^| t ) -> ~P s = ~P ( X i^i |^| t ) ) |
4 |
3
|
ineq1d |
|- ( s = ( X i^i |^| t ) -> ( ~P s i^i Fin ) = ( ~P ( X i^i |^| t ) i^i Fin ) ) |
5 |
4
|
imaeq2d |
|- ( s = ( X i^i |^| t ) -> ( F " ( ~P s i^i Fin ) ) = ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) ) |
6 |
5
|
unieqd |
|- ( s = ( X i^i |^| t ) -> U. ( F " ( ~P s i^i Fin ) ) = U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) ) |
7 |
|
id |
|- ( s = ( X i^i |^| t ) -> s = ( X i^i |^| t ) ) |
8 |
6 7
|
sseq12d |
|- ( s = ( X i^i |^| t ) -> ( U. ( F " ( ~P s i^i Fin ) ) C_ s <-> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ( X i^i |^| t ) ) ) |
9 |
|
inss1 |
|- ( X i^i |^| t ) C_ X |
10 |
|
elpw2g |
|- ( X e. V -> ( ( X i^i |^| t ) e. ~P X <-> ( X i^i |^| t ) C_ X ) ) |
11 |
9 10
|
mpbiri |
|- ( X e. V -> ( X i^i |^| t ) e. ~P X ) |
12 |
11
|
ad2antrr |
|- ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> ( X i^i |^| t ) e. ~P X ) |
13 |
|
imassrn |
|- ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ran F |
14 |
|
frn |
|- ( F : ~P X --> ~P X -> ran F C_ ~P X ) |
15 |
14
|
adantl |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> ran F C_ ~P X ) |
16 |
13 15
|
sstrid |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ~P X ) |
17 |
16
|
unissd |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ U. ~P X ) |
18 |
|
unipw |
|- U. ~P X = X |
19 |
17 18
|
sseqtrdi |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ X ) |
20 |
19
|
adantr |
|- ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ X ) |
21 |
|
inss2 |
|- ( X i^i |^| t ) C_ |^| t |
22 |
|
intss1 |
|- ( a e. t -> |^| t C_ a ) |
23 |
21 22
|
sstrid |
|- ( a e. t -> ( X i^i |^| t ) C_ a ) |
24 |
23
|
adantl |
|- ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> ( X i^i |^| t ) C_ a ) |
25 |
24
|
sspwd |
|- ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> ~P ( X i^i |^| t ) C_ ~P a ) |
26 |
25
|
ssrind |
|- ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> ( ~P ( X i^i |^| t ) i^i Fin ) C_ ( ~P a i^i Fin ) ) |
27 |
|
imass2 |
|- ( ( ~P ( X i^i |^| t ) i^i Fin ) C_ ( ~P a i^i Fin ) -> ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ( F " ( ~P a i^i Fin ) ) ) |
28 |
26 27
|
syl |
|- ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ( F " ( ~P a i^i Fin ) ) ) |
29 |
28
|
unissd |
|- ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ U. ( F " ( ~P a i^i Fin ) ) ) |
30 |
|
ssel2 |
|- ( ( t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } /\ a e. t ) -> a e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) |
31 |
|
pweq |
|- ( s = a -> ~P s = ~P a ) |
32 |
31
|
ineq1d |
|- ( s = a -> ( ~P s i^i Fin ) = ( ~P a i^i Fin ) ) |
33 |
32
|
imaeq2d |
|- ( s = a -> ( F " ( ~P s i^i Fin ) ) = ( F " ( ~P a i^i Fin ) ) ) |
34 |
33
|
unieqd |
|- ( s = a -> U. ( F " ( ~P s i^i Fin ) ) = U. ( F " ( ~P a i^i Fin ) ) ) |
35 |
|
id |
|- ( s = a -> s = a ) |
36 |
34 35
|
sseq12d |
|- ( s = a -> ( U. ( F " ( ~P s i^i Fin ) ) C_ s <-> U. ( F " ( ~P a i^i Fin ) ) C_ a ) ) |
37 |
36
|
elrab |
|- ( a e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> ( a e. ~P X /\ U. ( F " ( ~P a i^i Fin ) ) C_ a ) ) |
38 |
37
|
simprbi |
|- ( a e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } -> U. ( F " ( ~P a i^i Fin ) ) C_ a ) |
39 |
30 38
|
syl |
|- ( ( t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } /\ a e. t ) -> U. ( F " ( ~P a i^i Fin ) ) C_ a ) |
40 |
39
|
adantll |
|- ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> U. ( F " ( ~P a i^i Fin ) ) C_ a ) |
41 |
29 40
|
sstrd |
|- ( ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) /\ a e. t ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ a ) |
42 |
41
|
ralrimiva |
|- ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> A. a e. t U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ a ) |
43 |
|
ssint |
|- ( U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ |^| t <-> A. a e. t U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ a ) |
44 |
42 43
|
sylibr |
|- ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ |^| t ) |
45 |
20 44
|
ssind |
|- ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> U. ( F " ( ~P ( X i^i |^| t ) i^i Fin ) ) C_ ( X i^i |^| t ) ) |
46 |
8 12 45
|
elrabd |
|- ( ( ( X e. V /\ F : ~P X --> ~P X ) /\ t C_ { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) -> ( X i^i |^| t ) e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } ) |
47 |
2 46
|
ismred2 |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( Moore ` X ) ) |
48 |
|
fssxp |
|- ( F : ~P X --> ~P X -> F C_ ( ~P X X. ~P X ) ) |
49 |
|
pwexg |
|- ( X e. V -> ~P X e. _V ) |
50 |
49 49
|
xpexd |
|- ( X e. V -> ( ~P X X. ~P X ) e. _V ) |
51 |
|
ssexg |
|- ( ( F C_ ( ~P X X. ~P X ) /\ ( ~P X X. ~P X ) e. _V ) -> F e. _V ) |
52 |
48 50 51
|
syl2anr |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> F e. _V ) |
53 |
|
simpr |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> F : ~P X --> ~P X ) |
54 |
|
pweq |
|- ( s = t -> ~P s = ~P t ) |
55 |
54
|
ineq1d |
|- ( s = t -> ( ~P s i^i Fin ) = ( ~P t i^i Fin ) ) |
56 |
55
|
imaeq2d |
|- ( s = t -> ( F " ( ~P s i^i Fin ) ) = ( F " ( ~P t i^i Fin ) ) ) |
57 |
56
|
unieqd |
|- ( s = t -> U. ( F " ( ~P s i^i Fin ) ) = U. ( F " ( ~P t i^i Fin ) ) ) |
58 |
|
id |
|- ( s = t -> s = t ) |
59 |
57 58
|
sseq12d |
|- ( s = t -> ( U. ( F " ( ~P s i^i Fin ) ) C_ s <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) |
60 |
59
|
elrab3 |
|- ( t e. ~P X -> ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) |
61 |
60
|
rgen |
|- A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) |
62 |
53 61
|
jctir |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> ( F : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) ) |
63 |
|
feq1 |
|- ( f = F -> ( f : ~P X --> ~P X <-> F : ~P X --> ~P X ) ) |
64 |
|
imaeq1 |
|- ( f = F -> ( f " ( ~P t i^i Fin ) ) = ( F " ( ~P t i^i Fin ) ) ) |
65 |
64
|
unieqd |
|- ( f = F -> U. ( f " ( ~P t i^i Fin ) ) = U. ( F " ( ~P t i^i Fin ) ) ) |
66 |
65
|
sseq1d |
|- ( f = F -> ( U. ( f " ( ~P t i^i Fin ) ) C_ t <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) |
67 |
66
|
bibi2d |
|- ( f = F -> ( ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) <-> ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) ) |
68 |
67
|
ralbidv |
|- ( f = F -> ( A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) <-> A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) ) |
69 |
63 68
|
anbi12d |
|- ( f = F -> ( ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) <-> ( F : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( F " ( ~P t i^i Fin ) ) C_ t ) ) ) ) |
70 |
52 62 69
|
spcedv |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) ) |
71 |
|
isacs |
|- ( { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( ACS ` X ) <-> ( { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( Moore ` X ) /\ E. f ( f : ~P X --> ~P X /\ A. t e. ~P X ( t e. { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } <-> U. ( f " ( ~P t i^i Fin ) ) C_ t ) ) ) ) |
72 |
47 70 71
|
sylanbrc |
|- ( ( X e. V /\ F : ~P X --> ~P X ) -> { s e. ~P X | U. ( F " ( ~P s i^i Fin ) ) C_ s } e. ( ACS ` X ) ) |