Definition df-wina

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwina	|- InaccW
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		vz	|- z
10	8	cv	|- y
11		csdm	|- ~<
12	9	cv	|- z
13	10 12 11	wbr	|- y ~< z
14	13 9 2	wrex	|- E. z e. x y ~< z
15	14 8 2	wral	|- A. y e. x E. z e. x y ~< z
16	4 7 15	w3a	|- ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z )
17	16 1	cab	|- { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z ) }
18	0 17	wceq	|- InaccW = { x | ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z ) }