Step |
Hyp |
Ref |
Expression |
1 |
|
pwexg |
|- ( A e. V -> ~P A e. _V ) |
2 |
1
|
adantr |
|- ( ( A e. V /\ B C_ A ) -> ~P A e. _V ) |
3 |
|
inex1g |
|- ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V ) |
4 |
2 3
|
syl |
|- ( ( A e. V /\ B C_ A ) -> ( ~P A i^i Fin ) e. _V ) |
5 |
|
ssexg |
|- ( ( B C_ A /\ A e. V ) -> B e. _V ) |
6 |
5
|
ancoms |
|- ( ( A e. V /\ B C_ A ) -> B e. _V ) |
7 |
|
restval |
|- ( ( ( ~P A i^i Fin ) e. _V /\ B e. _V ) -> ( ( ~P A i^i Fin ) |`t B ) = ran ( x e. ( ~P A i^i Fin ) |-> ( x i^i B ) ) ) |
8 |
4 6 7
|
syl2anc |
|- ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) |`t B ) = ran ( x e. ( ~P A i^i Fin ) |-> ( x i^i B ) ) ) |
9 |
|
inss2 |
|- ( x i^i B ) C_ B |
10 |
9
|
a1i |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P A i^i Fin ) ) -> ( x i^i B ) C_ B ) |
11 |
|
elinel2 |
|- ( x e. ( ~P A i^i Fin ) -> x e. Fin ) |
12 |
11
|
adantl |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin ) |
13 |
|
inss1 |
|- ( x i^i B ) C_ x |
14 |
|
ssfi |
|- ( ( x e. Fin /\ ( x i^i B ) C_ x ) -> ( x i^i B ) e. Fin ) |
15 |
12 13 14
|
sylancl |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P A i^i Fin ) ) -> ( x i^i B ) e. Fin ) |
16 |
|
elfpw |
|- ( ( x i^i B ) e. ( ~P B i^i Fin ) <-> ( ( x i^i B ) C_ B /\ ( x i^i B ) e. Fin ) ) |
17 |
10 15 16
|
sylanbrc |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P A i^i Fin ) ) -> ( x i^i B ) e. ( ~P B i^i Fin ) ) |
18 |
17
|
fmpttd |
|- ( ( A e. V /\ B C_ A ) -> ( x e. ( ~P A i^i Fin ) |-> ( x i^i B ) ) : ( ~P A i^i Fin ) --> ( ~P B i^i Fin ) ) |
19 |
18
|
frnd |
|- ( ( A e. V /\ B C_ A ) -> ran ( x e. ( ~P A i^i Fin ) |-> ( x i^i B ) ) C_ ( ~P B i^i Fin ) ) |
20 |
8 19
|
eqsstrd |
|- ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) |`t B ) C_ ( ~P B i^i Fin ) ) |
21 |
|
elfpw |
|- ( x e. ( ~P B i^i Fin ) <-> ( x C_ B /\ x e. Fin ) ) |
22 |
21
|
simplbi |
|- ( x e. ( ~P B i^i Fin ) -> x C_ B ) |
23 |
22
|
adantl |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x C_ B ) |
24 |
|
df-ss |
|- ( x C_ B <-> ( x i^i B ) = x ) |
25 |
23 24
|
sylib |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> ( x i^i B ) = x ) |
26 |
4
|
adantr |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> ( ~P A i^i Fin ) e. _V ) |
27 |
6
|
adantr |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> B e. _V ) |
28 |
|
simplr |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> B C_ A ) |
29 |
23 28
|
sstrd |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x C_ A ) |
30 |
|
elinel2 |
|- ( x e. ( ~P B i^i Fin ) -> x e. Fin ) |
31 |
30
|
adantl |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x e. Fin ) |
32 |
|
elfpw |
|- ( x e. ( ~P A i^i Fin ) <-> ( x C_ A /\ x e. Fin ) ) |
33 |
29 31 32
|
sylanbrc |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x e. ( ~P A i^i Fin ) ) |
34 |
|
elrestr |
|- ( ( ( ~P A i^i Fin ) e. _V /\ B e. _V /\ x e. ( ~P A i^i Fin ) ) -> ( x i^i B ) e. ( ( ~P A i^i Fin ) |`t B ) ) |
35 |
26 27 33 34
|
syl3anc |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> ( x i^i B ) e. ( ( ~P A i^i Fin ) |`t B ) ) |
36 |
25 35
|
eqeltrrd |
|- ( ( ( A e. V /\ B C_ A ) /\ x e. ( ~P B i^i Fin ) ) -> x e. ( ( ~P A i^i Fin ) |`t B ) ) |
37 |
20 36
|
eqelssd |
|- ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) |`t B ) = ( ~P B i^i Fin ) ) |