Metamath Proof Explorer

Theorem tfsconcatfv1

Description: An early value of the concatenation of two transfinite series. (Contributed by RP, 23-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 tfsconcatfv1 
|- ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> ( ( A .+ B ) ` X ) = ( A ` X ) )

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 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 ) ) ) } ) )
3 2 fveq1d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( A .+ B ) ` X ) = ( ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) ` X ) )
4 3 adantr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> ( ( A .+ B ) ` X ) = ( ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) ` X ) )
5 simplll 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> A Fn C )
6 simplrl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> C e. On )
7 simplrr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> D e. On )
8 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 ) )
9 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 ) ) )
10 6 7 8 9 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 ) ) )
11 10 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 ) ) )
12 11 adantr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> A. x e. ( ( C +o D ) \ C ) E! y E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) )
13 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 ) ) ) }
14 13 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 ) )
15 12 14 sylib 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } Fn ( ( C +o D ) \ C ) )
16 disjdif 
 |-  ( C i^i ( ( C +o D ) \ C ) ) = (/)
17 16 a1i 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> ( C i^i ( ( C +o D ) \ C ) ) = (/) )
18 simpr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> X e. C )
19 5 15 17 18 fvun1d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> ( ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) ` X ) = ( A ` X ) )
20 4 19 eqtrd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> ( ( A .+ B ) ` X ) = ( A ` X ) )