Definition df-wina 10769

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 10767	. 2 class Inaccw
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1569	. . . . 5 class 𝑥
4		c0 4279	. . . . 5 class ∅
5	3, 4	wne 2956	. . . 4 wff 𝑥 ≠ ∅
6		ccf 10018	. . . . . 6 class cf
7	3, 6	cfv 6538	. . . . 5 class (cf‘𝑥)
8	7, 3	wceq 1570	. . . 4 wff (cf‘𝑥) = 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1569	. . . . . . 7 class 𝑦
11		vz	. . . . . . . 8 setvar 𝑧
12	11	cv 1569	. . . . . . 7 class 𝑧
13		csdm 8972	. . . . . . 7 class ≺
14	10, 12, 13	wbr 5103	. . . . . 6 wff 𝑦 ≺ 𝑧
15	14, 11, 3	wrex 3087	. . . . 5 wff ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
16	15, 9, 3	wral 3077	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
17	5, 8, 16	w3a 1103	. . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)
18	17, 2	cab 2739	. 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}
19	1, 18	wceq 1570	1 wff Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}

This definition is used by:  elwina  10771