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 |
|
vex |
|- v e. _V |
3 |
|
eqeq1 |
|- ( x = v -> ( x = ( card ` y ) <-> v = ( card ` y ) ) ) |
4 |
3
|
anbi1d |
|- ( x = v -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
5 |
4
|
exbidv |
|- ( x = v -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
6 |
2 5
|
elab |
|- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) |
7 |
|
fveq2 |
|- ( v = ( card ` y ) -> ( card ` v ) = ( card ` ( card ` y ) ) ) |
8 |
|
cardidm |
|- ( card ` ( card ` y ) ) = ( card ` y ) |
9 |
7 8
|
eqtrdi |
|- ( v = ( card ` y ) -> ( card ` v ) = ( card ` y ) ) |
10 |
|
eqeq2 |
|- ( v = ( card ` y ) -> ( ( card ` v ) = v <-> ( card ` v ) = ( card ` y ) ) ) |
11 |
9 10
|
mpbird |
|- ( v = ( card ` y ) -> ( card ` v ) = v ) |
12 |
11
|
adantr |
|- ( ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v ) |
13 |
12
|
exlimiv |
|- ( E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v ) |
14 |
6 13
|
sylbi |
|- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> ( card ` v ) = v ) |
15 |
|
cardon |
|- ( card ` v ) e. On |
16 |
14 15
|
eqeltrrdi |
|- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> v e. On ) |
17 |
16
|
ssriv |
|- { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On |
18 |
|
fvex |
|- ( cf ` A ) e. _V |
19 |
1 18
|
eqeltrrdi |
|- ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } e. _V ) |
20 |
|
intex |
|- ( { 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 ) ) } e. _V ) |
21 |
19 20
|
sylibr |
|- ( A e. On -> { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } =/= (/) ) |
22 |
|
onint |
|- ( ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On /\ { 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 ) ) } e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
23 |
17 21 22
|
sylancr |
|- ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
24 |
1 23
|
eqeltrd |
|- ( A e. On -> ( cf ` A ) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
25 |
|
fveq2 |
|- ( v = ( cf ` A ) -> ( card ` v ) = ( card ` ( cf ` A ) ) ) |
26 |
|
id |
|- ( v = ( cf ` A ) -> v = ( cf ` A ) ) |
27 |
25 26
|
eqeq12d |
|- ( v = ( cf ` A ) -> ( ( card ` v ) = v <-> ( card ` ( cf ` A ) ) = ( cf ` A ) ) ) |
28 |
27 14
|
vtoclga |
|- ( ( cf ` A ) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> ( card ` ( cf ` A ) ) = ( cf ` A ) ) |
29 |
24 28
|
syl |
|- ( A e. On -> ( card ` ( cf ` A ) ) = ( cf ` A ) ) |
30 |
|
cff |
|- cf : On --> On |
31 |
30
|
fdmi |
|- dom cf = On |
32 |
31
|
eleq2i |
|- ( A e. dom cf <-> A e. On ) |
33 |
|
ndmfv |
|- ( -. A e. dom cf -> ( cf ` A ) = (/) ) |
34 |
32 33
|
sylnbir |
|- ( -. A e. On -> ( cf ` A ) = (/) ) |
35 |
|
card0 |
|- ( card ` (/) ) = (/) |
36 |
|
fveq2 |
|- ( ( cf ` A ) = (/) -> ( card ` ( cf ` A ) ) = ( card ` (/) ) ) |
37 |
|
id |
|- ( ( cf ` A ) = (/) -> ( cf ` A ) = (/) ) |
38 |
35 36 37
|
3eqtr4a |
|- ( ( cf ` A ) = (/) -> ( card ` ( cf ` A ) ) = ( cf ` A ) ) |
39 |
34 38
|
syl |
|- ( -. A e. On -> ( card ` ( cf ` A ) ) = ( cf ` A ) ) |
40 |
29 39
|
pm2.61i |
|- ( card ` ( cf ` A ) ) = ( cf ` A ) |