This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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