Metamath Proof Explorer


Theorem tfi

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 )

Proof

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 )