This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 12-Feb-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cfeq0 | |- ( A e. On -> ( ( cf ` A ) = (/) <-> A = (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cfval | |- ( A e. On -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
|
| 2 | 1 | eqeq1d | |- ( A e. On -> ( ( cf ` A ) = (/) <-> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) ) ) |
| 3 | vex | |- v e. _V |
|
| 4 | eqeq1 | |- ( x = v -> ( x = ( card ` y ) <-> v = ( card ` y ) ) ) |
|
| 5 | 4 | anbi1d | |- ( x = v -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
| 6 | 5 | exbidv | |- ( x = v -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
| 7 | 3 6 | elab | |- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) |
| 8 | fveq2 | |- ( v = ( card ` y ) -> ( card ` v ) = ( card ` ( card ` y ) ) ) |
|
| 9 | cardidm | |- ( card ` ( card ` y ) ) = ( card ` y ) |
|
| 10 | 8 9 | eqtrdi | |- ( v = ( card ` y ) -> ( card ` v ) = ( card ` y ) ) |
| 11 | eqeq2 | |- ( v = ( card ` y ) -> ( ( card ` v ) = v <-> ( card ` v ) = ( card ` y ) ) ) |
|
| 12 | 10 11 | mpbird | |- ( v = ( card ` y ) -> ( card ` v ) = v ) |
| 13 | 12 | adantr | |- ( ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v ) |
| 14 | 13 | exlimiv | |- ( E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v ) |
| 15 | 7 14 | sylbi | |- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> ( card ` v ) = v ) |
| 16 | cardon | |- ( card ` v ) e. On |
|
| 17 | 15 16 | eqeltrrdi | |- ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> v e. On ) |
| 18 | 17 | ssriv | |- { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On |
| 19 | onint0 | |- ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On -> ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) <-> (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) ) |
|
| 20 | 18 19 | ax-mp | |- ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) <-> (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } ) |
| 21 | 0ex | |- (/) e. _V |
|
| 22 | eqeq1 | |- ( x = (/) -> ( x = ( card ` y ) <-> (/) = ( card ` y ) ) ) |
|
| 23 | 22 | anbi1d | |- ( x = (/) -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
| 24 | 23 | exbidv | |- ( x = (/) -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) ) |
| 25 | 21 24 | elab | |- ( (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } <-> E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) |
| 26 | onss | |- ( A e. On -> A C_ On ) |
|
| 27 | sstr | |- ( ( y C_ A /\ A C_ On ) -> y C_ On ) |
|
| 28 | 27 | ancoms | |- ( ( A C_ On /\ y C_ A ) -> y C_ On ) |
| 29 | 26 28 | sylan | |- ( ( A e. On /\ y C_ A ) -> y C_ On ) |
| 30 | 29 | 3adant2 | |- ( ( A e. On /\ (/) = ( card ` y ) /\ y C_ A ) -> y C_ On ) |
| 31 | 30 | 3adant3r | |- ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> y C_ On ) |
| 32 | simp2 | |- ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> (/) = ( card ` y ) ) |
|
| 33 | simp3 | |- ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) |
|
| 34 | eqcom | |- ( (/) = ( card ` y ) <-> ( card ` y ) = (/) ) |
|
| 35 | vex | |- y e. _V |
|
| 36 | onssnum | |- ( ( y e. _V /\ y C_ On ) -> y e. dom card ) |
|
| 37 | 35 36 | mpan | |- ( y C_ On -> y e. dom card ) |
| 38 | cardnueq0 | |- ( y e. dom card -> ( ( card ` y ) = (/) <-> y = (/) ) ) |
|
| 39 | 37 38 | syl | |- ( y C_ On -> ( ( card ` y ) = (/) <-> y = (/) ) ) |
| 40 | 34 39 | bitrid | |- ( y C_ On -> ( (/) = ( card ` y ) <-> y = (/) ) ) |
| 41 | 40 | biimpa | |- ( ( y C_ On /\ (/) = ( card ` y ) ) -> y = (/) ) |
| 42 | sseq1 | |- ( y = (/) -> ( y C_ A <-> (/) C_ A ) ) |
|
| 43 | rexeq | |- ( y = (/) -> ( E. w e. y z C_ w <-> E. w e. (/) z C_ w ) ) |
|
| 44 | 43 | ralbidv | |- ( y = (/) -> ( A. z e. A E. w e. y z C_ w <-> A. z e. A E. w e. (/) z C_ w ) ) |
| 45 | 42 44 | anbi12d | |- ( y = (/) -> ( ( y C_ A /\ A. z e. A E. w e. y z C_ w ) <-> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) ) ) |
| 46 | 45 | biimpa | |- ( ( y = (/) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) ) |
| 47 | 41 46 | sylan | |- ( ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( (/) C_ A /\ A. z e. A E. w e. (/) z C_ w ) ) |
| 48 | rex0 | |- -. E. w e. (/) z C_ w |
|
| 49 | 48 | rgenw | |- A. z e. A -. E. w e. (/) z C_ w |
| 50 | r19.2z | |- ( ( A =/= (/) /\ A. z e. A -. E. w e. (/) z C_ w ) -> E. z e. A -. E. w e. (/) z C_ w ) |
|
| 51 | 49 50 | mpan2 | |- ( A =/= (/) -> E. z e. A -. E. w e. (/) z C_ w ) |
| 52 | rexnal | |- ( E. z e. A -. E. w e. (/) z C_ w <-> -. A. z e. A E. w e. (/) z C_ w ) |
|
| 53 | 51 52 | sylib | |- ( A =/= (/) -> -. A. z e. A E. w e. (/) z C_ w ) |
| 54 | 53 | necon4ai | |- ( A. z e. A E. w e. (/) z C_ w -> A = (/) ) |
| 55 | 47 54 | simpl2im | |- ( ( ( y C_ On /\ (/) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) |
| 56 | 31 32 33 55 | syl21anc | |- ( ( A e. On /\ (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) |
| 57 | 56 | 3expib | |- ( A e. On -> ( ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) ) |
| 58 | 57 | exlimdv | |- ( A e. On -> ( E. y ( (/) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> A = (/) ) ) |
| 59 | 25 58 | biimtrid | |- ( A e. On -> ( (/) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> A = (/) ) ) |
| 60 | 20 59 | biimtrid | |- ( A e. On -> ( |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } = (/) -> A = (/) ) ) |
| 61 | 2 60 | sylbid | |- ( A e. On -> ( ( cf ` A ) = (/) -> A = (/) ) ) |
| 62 | fveq2 | |- ( A = (/) -> ( cf ` A ) = ( cf ` (/) ) ) |
|
| 63 | cf0 | |- ( cf ` (/) ) = (/) |
|
| 64 | 62 63 | eqtrdi | |- ( A = (/) -> ( cf ` A ) = (/) ) |
| 65 | 61 64 | impbid1 | |- ( A e. On -> ( ( cf ` A ) = (/) <-> A = (/) ) ) |