Metamath Proof Explorer


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 ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦𝑥 𝒫 𝑦𝑥 ) }