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 = { 𝑥 ∣ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwina	⊢ Inaccw
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3		c0	⊢ ∅
4	2 3	wne	⊢ 𝑥 ≠ ∅
5		ccf	⊢ cf
6	2 5	cfv	⊢ ( cf ‘ 𝑥 )
7	6 2	wceq	⊢ ( cf ‘ 𝑥 ) = 𝑥
8		vy	⊢ 𝑦
9		vz	⊢ 𝑧
10	8	cv	⊢ 𝑦
11		csdm	⊢ ≺
12	9	cv	⊢ 𝑧
13	10 12 11	wbr	⊢ 𝑦 ≺ 𝑧
14	13 9 2	wrex	⊢ ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
15	14 8 2	wral	⊢ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧
16	4 7 15	w3a	⊢ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 )
17	16 1	cab	⊢ { 𝑥 ∣ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 ) }
18	0 17	wceq	⊢ Inaccw = { 𝑥 ∣ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 ) }