Definition df-wina 10440

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 10438	. 2 class Inaccw
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1538	. . . . 5 class 𝑥
4		c0 4256	. . . . 5 class ∅
5	3, 4	wne 2943	. . . 4 wff 𝑥 ≠ ∅
6		ccf 9695	. . . . . 6 class cf
7	3, 6	cfv 6433	. . . . 5 class (cf‘𝑥)
8	7, 3	wceq 1539	. . . 4 wff (cf‘𝑥) = 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1538	. . . . . . 7 class 𝑦
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1538	. . . . . . 7 class 𝑧
13		csdm 8732	. . . . . . 7 class ≺
14	10, 12, 13	wbr 5074	. . . . . 6 wff 𝑦 ≺ 𝑧
15	14, 11, 3	wrex 3065	. . . . 5 wff ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
16	15, 9, 3	wral 3064	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
17	5, 8, 16	w3a 1086	. . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)
18	17, 2	cab 2715	. 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}
19	1, 18	wceq 1539	1 wff Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}

This definition is referenced by:  elwina  10442