| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-fi |
|- fi = ( z e. _V |-> { y | E. x e. ( ~P z i^i Fin ) y = |^| x } ) |
| 2 |
|
pweq |
|- ( z = A -> ~P z = ~P A ) |
| 3 |
2
|
ineq1d |
|- ( z = A -> ( ~P z i^i Fin ) = ( ~P A i^i Fin ) ) |
| 4 |
3
|
rexeqdv |
|- ( z = A -> ( E. x e. ( ~P z i^i Fin ) y = |^| x <-> E. x e. ( ~P A i^i Fin ) y = |^| x ) ) |
| 5 |
4
|
abbidv |
|- ( z = A -> { y | E. x e. ( ~P z i^i Fin ) y = |^| x } = { y | E. x e. ( ~P A i^i Fin ) y = |^| x } ) |
| 6 |
|
elex |
|- ( A e. V -> A e. _V ) |
| 7 |
|
simpr |
|- ( ( x e. ( ~P A i^i Fin ) /\ y = |^| x ) -> y = |^| x ) |
| 8 |
|
elinel1 |
|- ( x e. ( ~P A i^i Fin ) -> x e. ~P A ) |
| 9 |
8
|
elpwid |
|- ( x e. ( ~P A i^i Fin ) -> x C_ A ) |
| 10 |
|
eqvisset |
|- ( y = |^| x -> |^| x e. _V ) |
| 11 |
|
intex |
|- ( x =/= (/) <-> |^| x e. _V ) |
| 12 |
10 11
|
sylibr |
|- ( y = |^| x -> x =/= (/) ) |
| 13 |
|
intssuni2 |
|- ( ( x C_ A /\ x =/= (/) ) -> |^| x C_ U. A ) |
| 14 |
9 12 13
|
syl2an |
|- ( ( x e. ( ~P A i^i Fin ) /\ y = |^| x ) -> |^| x C_ U. A ) |
| 15 |
7 14
|
eqsstrd |
|- ( ( x e. ( ~P A i^i Fin ) /\ y = |^| x ) -> y C_ U. A ) |
| 16 |
|
velpw |
|- ( y e. ~P U. A <-> y C_ U. A ) |
| 17 |
15 16
|
sylibr |
|- ( ( x e. ( ~P A i^i Fin ) /\ y = |^| x ) -> y e. ~P U. A ) |
| 18 |
17
|
rexlimiva |
|- ( E. x e. ( ~P A i^i Fin ) y = |^| x -> y e. ~P U. A ) |
| 19 |
18
|
abssi |
|- { y | E. x e. ( ~P A i^i Fin ) y = |^| x } C_ ~P U. A |
| 20 |
|
uniexg |
|- ( A e. V -> U. A e. _V ) |
| 21 |
20
|
pwexd |
|- ( A e. V -> ~P U. A e. _V ) |
| 22 |
|
ssexg |
|- ( ( { y | E. x e. ( ~P A i^i Fin ) y = |^| x } C_ ~P U. A /\ ~P U. A e. _V ) -> { y | E. x e. ( ~P A i^i Fin ) y = |^| x } e. _V ) |
| 23 |
19 21 22
|
sylancr |
|- ( A e. V -> { y | E. x e. ( ~P A i^i Fin ) y = |^| x } e. _V ) |
| 24 |
1 5 6 23
|
fvmptd3 |
|- ( A e. V -> ( fi ` A ) = { y | E. x e. ( ~P A i^i Fin ) y = |^| x } ) |