Description: A version of fodom that doesn't require the Axiom of Choice ax-ac . (Contributed by Mario Carneiro, 28-Feb-2013) (Revised by Mario Carneiro, 28-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fodomnum | |- ( A e. dom card -> ( F : A -onto-> B -> B ~<_ A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fornex | |- ( A e. dom card -> ( F : A -onto-> B -> B e. _V ) ) |
|
| 2 | 1 | com12 | |- ( F : A -onto-> B -> ( A e. dom card -> B e. _V ) ) |
| 3 | numacn | |- ( B e. _V -> ( A e. dom card -> A e. AC_ B ) ) |
|
| 4 | 2 3 | syli | |- ( F : A -onto-> B -> ( A e. dom card -> A e. AC_ B ) ) |
| 5 | 4 | com12 | |- ( A e. dom card -> ( F : A -onto-> B -> A e. AC_ B ) ) |
| 6 | fodomacn | |- ( A e. AC_ B -> ( F : A -onto-> B -> B ~<_ A ) ) |
|
| 7 | 5 6 | syli | |- ( A e. dom card -> ( F : A -onto-> B -> B ~<_ A ) ) |