Theorem winainf

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

	Ref	Expression
Assertion	winainf	⊢ ( 𝐴 ∈ Inaccw → ω ⊆ 𝐴 )

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		winainflem	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ω ⊆ 𝐴 )
6	4 5	syl3an2	⊢ ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ω ⊆ 𝐴 )
7	1 6	sylbi	⊢ ( 𝐴 ∈ Inaccw → ω ⊆ 𝐴 )