| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ordom |
|- Ord _om |
| 2 |
|
reldom |
|- Rel ~<_ |
| 3 |
2
|
brrelex2i |
|- ( B ~<_ _om -> _om e. _V ) |
| 4 |
|
elong |
|- ( _om e. _V -> ( _om e. On <-> Ord _om ) ) |
| 5 |
3 4
|
syl |
|- ( B ~<_ _om -> ( _om e. On <-> Ord _om ) ) |
| 6 |
1 5
|
mpbiri |
|- ( B ~<_ _om -> _om e. On ) |
| 7 |
|
ondomen |
|- ( ( _om e. On /\ B ~<_ _om ) -> B e. dom card ) |
| 8 |
6 7
|
mpancom |
|- ( B ~<_ _om -> B e. dom card ) |
| 9 |
|
eqid |
|- ( x e. B |-> C ) = ( x e. B |-> C ) |
| 10 |
9
|
dmmptss |
|- dom ( x e. B |-> C ) C_ B |
| 11 |
|
ssnum |
|- ( ( B e. dom card /\ dom ( x e. B |-> C ) C_ B ) -> dom ( x e. B |-> C ) e. dom card ) |
| 12 |
8 10 11
|
sylancl |
|- ( B ~<_ _om -> dom ( x e. B |-> C ) e. dom card ) |
| 13 |
|
funmpt |
|- Fun ( x e. B |-> C ) |
| 14 |
|
funforn |
|- ( Fun ( x e. B |-> C ) <-> ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C ) ) |
| 15 |
13 14
|
mpbi |
|- ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C ) |
| 16 |
|
fodomnum |
|- ( dom ( x e. B |-> C ) e. dom card -> ( ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C ) -> ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) ) ) |
| 17 |
12 15 16
|
mpisyl |
|- ( B ~<_ _om -> ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) ) |
| 18 |
|
ctex |
|- ( B ~<_ _om -> B e. _V ) |
| 19 |
|
ssdomg |
|- ( B e. _V -> ( dom ( x e. B |-> C ) C_ B -> dom ( x e. B |-> C ) ~<_ B ) ) |
| 20 |
18 10 19
|
mpisyl |
|- ( B ~<_ _om -> dom ( x e. B |-> C ) ~<_ B ) |
| 21 |
|
domtr |
|- ( ( dom ( x e. B |-> C ) ~<_ B /\ B ~<_ _om ) -> dom ( x e. B |-> C ) ~<_ _om ) |
| 22 |
20 21
|
mpancom |
|- ( B ~<_ _om -> dom ( x e. B |-> C ) ~<_ _om ) |
| 23 |
|
domtr |
|- ( ( ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) /\ dom ( x e. B |-> C ) ~<_ _om ) -> ran ( x e. B |-> C ) ~<_ _om ) |
| 24 |
17 22 23
|
syl2anc |
|- ( B ~<_ _om -> ran ( x e. B |-> C ) ~<_ _om ) |