This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Functions on ordinals; strictly monotone ordinal functions smofvon
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 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐵 ‘ 𝐴 ) ∈ On )
Proof
Step
Hyp
Ref
Expression
1
df-smo ⊢ ( Smo 𝐵 ↔ ( 𝐵 : dom 𝐵 ⟶ On ∧ Ord dom 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
2
1
simp1bi ⊢ ( Smo 𝐵 → 𝐵 : dom 𝐵 ⟶ On )
3
2
ffvelcdmda ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐵 ‘ 𝐴 ) ∈ On )