Definition df-ina

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)

	Ref	Expression
Assertion	df-ina	|- Inacc = { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cina	|- Inacc
1		vx	|- x
2	1	cv	|- x
3		c0	|- (/)
4	2 3	wne	|- x =/= (/)
5		ccf	|- cf
6	2 5	cfv	|- ( cf ` x )
7	6 2	wceq	|- ( cf ` x ) = x
8		vy	|- y
9	8	cv	|- y
10	9	cpw	|- ~P y
11		csdm	|- ~<
12	10 2 11	wbr	|- ~P y ~< x
13	12 8 2	wral	|- A. y e. x ~P y ~< x
14	4 7 13	w3a	|- ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x )
15	14 1	cab	|- { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x ) }
16	0 15	wceq	|- Inacc = { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x ) }