Metamath Proof Explorer


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 )