Description: The concatenation of transfinite sequences yields elements from a class iff both sequences yield elements from that class. (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 ) ) ) } ) ) |
|
| Assertion | tfsconcatrnss | |- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ran ( A .+ B ) C_ X <-> ( ran A C_ X /\ ran B C_ X ) ) ) |
| 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 | tfsconcatrn | |- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran ( A .+ B ) = ( ran A u. ran B ) ) |
| 3 | 2 | sseq1d | |- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ran ( A .+ B ) C_ X <-> ( ran A u. ran B ) C_ X ) ) |
| 4 | unss | |- ( ( ran A C_ X /\ ran B C_ X ) <-> ( ran A u. ran B ) C_ X ) |
|
| 5 | 3 4 | bitr4di | |- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ran ( A .+ B ) C_ X <-> ( ran A C_ X /\ ran B C_ X ) ) ) |