Description: The concatenation of transfinite sequences yields ordinals iff both
sequences yield ordinals. Theorem 4 in Grzegorz Bancerek, "Epsilon
Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4,
Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025)
Ref
Expression
Hypothesis
tfsconcat.op
|- .+ = ( a e. _V , b e. _V |-> ( a u. { <. x , y >. | ( x e. ( ( dom a +o dom b ) \ dom a ) /\ E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) ) } ) )
|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ran ( A .+ B ) C_ On <-> ( ran A C_ On /\ ran B C_ On ) ) )
Proof
Step
Hyp
Ref
Expression
1
tfsconcat.op
|- .+ = ( a e. _V , b e. _V |-> ( a u. { <. x , y >. | ( x e. ( ( dom a +o dom b ) \ dom a ) /\ E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) ) } ) )