Metamath Proof Explorer

Theorem tfsconcatfn

Description: The concatenation of two transfinite series is a transfinite series. (Contributed by RP, 22-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 tfsconcatfn 
|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A .+ B ) Fn ( C +o D ) )

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 simpll 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> A Fn C )
3 simplrl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> C e. On )
4 simplrr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> D e. On )
5 simpr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> x e. ( ( C +o D ) \ C ) )
6 tfsconcatlem 
 |-  ( ( C e. On /\ D e. On /\ x e. ( ( C +o D ) \ C ) ) -> E! y E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) )
7 3 4 5 6 syl3anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> E! y E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) )
8 7 ralrimiva 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> A. x e. ( ( C +o D ) \ C ) E! y E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) )
9 eqid 
 |-  { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) }
10 9 fnopabg 
 |-  ( A. x e. ( ( C +o D ) \ C ) E! y E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } Fn ( ( C +o D ) \ C ) )
11 8 10 sylib 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } Fn ( ( C +o D ) \ C ) )
12 disjdif 
 |-  ( C i^i ( ( C +o D ) \ C ) ) = (/)
13 12 a1i 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( C i^i ( ( C +o D ) \ C ) ) = (/) )
14 2 11 13 fnund 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) Fn ( C u. ( ( C +o D ) \ C ) ) )
15 1 tfsconcatun 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A .+ B ) = ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) )
16 oaword1 
 |-  ( ( C e. On /\ D e. On ) -> C C_ ( C +o D ) )
17 undif 
 |-  ( C C_ ( C +o D ) <-> ( C u. ( ( C +o D ) \ C ) ) = ( C +o D ) )
18 16 17 sylib 
 |-  ( ( C e. On /\ D e. On ) -> ( C u. ( ( C +o D ) \ C ) ) = ( C +o D ) )
19 18 eqcomd 
 |-  ( ( C e. On /\ D e. On ) -> ( C +o D ) = ( C u. ( ( C +o D ) \ C ) ) )
20 19 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( C +o D ) = ( C u. ( ( C +o D ) \ C ) ) )
21 15 20 fneq12d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( A .+ B ) Fn ( C +o D ) <-> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) Fn ( C u. ( ( C +o D ) \ C ) ) ) )
22 14 21 mpbird 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A .+ B ) Fn ( C +o D ) )