Description: Shorter proof of fineqvac using ax-rep and ax-pow . (Contributed by BTernaryTau, 21-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fineqvacALT | |- ( Fin = _V -> CHOICE ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssv | |- dom card C_ _V |
|
| 2 | 1 | a1i | |- ( Fin = _V -> dom card C_ _V ) |
| 3 | finnum | |- ( x e. Fin -> x e. dom card ) |
|
| 4 | 3 | ssriv | |- Fin C_ dom card |
| 5 | sseq1 | |- ( Fin = _V -> ( Fin C_ dom card <-> _V C_ dom card ) ) |
|
| 6 | 4 5 | mpbii | |- ( Fin = _V -> _V C_ dom card ) |
| 7 | 2 6 | eqssd | |- ( Fin = _V -> dom card = _V ) |
| 8 | dfac10 | |- ( CHOICE <-> dom card = _V ) |
|
| 9 | 7 8 | sylibr | |- ( Fin = _V -> CHOICE ) |