Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Functions on ordinals; strictly monotone ordinal functions
smofvon
Metamath Proof Explorer
Description: If B is a strictly monotone ordinal function, and A is in the
domain of B , then the value of the function at A is an ordinal.
(Contributed by Andrew Salmon , 20-Nov-2011)
Ref
Expression
Assertion
smofvon
⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → B ⁡ A ∈ On
Proof
Step
Hyp
Ref
Expression
1
df-smo
⊢ Smo ⁡ B ↔ B : dom ⁡ B ⟶ On ∧ Ord ⁡ dom ⁡ B ∧ ∀ x ∈ dom ⁡ B ∀ y ∈ dom ⁡ B x ∈ y → B ⁡ x ∈ B ⁡ y
2
1
simp1bi
⊢ Smo ⁡ B → B : dom ⁡ B ⟶ On
3
2
ffvelrnda
⊢ Smo ⁡ B ∧ A ∈ dom ⁡ B → B ⁡ A ∈ On