Description: When assuming AC, weak and usual dominance coincide. It is not known if this is an AC equivalent. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wdomac | |- ( X ~<_* Y <-> X ~<_ Y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relwdom | |- Rel ~<_* |
|
| 2 | 1 | brrelex2i | |- ( X ~<_* Y -> Y e. _V ) |
| 3 | reldom | |- Rel ~<_ |
|
| 4 | 3 | brrelex2i | |- ( X ~<_ Y -> Y e. _V ) |
| 5 | numth3 | |- ( Y e. _V -> Y e. dom card ) |
|
| 6 | wdomnumr | |- ( Y e. dom card -> ( X ~<_* Y <-> X ~<_ Y ) ) |
|
| 7 | 5 6 | syl | |- ( Y e. _V -> ( X ~<_* Y <-> X ~<_ Y ) ) |
| 8 | 2 4 7 | pm5.21nii | |- ( X ~<_* Y <-> X ~<_ Y ) |