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 4803).
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 4697 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 4372 |
. . . . . . 7
|
| 3 | breq1 2612 |
. . . . . . . 8
| |
| 4 | 1, 3 | cla4ev 1860 |
. . . . . . 7
 |
| 5 | 2, 4 | ax-mp 7 |
. . . . . 6
|
| 6 | abn0 2280 |
. . . . . 6
  | |
| 7 | 5, 6 | mpbir 190 |
. . . . 5
|
| 8 | scott0 4689 |
. . . . . 6
| |
| 9 | 8 | necon3bii 1590 |
. . . . 5
|
| 10 | 7, 9 | mpbi 189 |
. . . 4
|
| 11 | rabn0 2282 |
. . . 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 1480 |
. . . . . . . . . . 11
|
| 18 | eq2ab 1565 |
. . . . . . . . . . 11
| |
| 19 | 17, 18 | bitr 173 |
. . . . . . . . . 10
|
| 20 | breq1 2612 |
. . . . . . . . . . . . 13
| |
| 21 | fveq2 3709 |
. . . . . . . . . . . . . . . 16
| |
| 22 | 21 | sseq1d 2078 |
. . . . . . . . . . . . . . 15
|
| 23 | 22 | imbi2d 610 |
. . . . . . . . . . . . . 14
|
| 24 | 23 | albidv 1273 |
. . . . . . . . . . . . 13
|
| 25 | 20, 24 | anbi12d 626 |
. . . . . . . . . . . 12
|
| 26 | breq1 2612 |
. . . . . . . . . . . . 13
| |
| 27 | 22 | imbi2d 610 |
. . . . . . . . . . . . . 14
|
| 28 | 27 | albidv 1273 |
. . . . . . . . . . . . 13
|
| 29 | 26, 28 | anbi12d 626 |
. . . . . . . . . . . 12
|
| 30 | 25, 29 | bibi12d 627 |
. . . . . . . . . . 11
|
| 31 | 30 | a4v 1267 |
. . . . . . . . . 10
|
| 32 | 19, 31 | sylbi 199 |
. . . . . . . . 9
|
| 33 | pm3.26 319 |
. . . . . . . . 9
| |
| 34 | 32, 33 | syl6bi 214 |
. . . . . . . 8
|
| 35 | 14, 34 | jcad 598 |
. . . . . . 7
|
| 36 | entrt 4395 |
. . . . . . . 8
| |
| 37 | 1 | ensym 4393 |
. . . . . . . 8
|
| 38 | 36, 37 | sylan 448 |
. . . . . . 7
|
| 39 | 35, 38 | syl6 22 |
. . . . . 6
|
| 40 | visset 1804 |
. . . . . . . 8
| |
| 41 | breq1 2612 |
. . . . . . . 8
| |
| 42 | 40, 41 | elab 1888 |
. . . . . . 7
|
| 43 | df-ral 1641 |
. . . . . . . 8
| |
| 44 | visset 1804 |
. . . . . . . . . . 11
| |
| 45 | breq1 2612 |
. . . . . . . . . . 11
| |
| 46 | 44, 45 | elab 1888 |
. . . . . . . . . 10
|
| 47 | 46 | imbi1i 186 |
. . . . . . . . 9
|
| 48 | 47 | albii 996 |
. . . . . . . 8
|
| 49 | 43, 48 | bitr 173 |
. . . . . . 7
|
| 50 | 42, 49 | anbi12i 481 |
. . . . . 6
|
| 51 | 39, 50 | syl5ib 206 |
. . . . 5
|