HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
Description: If we allow the Axiom of
Regularity, we can avoid the Axiom of Choice by
defining the cardinal number of a set as the set of all sets
equinumerous to it and having least possible rank. This theorem proves
the equinumerosity relationship for this definition (compare carden 4831).
The hypotheses correspond to the definition of kard of [Enderton] p. 222
(which we don't define separately since currently we do not use it
elsewhere). This theorem along with kardex 4725 justify the definition of
kard. The restriction to least rank prevents the proper class that
would result from       . |
| Ref | Expression |
|---|---|
| karden.1 |
   |
| karden.2 |
 |
| karden.3 |
           |
| karden.4 |
 |
| Ref | Expression |
|---|---|
| karden |
 |
,, ,,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | karden.1 |
. . . . . . . 8
| |
| 2 | 1 | enref 4391 |
. . . . . . 7
|
| 3 | breq1 2622 |
. . . . . . . 8
| |
| 4 | 1, 3 | cla4ev 1869 |
. . . . . . 7
 |
| 5 | 2, 4 | ax-mp 7 |
. . . . . 6
|
| 6 | abn0 2290 |
. . . . . 6
  | |
| 7 | 5, 6 | mpbir 190 |
. . . . 5
|
| 8 | scott0 4717 |
. . . . . 6
| |
| 9 | 8 | necon3bii 1598 |
. . . . 5
|
| 10 | 7, 9 | mpbi 189 |
. . . 4
|
| 11 | rabn0 2292 |
. . . 4
| |
| 12 | 10, 11 | mpbi 189 |
. . 3
|
| 13 | pm3.26 319 |
. . . . . . . . 9
| |
| 14 | 13 | a1i 8 |
. . . . . . . 8
|
| 15 | karden.3 |
. . . . . . . . . . . 12
| |
| 16 | karden.4 |
. . . . . . . . . . . 12
| |
| 17 | 15, 16 | eqeq12i 1488 |
. . . . . . . . . . 11
|
| 18 | eq2ab 1573 |
. . . . . . . . . . 11
| |
| 19 | 17, 18 | bitr 173 |
. . . . . . . . . 10
|
| 20 | breq1 2622 |
. . . . . . . . . . . . 13
| |
| 21 | fveq2 3724 |
. . . . . . . . . . . . . . . 16
| |
| 22 | 21 | sseq1d 2088 |
. . . . . . . . . . . . . . 15
|
| 23 | 22 | imbi2d 612 |
. . . . . . . . . . . . . 14
|
| 24 | 23 | albidv 1278 |
. . . . . . . . . . . . 13
|
| 25 | 20, 24 | anbi12d 628 |
. . . . . . . . . . . 12
|
| 26 | breq1 2622 |
. . . . . . . . . . . . 13
| |
| 27 | 22 | imbi2d 612 |
. . . . . . . . . . . . . 14
|
| 28 | 27 | albidv 1278 |
. . . . . . . . . . . . 13
|
| 29 | 26, 28 | anbi12d 628 |
. . . . . . . . . . . 12
|
| 30 | 25, 29 | bibi12d 629 |
. . . . . . . . . . 11
|
| 31 | 30 | a4v 1272 |
. . . . . . . . . 10
|
| 32 | 19, 31 | sylbi 199 |
. . . . . . . . 9
|
| 33 | pm3.26 319 |
. . . . . . . . 9
| |
| 34 | 32, 33 | syl6bi 214 |
. . . . . . . 8
|
| 35 | 14, 34 | jcad 600 |
. . . . . . 7
|
| 36 | entrt 4414 |
. . . . . . . 8
| |
| 37 | 1 | ensym 4412 |
. . . . . . . 8
|
| 38 | 36, 37 | sylan 448 |
. . . . . . 7
|
| 39 | 35, 38 | syl6 22 |
. . . . . 6
|
| 40 | visset 1813 |
. . . . . . . 8
| |
| 41 | breq1 2622 |
. . . . . . . 8
| |
| 42 | 40, 41 | elab 1897 |
. . . . . . 7
|
| 43 | df-ral 1649 |
. . . . . . . 8
| |
| 44 | visset 1813 |
. . . . . . . . . . 11
| |
| 45 | breq1 2622 |
. . . . . . . . . . 11
| |
| 46 | 44, 45 | elab 1897 |
. . . . . . . . . 10
|
| 47 | 46 | imbi1i 186 |
. . . . . . . . 9
|
| 48 | 47 | albii 999 |
. . . . . . . 8
|
| 49 | 43, 48 | bitr 173 |
. . . . . . 7
|
| 50 | 42, 49 | anbi12i 482 |
. . . . . 6
|
| 51 | 39, 50 | syl5ib 206 |
. . . . 5
|