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 ) |