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 Inaccw = { 𝑥 ∣ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwina ⊢ Inaccw
1 vx ⊢ 𝑥
2 1 cv ⊢ 𝑥
3 c0 ⊢ ∅
4 2 3 wne ⊢ 𝑥 ≠ ∅
5 ccf ⊢ cf
6 2 5 cfv ⊢ ( cf ‘ 𝑥 )
7 6 2 wceq ⊢ ( cf ‘ 𝑥 ) = 𝑥
8 vy ⊢ 𝑦
9 vz ⊢ 𝑧
10 8 cv ⊢ 𝑦
11 csdm ⊢ ≺
12 9 cv ⊢ 𝑧
13 10 12 11 wbr ⊢ 𝑦 ≺ 𝑧
14 13 9 2 wrex ⊢ ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
15 14 8 2 wral ⊢ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
16 4 7 15 w3a ⊢ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 )
17 16 1 cab ⊢ { 𝑥 ∣ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 ) }
18 0 17 wceq ⊢ Inaccw = { 𝑥 ∣ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 ) }