Description: If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | ondomen | |- ( ( A e. On /\ B ~<_ A ) -> B e. dom card ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq2 | |- ( x = A -> ( B ~<_ x <-> B ~<_ A ) ) |
|
2 | 1 | rspcev | |- ( ( A e. On /\ B ~<_ A ) -> E. x e. On B ~<_ x ) |
3 | ac10ct | |- ( E. x e. On B ~<_ x -> E. r r We B ) |
|
4 | 2 3 | syl | |- ( ( A e. On /\ B ~<_ A ) -> E. r r We B ) |
5 | ween | |- ( B e. dom card <-> E. r r We B ) |
|
6 | 4 5 | sylibr | |- ( ( A e. On /\ B ~<_ A ) -> B e. dom card ) |