Description: The Principle of Transfinite Induction. Theorem 7.17 of TakeutiZaring p. 39. This principle states that if A is a class of ordinal numbers with the property that every ordinal number included in A also belongs to A , then every ordinal number is in A .
See Theorem tfindes or tfinds for the version involving basis and induction hypotheses. (Contributed by NM, 18-Feb-2004)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tfi | |- ( ( A C_ On /\ A. x e. On ( x C_ A -> x e. A ) ) -> A = On ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldifn | |- ( x e. ( On \ A ) -> -. x e. A ) |
|
| 2 | 1 | adantl | |- ( ( ( x e. On -> ( x C_ A -> x e. A ) ) /\ x e. ( On \ A ) ) -> -. x e. A ) |
| 3 | onss | |- ( x e. On -> x C_ On ) |
|
| 4 | difin0ss | |- ( ( ( On \ A ) i^i x ) = (/) -> ( x C_ On -> x C_ A ) ) |
|
| 5 | 3 4 | syl5com | |- ( x e. On -> ( ( ( On \ A ) i^i x ) = (/) -> x C_ A ) ) |
| 6 | 5 | imim1d | |- ( x e. On -> ( ( x C_ A -> x e. A ) -> ( ( ( On \ A ) i^i x ) = (/) -> x e. A ) ) ) |
| 7 | 6 | a2i | |- ( ( x e. On -> ( x C_ A -> x e. A ) ) -> ( x e. On -> ( ( ( On \ A ) i^i x ) = (/) -> x e. A ) ) ) |
| 8 | eldifi | |- ( x e. ( On \ A ) -> x e. On ) |
|
| 9 | 7 8 | impel | |- ( ( ( x e. On -> ( x C_ A -> x e. A ) ) /\ x e. ( On \ A ) ) -> ( ( ( On \ A ) i^i x ) = (/) -> x e. A ) ) |
| 10 | 2 9 | mtod | |- ( ( ( x e. On -> ( x C_ A -> x e. A ) ) /\ x e. ( On \ A ) ) -> -. ( ( On \ A ) i^i x ) = (/) ) |
| 11 | 10 | ex | |- ( ( x e. On -> ( x C_ A -> x e. A ) ) -> ( x e. ( On \ A ) -> -. ( ( On \ A ) i^i x ) = (/) ) ) |
| 12 | 11 | ralimi2 | |- ( A. x e. On ( x C_ A -> x e. A ) -> A. x e. ( On \ A ) -. ( ( On \ A ) i^i x ) = (/) ) |
| 13 | ralnex | |- ( A. x e. ( On \ A ) -. ( ( On \ A ) i^i x ) = (/) <-> -. E. x e. ( On \ A ) ( ( On \ A ) i^i x ) = (/) ) |
|
| 14 | 12 13 | sylib | |- ( A. x e. On ( x C_ A -> x e. A ) -> -. E. x e. ( On \ A ) ( ( On \ A ) i^i x ) = (/) ) |
| 15 | ssdif0 | |- ( On C_ A <-> ( On \ A ) = (/) ) |
|
| 16 | 15 | necon3bbii | |- ( -. On C_ A <-> ( On \ A ) =/= (/) ) |
| 17 | ordon | |- Ord On |
|
| 18 | difss | |- ( On \ A ) C_ On |
|
| 19 | tz7.5 | |- ( ( Ord On /\ ( On \ A ) C_ On /\ ( On \ A ) =/= (/) ) -> E. x e. ( On \ A ) ( ( On \ A ) i^i x ) = (/) ) |
|
| 20 | 17 18 19 | mp3an12 | |- ( ( On \ A ) =/= (/) -> E. x e. ( On \ A ) ( ( On \ A ) i^i x ) = (/) ) |
| 21 | 16 20 | sylbi | |- ( -. On C_ A -> E. x e. ( On \ A ) ( ( On \ A ) i^i x ) = (/) ) |
| 22 | 14 21 | nsyl2 | |- ( A. x e. On ( x C_ A -> x e. A ) -> On C_ A ) |
| 23 | 22 | anim2i | |- ( ( A C_ On /\ A. x e. On ( x C_ A -> x e. A ) ) -> ( A C_ On /\ On C_ A ) ) |
| 24 | eqss | |- ( A = On <-> ( A C_ On /\ On C_ A ) ) |
|
| 25 | 23 24 | sylibr | |- ( ( A C_ On /\ A. x e. On ( x C_ A -> x e. A ) ) -> A = On ) |