Description: A set strictly dominates iff its cardinal strictly dominates. (Contributed by NM, 30-Oct-2003)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sdomsdomcard | |- ( A ~< B <-> A ~< ( card ` B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relsdom | |- Rel ~< |
|
| 2 | 1 | brrelex2i | |- ( A ~< B -> B e. _V ) |
| 3 | numth3 | |- ( B e. _V -> B e. dom card ) |
|
| 4 | cardid2 | |- ( B e. dom card -> ( card ` B ) ~~ B ) |
|
| 5 | ensym | |- ( ( card ` B ) ~~ B -> B ~~ ( card ` B ) ) |
|
| 6 | 2 3 4 5 | 4syl | |- ( A ~< B -> B ~~ ( card ` B ) ) |
| 7 | sdomentr | |- ( ( A ~< B /\ B ~~ ( card ` B ) ) -> A ~< ( card ` B ) ) |
|
| 8 | 6 7 | mpdan | |- ( A ~< B -> A ~< ( card ` B ) ) |
| 9 | sdomsdomcardi | |- ( A ~< ( card ` B ) -> A ~< B ) |
|
| 10 | 8 9 | impbii | |- ( A ~< B <-> A ~< ( card ` B ) ) |