Definition df-wina 9385

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

Assertion

Ref	Expression
df-wina	⊢ Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-wina

Step	Hyp	Ref	Expression
1		cwina 9383	. 2 class Inaccw
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1474	. . . . 5 class 𝑥
4		c0 3874	. . . . 5 class ∅
5	3, 4	wne 2780	. . . 4 wff 𝑥 ≠ ∅
6		ccf 8646	. . . . . 6 class cf
7	3, 6	cfv 5804	. . . . 5 class (cf‘𝑥)
8	7, 3	wceq 1475	. . . 4 wff (cf‘𝑥) = 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1474	. . . . . . 7 class 𝑦
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1474	. . . . . . 7 class 𝑧
13		csdm 7840	. . . . . . 7 class ≺
14	10, 12, 13	wbr 4583	. . . . . 6 wff 𝑦 ≺ 𝑧
15	14, 11, 3	wrex 2897	. . . . 5 wff ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
16	15, 9, 3	wral 2896	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
17	5, 8, 16	w3a 1031	. . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)
18	17, 2	cab 2596	. 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}
19	1, 18	wceq 1475	1 wff Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}

This definition is referenced by:  elwina  9387