Theorem inawina

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

	Ref	Expression
Assertion	inawina	⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ Inaccw )

Proof

Step	Hyp	Ref	Expression
1		cfon	⊢ ( cf ‘ 𝐴 ) ∈ On
2		eleq1	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → ( ( cf ‘ 𝐴 ) ∈ On ↔ 𝐴 ∈ On ) )
3	1 2	mpbii	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → 𝐴 ∈ On )
4	3	3ad2ant2	⊢ ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) → 𝐴 ∈ On )
5		idd	⊢ ( 𝐴 ∈ On → ( 𝐴 ≠ ∅ → 𝐴 ≠ ∅ ) )
6		idd	⊢ ( 𝐴 ∈ On → ( ( cf ‘ 𝐴 ) = 𝐴 → ( cf ‘ 𝐴 ) = 𝐴 ) )
7		inawinalem	⊢ ( 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
8	5 6 7	3anim123d	⊢ ( 𝐴 ∈ On → ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ) )
9	4 8	mpcom	⊢ ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
10		elina	⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 ) )
11		elwina	⊢ ( 𝐴 ∈ Inaccw ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
12	9 10 11	3imtr4i	⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ Inaccw )