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 | ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ On ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → 𝐴 = On ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldifn | ⊢ ( 𝑥 ∈ ( On ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 ) | |
| 2 | 1 | adantl | ⊢ ( ( ( 𝑥 ∈ On → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( On ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 ) |
| 3 | onss | ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On ) | |
| 4 | difin0ss | ⊢ ( ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ → ( 𝑥 ⊆ On → 𝑥 ⊆ 𝐴 ) ) | |
| 5 | 3 4 | syl5com | ⊢ ( 𝑥 ∈ On → ( ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ → 𝑥 ⊆ 𝐴 ) ) |
| 6 | 5 | imim1d | ⊢ ( 𝑥 ∈ On → ( ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ( ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ → 𝑥 ∈ 𝐴 ) ) ) |
| 7 | 6 | a2i | ⊢ ( ( 𝑥 ∈ On → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ On → ( ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ → 𝑥 ∈ 𝐴 ) ) ) |
| 8 | eldifi | ⊢ ( 𝑥 ∈ ( On ∖ 𝐴 ) → 𝑥 ∈ On ) | |
| 9 | 7 8 | impel | ⊢ ( ( ( 𝑥 ∈ On → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( On ∖ 𝐴 ) ) → ( ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ → 𝑥 ∈ 𝐴 ) ) |
| 10 | 2 9 | mtod | ⊢ ( ( ( 𝑥 ∈ On → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) ∧ 𝑥 ∈ ( On ∖ 𝐴 ) ) → ¬ ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ) |
| 11 | 10 | ex | ⊢ ( ( 𝑥 ∈ On → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ ( On ∖ 𝐴 ) → ¬ ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ) ) |
| 12 | 11 | ralimi2 | ⊢ ( ∀ 𝑥 ∈ On ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ∀ 𝑥 ∈ ( On ∖ 𝐴 ) ¬ ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ) |
| 13 | ralnex | ⊢ ( ∀ 𝑥 ∈ ( On ∖ 𝐴 ) ¬ ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ↔ ¬ ∃ 𝑥 ∈ ( On ∖ 𝐴 ) ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ) | |
| 14 | 12 13 | sylib | ⊢ ( ∀ 𝑥 ∈ On ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → ¬ ∃ 𝑥 ∈ ( On ∖ 𝐴 ) ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ) |
| 15 | ssdif0 | ⊢ ( On ⊆ 𝐴 ↔ ( On ∖ 𝐴 ) = ∅ ) | |
| 16 | 15 | necon3bbii | ⊢ ( ¬ On ⊆ 𝐴 ↔ ( On ∖ 𝐴 ) ≠ ∅ ) |
| 17 | ordon | ⊢ Ord On | |
| 18 | difss | ⊢ ( On ∖ 𝐴 ) ⊆ On | |
| 19 | tz7.5 | ⊢ ( ( Ord On ∧ ( On ∖ 𝐴 ) ⊆ On ∧ ( On ∖ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ ( On ∖ 𝐴 ) ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ) | |
| 20 | 17 18 19 | mp3an12 | ⊢ ( ( On ∖ 𝐴 ) ≠ ∅ → ∃ 𝑥 ∈ ( On ∖ 𝐴 ) ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ) |
| 21 | 16 20 | sylbi | ⊢ ( ¬ On ⊆ 𝐴 → ∃ 𝑥 ∈ ( On ∖ 𝐴 ) ( ( On ∖ 𝐴 ) ∩ 𝑥 ) = ∅ ) |
| 22 | 14 21 | nsyl2 | ⊢ ( ∀ 𝑥 ∈ On ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) → On ⊆ 𝐴 ) |
| 23 | 22 | anim2i | ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ On ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → ( 𝐴 ⊆ On ∧ On ⊆ 𝐴 ) ) |
| 24 | eqss | ⊢ ( 𝐴 = On ↔ ( 𝐴 ⊆ On ∧ On ⊆ 𝐴 ) ) | |
| 25 | 23 24 | sylibr | ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ On ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴 ) ) → 𝐴 = On ) |