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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cina	⊢ Inacc
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	8	cv	⊢ 𝑦
10	9	cpw	⊢ 𝒫 𝑦
11		csdm	⊢ ≺
12	10 2 11	wbr	⊢ 𝒫 𝑦 ≺ 𝑥
13	12 8 2	wral	⊢ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥
14	4 7 13	w3a	⊢ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥 )
15	14 1	cab	⊢ { 𝑥 ∣ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥 ) }
16	0 15	wceq	⊢ Inacc = { 𝑥 ∣ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥 ) }