Theorem winaon

Description: A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014)

	Ref	Expression
Assertion	winaon	⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		elwina	⊢ ( 𝐴 ∈ Inaccw ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
2		cfon	⊢ ( cf ‘ 𝐴 ) ∈ On
3		eleq1	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → ( ( cf ‘ 𝐴 ) ∈ On ↔ 𝐴 ∈ On ) )
4	2 3	mpbii	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ On )
5	4	3ad2ant2	⊢ ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → 𝐴 ∈ On )
6	1 5	sylbi	⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ On )