Metamath Proof Explorer

Theorem onsucsuccmp

Description: The successor of a successor ordinal number is a compact topology. (Contributed by Chen-Pang He, 18-Oct-2015)

Ref Expression
Assertion onsucsuccmp ⊢ A ∈ On → suc ⁡ suc ⁡ A ∈ Comp

Proof

Step Hyp Ref Expression
1 suceq ⊢ A = if A ∈ On A ∅ → suc ⁡ A = suc ⁡ if A ∈ On A ∅
2 suceq ⊢ suc ⁡ A = suc ⁡ if A ∈ On A ∅ → suc ⁡ suc ⁡ A = suc ⁡ suc ⁡ if A ∈ On A ∅
3 1 2 syl ⊢ A = if A ∈ On A ∅ → suc ⁡ suc ⁡ A = suc ⁡ suc ⁡ if A ∈ On A ∅
4 3 eleq1d ⊢ A = if A ∈ On A ∅ → suc ⁡ suc ⁡ A ∈ Comp ↔ suc ⁡ suc ⁡ if A ∈ On A ∅ ∈ Comp
5 0elon ⊢ ∅ ∈ On
6 5 elimel ⊢ if A ∈ On A ∅ ∈ On
7 6 onsucsuccmpi ⊢ suc ⁡ suc ⁡ if A ∈ On A ∅ ∈ Comp
8 4 7 dedth ⊢ A ∈ On → suc ⁡ suc ⁡ A ∈ Comp