Description: An ordinal is a topology iff it is not its supremum (union), proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 1-Nov-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ordtop | ⊢ ( Ord 𝐽 → ( 𝐽 ∈ Top ↔ 𝐽 ≠ ∪ 𝐽 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | ⊢ ∪ 𝐽 = ∪ 𝐽 | |
| 2 | 1 | topopn | ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 ) |
| 3 | nordeq | ⊢ ( ( Ord 𝐽 ∧ ∪ 𝐽 ∈ 𝐽 ) → 𝐽 ≠ ∪ 𝐽 ) | |
| 4 | 3 | ex | ⊢ ( Ord 𝐽 → ( ∪ 𝐽 ∈ 𝐽 → 𝐽 ≠ ∪ 𝐽 ) ) |
| 5 | 2 4 | syl5 | ⊢ ( Ord 𝐽 → ( 𝐽 ∈ Top → 𝐽 ≠ ∪ 𝐽 ) ) |
| 6 | onsuctop | ⊢ ( ∪ 𝐽 ∈ On → suc ∪ 𝐽 ∈ Top ) | |
| 7 | 6 | ordtoplem | ⊢ ( Ord 𝐽 → ( 𝐽 ≠ ∪ 𝐽 → 𝐽 ∈ Top ) ) |
| 8 | 5 7 | impbid | ⊢ ( Ord 𝐽 → ( 𝐽 ∈ Top ↔ 𝐽 ≠ ∪ 𝐽 ) ) |