Definition df-wina 9127

Description: An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows om as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013.)

Assertion

Ref	Expression
df-wina	|- InaccW = { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-wina

Step	Hyp	Ref	Expression
1		cwina 9125	. 2 class InaccW
2		vx	. . . . . 6 setvar x
3	2	cv 1451	. . . . 5 class x
4		c0 3722	. . . . 5 class (/)
5	3, 4	wne 2641	. . . 4 wff x =/= (/)
6		ccf 8389	. . . . . 6 class cf
7	3, 6	cfv 5589	. . . . 5 class ( cf ` x )
8	7, 3	wceq 1452	. . . 4 wff ( cf ` x ) = x
9		vy	. . . . . . . 8 setvar y
10	9	cv 1451	. . . . . . 7 class y
11		vz	. . . . . . . 8 setvar z
12	11	cv 1451	. . . . . . 7 class z
13		csdm 7586	. . . . . . 7 class ~<
14	10, 12, 13	wbr 4395	. . . . . 6 wff y ~< z
15	14, 11, 3	wrex 2757	. . . . 5 wff E. z e. x y ~< z
16	15, 9, 3	wral 2756	. . . 4 wff A. y e. x E. z e. x y ~< z
17	5, 8, 16	w3a 1007	. . 3 wff ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z )
18	17, 2	cab 2457	. 2 class { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z ) }
19	1, 18	wceq 1452	1 wff InaccW = { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z ) }

This definition is referenced by:  elwina  9129