Step |
Hyp |
Ref |
Expression |
1 |
|
compss.a |
|- F = ( x e. ~P A |-> ( A \ x ) ) |
2 |
|
imassrn |
|- ( F " X ) C_ ran F |
3 |
1
|
isf34lem2 |
|- ( A e. V -> F : ~P A --> ~P A ) |
4 |
3
|
adantr |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> F : ~P A --> ~P A ) |
5 |
4
|
frnd |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ran F C_ ~P A ) |
6 |
2 5
|
sstrid |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F " X ) C_ ~P A ) |
7 |
|
simprl |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> X C_ ~P A ) |
8 |
4
|
fdmd |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> dom F = ~P A ) |
9 |
7 8
|
sseqtrrd |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> X C_ dom F ) |
10 |
|
sseqin2 |
|- ( X C_ dom F <-> ( dom F i^i X ) = X ) |
11 |
9 10
|
sylib |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( dom F i^i X ) = X ) |
12 |
|
simprr |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> X =/= (/) ) |
13 |
11 12
|
eqnetrd |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( dom F i^i X ) =/= (/) ) |
14 |
|
imadisj |
|- ( ( F " X ) = (/) <-> ( dom F i^i X ) = (/) ) |
15 |
14
|
necon3bii |
|- ( ( F " X ) =/= (/) <-> ( dom F i^i X ) =/= (/) ) |
16 |
13 15
|
sylibr |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F " X ) =/= (/) ) |
17 |
6 16
|
jca |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( ( F " X ) C_ ~P A /\ ( F " X ) =/= (/) ) ) |
18 |
1
|
isf34lem4 |
|- ( ( A e. V /\ ( ( F " X ) C_ ~P A /\ ( F " X ) =/= (/) ) ) -> ( F ` U. ( F " X ) ) = |^| ( F " ( F " X ) ) ) |
19 |
17 18
|
syldan |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. ( F " X ) ) = |^| ( F " ( F " X ) ) ) |
20 |
1
|
isf34lem3 |
|- ( ( A e. V /\ X C_ ~P A ) -> ( F " ( F " X ) ) = X ) |
21 |
20
|
adantrr |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F " ( F " X ) ) = X ) |
22 |
21
|
inteqd |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> |^| ( F " ( F " X ) ) = |^| X ) |
23 |
19 22
|
eqtrd |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. ( F " X ) ) = |^| X ) |
24 |
23
|
fveq2d |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` ( F ` U. ( F " X ) ) ) = ( F ` |^| X ) ) |
25 |
1
|
compsscnv |
|- `' F = F |
26 |
25
|
fveq1i |
|- ( `' F ` ( F ` U. ( F " X ) ) ) = ( F ` ( F ` U. ( F " X ) ) ) |
27 |
1
|
compssiso |
|- ( A e. V -> F Isom [C.] , `' [C.] ( ~P A , ~P A ) ) |
28 |
|
isof1o |
|- ( F Isom [C.] , `' [C.] ( ~P A , ~P A ) -> F : ~P A -1-1-onto-> ~P A ) |
29 |
27 28
|
syl |
|- ( A e. V -> F : ~P A -1-1-onto-> ~P A ) |
30 |
|
sspwuni |
|- ( ( F " X ) C_ ~P A <-> U. ( F " X ) C_ A ) |
31 |
6 30
|
sylib |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> U. ( F " X ) C_ A ) |
32 |
|
elpw2g |
|- ( A e. V -> ( U. ( F " X ) e. ~P A <-> U. ( F " X ) C_ A ) ) |
33 |
32
|
adantr |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( U. ( F " X ) e. ~P A <-> U. ( F " X ) C_ A ) ) |
34 |
31 33
|
mpbird |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> U. ( F " X ) e. ~P A ) |
35 |
|
f1ocnvfv1 |
|- ( ( F : ~P A -1-1-onto-> ~P A /\ U. ( F " X ) e. ~P A ) -> ( `' F ` ( F ` U. ( F " X ) ) ) = U. ( F " X ) ) |
36 |
29 34 35
|
syl2an2r |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( `' F ` ( F ` U. ( F " X ) ) ) = U. ( F " X ) ) |
37 |
26 36
|
eqtr3id |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` ( F ` U. ( F " X ) ) ) = U. ( F " X ) ) |
38 |
24 37
|
eqtr3d |
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` |^| X ) = U. ( F " X ) ) |