Database
TG (TARSKI-GROTHENDIECK) SET THEORY
Inaccessibles
Weakly and strongly inaccessible cardinals
df-ina
Metamath Proof Explorer
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 ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥 ) }