Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ina | Structured version Visualization version GIF version |
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 |
---|---|
df-ina | ⊢ Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cina 10327 | . 2 class Inacc | |
2 | vx | . . . . . 6 setvar 𝑥 | |
3 | 2 | cv 1542 | . . . . 5 class 𝑥 |
4 | c0 4254 | . . . . 5 class ∅ | |
5 | 3, 4 | wne 2943 | . . . 4 wff 𝑥 ≠ ∅ |
6 | ccf 9583 | . . . . . 6 class cf | |
7 | 3, 6 | cfv 6401 | . . . . 5 class (cf‘𝑥) |
8 | 7, 3 | wceq 1543 | . . . 4 wff (cf‘𝑥) = 𝑥 |
9 | vy | . . . . . . . 8 setvar 𝑦 | |
10 | 9 | cv 1542 | . . . . . . 7 class 𝑦 |
11 | 10 | cpw 4530 | . . . . . 6 class 𝒫 𝑦 |
12 | csdm 8649 | . . . . . 6 class ≺ | |
13 | 11, 3, 12 | wbr 5070 | . . . . 5 wff 𝒫 𝑦 ≺ 𝑥 |
14 | 13, 9, 3 | wral 3064 | . . . 4 wff ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥 |
15 | 5, 8, 14 | w3a 1089 | . . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥) |
16 | 15, 2 | cab 2716 | . 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)} |
17 | 1, 16 | wceq 1543 | 1 wff Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)} |
Colors of variables: wff setvar class |
This definition is referenced by: elina 10331 |
Copyright terms: Public domain | W3C validator |