Definition df-ina 9507

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 = { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-ina

Step	Hyp	Ref	Expression
1		cina 9505	. 2 class Inacc
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4		c0 3915	. . . . 5 class (/)
5	3, 4	wne 2794	. . . 4 wff x =/= (/)
6		ccf 8763	. . . . . 6 class cf
7	3, 6	cfv 5888	. . . . 5 class ( cf ` x )
8	7, 3	wceq 1483	. . . 4 wff ( cf ` x ) = x
9		vy	. . . . . . . 8 setvar y
10	9	cv 1482	. . . . . . 7 class y
11	10	cpw 4158	. . . . . 6 class ~P y
12		csdm 7954	. . . . . 6 class ~<
13	11, 3, 12	wbr 4653	. . . . 5 wff ~P y ~< x
14	13, 9, 3	wral 2912	. . . 4 wff A. y e. x ~P y ~< x
15	5, 8, 14	w3a 1037	. . 3 wff ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x )
16	15, 2	cab 2608	. 2 class { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x ) }
17	1, 16	wceq 1483	1 wff Inacc = { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x ) }

This definition is referenced by:  elina  9509