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

Metamath Proof Explorer

Theorem winacard

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

Ref Expression
Assertion winacard ⊢ A ∈ Inacc 𝑤 → card ⁡ A = A

Proof

Step Hyp Ref Expression
1 elwina ⊢ A ∈ Inacc 𝑤 ↔ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A ∃ y ∈ A x ≺ y
2 cardcf ⊢ card ⁡ cf ⁡ A = cf ⁡ A
3 fveq2 ⊢ cf ⁡ A = A → card ⁡ cf ⁡ A = card ⁡ A
4 id ⊢ cf ⁡ A = A → cf ⁡ A = A
5 2 3 4 3eqtr3a ⊢ cf ⁡ A = A → card ⁡ A = A
6 5 3ad2ant2 ⊢ A ≠ ∅ ∧ cf ⁡ A = A ∧ ∀ x ∈ A ∃ y ∈ A x ≺ y → card ⁡ A = A
7 1 6 sylbi ⊢ A ∈ Inacc 𝑤 → card ⁡ A = A