Step |
Hyp |
Ref |
Expression |
1 |
|
cfval |
|- ( A e. On -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
2 |
|
dfss3 |
|- ( A C_ U. y <-> A. z e. A z e. U. y ) |
3 |
|
ssel |
|- ( y C_ A -> ( w e. y -> w e. A ) ) |
4 |
|
onelon |
|- ( ( A e. On /\ w e. A ) -> w e. On ) |
5 |
4
|
ex |
|- ( A e. On -> ( w e. A -> w e. On ) ) |
6 |
3 5
|
sylan9r |
|- ( ( A e. On /\ y C_ A ) -> ( w e. y -> w e. On ) ) |
7 |
|
onelss |
|- ( w e. On -> ( z e. w -> z C_ w ) ) |
8 |
6 7
|
syl6 |
|- ( ( A e. On /\ y C_ A ) -> ( w e. y -> ( z e. w -> z C_ w ) ) ) |
9 |
8
|
imdistand |
|- ( ( A e. On /\ y C_ A ) -> ( ( w e. y /\ z e. w ) -> ( w e. y /\ z C_ w ) ) ) |
10 |
9
|
ancomsd |
|- ( ( A e. On /\ y C_ A ) -> ( ( z e. w /\ w e. y ) -> ( w e. y /\ z C_ w ) ) ) |
11 |
10
|
eximdv |
|- ( ( A e. On /\ y C_ A ) -> ( E. w ( z e. w /\ w e. y ) -> E. w ( w e. y /\ z C_ w ) ) ) |
12 |
|
eluni |
|- ( z e. U. y <-> E. w ( z e. w /\ w e. y ) ) |
13 |
|
df-rex |
|- ( E. w e. y z C_ w <-> E. w ( w e. y /\ z C_ w ) ) |
14 |
11 12 13
|
3imtr4g |
|- ( ( A e. On /\ y C_ A ) -> ( z e. U. y -> E. w e. y z C_ w ) ) |
15 |
14
|
ralimdv |
|- ( ( A e. On /\ y C_ A ) -> ( A. z e. A z e. U. y -> A. z e. A E. w e. y z C_ w ) ) |
16 |
2 15
|
syl5bi |
|- ( ( A e. On /\ y C_ A ) -> ( A C_ U. y -> A. z e. A E. w e. y z C_ w ) ) |
17 |
16
|
imdistanda |
|- ( A e. On -> ( ( y C_ A /\ A C_ U. y ) -> ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) |
18 |
17
|
anim2d |
|- ( A e. On -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) -> ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
19 |
18
|
eximdv |
|- ( A e. On -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) -> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
20 |
19
|
ss2abdv |
|- ( A e. On -> { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
21 |
|
intss |
|- ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } ) |
22 |
20 21
|
syl |
|- ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } ) |
23 |
1 22
|
eqsstrd |
|- ( A e. On -> ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } ) |
24 |
|
cff |
|- cf : On --> On |
25 |
24
|
fdmi |
|- dom cf = On |
26 |
25
|
eleq2i |
|- ( A e. dom cf <-> A e. On ) |
27 |
|
ndmfv |
|- ( -. A e. dom cf -> ( cf ` A ) = (/) ) |
28 |
26 27
|
sylnbir |
|- ( -. A e. On -> ( cf ` A ) = (/) ) |
29 |
|
0ss |
|- (/) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } |
30 |
28 29
|
eqsstrdi |
|- ( -. A e. On -> ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } ) |
31 |
23 30
|
pm2.61i |
|- ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } |