Definition df-wina 10100

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 10098	. 2 class Inaccw
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1532	. . . . 5 class 𝑥
4		c0 4290	. . . . 5 class ∅
5	3, 4	wne 3016	. . . 4 wff 𝑥 ≠ ∅
6		ccf 9360	. . . . . 6 class cf
7	3, 6	cfv 6349	. . . . 5 class (cf‘𝑥)
8	7, 3	wceq 1533	. . . 4 wff (cf‘𝑥) = 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1532	. . . . . . 7 class 𝑦
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1532	. . . . . . 7 class 𝑧
13		csdm 8502	. . . . . . 7 class ≺
14	10, 12, 13	wbr 5058	. . . . . 6 wff 𝑦 ≺ 𝑧
15	14, 11, 3	wrex 3139	. . . . 5 wff ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
16	15, 9, 3	wral 3138	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
17	5, 8, 16	w3a 1083	. . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)
18	17, 2	cab 2799	. 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}
19	1, 18	wceq 1533	1 wff Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}

This definition is referenced by:  elwina  10102