Definition df-ina 10096

Description: An ordinal is strongly inaccessible iff it is a regular strong limit cardinal, which is to say that it dominates the powersets of every smaller ordinal. (Contributed by Mario Carneiro, 22-Jun-2013.)

Assertion

Ref	Expression
df-ina	⊢ Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-ina

Step	Hyp	Ref	Expression
1		cina 10094	. 2 class Inacc
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1537	. . . . 5 class 𝑥
4		c0 4243	. . . . 5 class ∅
5	3, 4	wne 2987	. . . 4 wff 𝑥 ≠ ∅
6		ccf 9350	. . . . . 6 class cf
7	3, 6	cfv 6324	. . . . 5 class (cf‘𝑥)
8	7, 3	wceq 1538	. . . 4 wff (cf‘𝑥) = 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1537	. . . . . . 7 class 𝑦
11	10	cpw 4497	. . . . . 6 class 𝒫 𝑦
12		csdm 8491	. . . . . 6 class ≺
13	11, 3, 12	wbr 5030	. . . . 5 wff 𝒫 𝑦 ≺ 𝑥
14	13, 9, 3	wral 3106	. . . 4 wff ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥
15	5, 8, 14	w3a 1084	. . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)
16	15, 2	cab 2776	. 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)}
17	1, 16	wceq 1538	1 wff Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)}

This definition is referenced by:  elina  10098