Theorem tfsconcatfo

Description: The concatenation of two transfinite series is onto the union of the ranges. (Contributed by RP, 24-Feb-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 ) ) ) } ) )
Assertion	tfsconcatfo	|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A .+ B ) : ( C +o D ) -onto-> ( ran A u. ran B ) )

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 ) ) ) } ) )
2	1	tfsconcatfn	|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A .+ B ) Fn ( C +o D ) )
3	1	tfsconcatrn	|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran ( A .+ B ) = ( ran A u. ran B ) )
4		df-fo	|- ( ( A .+ B ) : ( C +o D ) -onto-> ( ran A u. ran B ) <-> ( ( A .+ B ) Fn ( C +o D ) /\ ran ( A .+ B ) = ( ran A u. ran B ) ) )
5	2 3 4	sylanbrc	|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A .+ B ) : ( C +o D ) -onto-> ( ran A u. ran B ) )