Step |
Hyp |
Ref |
Expression |
1 |
|
cflem |
|- ( A e. On -> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) |
2 |
|
intexab |
|- ( E. 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 ) |
3 |
1 2
|
sylib |
|- ( 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 ) |
4 |
|
sseq2 |
|- ( v = A -> ( y C_ v <-> y C_ A ) ) |
5 |
|
raleq |
|- ( v = A -> ( A. z e. v E. w e. y z C_ w <-> A. z e. A E. w e. y z C_ w ) ) |
6 |
4 5
|
anbi12d |
|- ( v = A -> ( ( y C_ v /\ A. z e. v E. w e. y z C_ w ) <-> ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) |
7 |
6
|
anbi2d |
|- ( v = A -> ( ( x = ( card ` y ) /\ ( y C_ v /\ A. z e. v E. w e. y z C_ w ) ) <-> ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
8 |
7
|
exbidv |
|- ( v = A -> ( E. y ( x = ( card ` y ) /\ ( y C_ v /\ A. z e. v E. w e. y z C_ w ) ) <-> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
9 |
8
|
abbidv |
|- ( v = A -> { x | E. y ( x = ( card ` y ) /\ ( y C_ v /\ A. z e. v 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 ) ) } ) |
10 |
9
|
inteqd |
|- ( v = A -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ v /\ A. z e. v 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 ) ) } ) |
11 |
|
df-cf |
|- cf = ( v e. On |-> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ v /\ A. z e. v E. w e. y z C_ w ) ) } ) |
12 |
10 11
|
fvmptg |
|- ( ( 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 ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
13 |
3 12
|
mpdan |
|- ( 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 ) ) } ) |