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

Metamath Proof Explorer

Definition df-wina

Description: An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows _om as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013)

Ref Expression
Assertion df-wina ⊢ Inacc 𝑤 = x | x ≠ ∅ ∧ cf ⁡ x = x ∧ ∀ y ∈ x ∃ z ∈ x y ≺ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwina class Inacc 𝑤
1 vx setvar x
2 1 cv setvar x
3 c0 class ∅
4 2 3 wne wff x ≠ ∅
5 ccf class cf
6 2 5 cfv class cf ⁡ x
7 6 2 wceq wff cf ⁡ x = x
8 vy setvar y
9 vz setvar z
10 8 cv setvar y
11 csdm class ≺
12 9 cv setvar z
13 10 12 11 wbr wff y ≺ z
14 13 9 2 wrex wff ∃ z ∈ x y ≺ z
15 14 8 2 wral wff ∀ y ∈ x ∃ z ∈ x y ≺ z
16 4 7 15 w3a wff x ≠ ∅ ∧ cf ⁡ x = x ∧ ∀ y ∈ x ∃ z ∈ x y ≺ z
17 16 1 cab class x | x ≠ ∅ ∧ cf ⁡ x = x ∧ ∀ y ∈ x ∃ z ∈ x y ≺ z
18 0 17 wceq wff Inacc 𝑤 = x | x ≠ ∅ ∧ cf ⁡ x = x ∧ ∀ y ∈ x ∃ z ∈ x y ≺ z