This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem winalim

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

Ref Expression
Assertion winalim ( 𝐴 ∈ Inaccw → Lim 𝐴 )

Proof

Step Hyp Ref Expression
1 winainf ⊢ ( 𝐴 ∈ Inaccw → ω ⊆ 𝐴 )
2 winacard ⊢ ( 𝐴 ∈ Inaccw → ( card ‘ 𝐴 ) = 𝐴 )
3 cardlim ⊢ ( ω ⊆ ( card ‘ 𝐴 ) ↔ Lim ( card ‘ 𝐴 ) )
4 sseq2 ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ω ⊆ ( card ‘ 𝐴 ) ↔ ω ⊆ 𝐴 ) )
5 limeq ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( Lim ( card ‘ 𝐴 ) ↔ Lim 𝐴 ) )
6 4 5 bibi12d ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ( ω ⊆ ( card ‘ 𝐴 ) ↔ Lim ( card ‘ 𝐴 ) ) ↔ ( ω ⊆ 𝐴 ↔ Lim 𝐴 ) ) )
7 3 6 mpbii ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ( ω ⊆ 𝐴 ↔ Lim 𝐴 ) )
8 2 7 syl ⊢ ( 𝐴 ∈ Inaccw → ( ω ⊆ 𝐴 ↔ Lim 𝐴 ) )
9 1 8 mpbid ⊢ ( 𝐴 ∈ Inaccw → Lim 𝐴 )