Metamath Proof Explorer

Theorem tfsconcatun

Description: The concatenation of two transfinite series is a union of functions. (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 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 ) ) ) } ) )

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 a1i 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> .+ = ( 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 ) ) ) } ) ) )
3 simprl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> a = A )
4 dmeq 
 |-  ( a = A -> dom a = dom A )
5 4 adantr 
 |-  ( ( a = A /\ b = B ) -> dom a = dom A )
6 fndm 
 |-  ( A Fn C -> dom A = C )
7 6 adantr 
 |-  ( ( A Fn C /\ B Fn D ) -> dom A = C )
8 7 adantr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> dom A = C )
9 5 8 sylan9eqr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> dom a = C )
10 dmeq 
 |-  ( b = B -> dom b = dom B )
11 10 adantl 
 |-  ( ( a = A /\ b = B ) -> dom b = dom B )
12 fndm 
 |-  ( B Fn D -> dom B = D )
13 12 adantl 
 |-  ( ( A Fn C /\ B Fn D ) -> dom B = D )
14 13 adantr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> dom B = D )
15 11 14 sylan9eqr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> dom b = D )
16 9 15 oveq12d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( dom a +o dom b ) = ( C +o D ) )
17 16 9 difeq12d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( ( dom a +o dom b ) \ dom a ) = ( ( C +o D ) \ C ) )
18 17 eleq2d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( x e. ( ( dom a +o dom b ) \ dom a ) <-> x e. ( ( C +o D ) \ C ) ) )
19 9 oveq1d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( dom a +o z ) = ( C +o z ) )
20 19 eqeq2d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( x = ( dom a +o z ) <-> x = ( C +o z ) ) )
21 fveq1 
 |-  ( b = B -> ( b ` z ) = ( B ` z ) )
22 21 eqeq2d 
 |-  ( b = B -> ( y = ( b ` z ) <-> y = ( B ` z ) ) )
23 22 adantl 
 |-  ( ( a = A /\ b = B ) -> ( y = ( b ` z ) <-> y = ( B ` z ) ) )
24 23 adantl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( y = ( b ` z ) <-> y = ( B ` z ) ) )
25 20 24 anbi12d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( ( x = ( dom a +o z ) /\ y = ( b ` z ) ) <-> ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
26 15 25 rexeqbidv 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) <-> E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
27 18 26 anbi12d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( ( x e. ( ( dom a +o dom b ) \ dom a ) /\ E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) ) <-> ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) ) )
28 27 opabbidv 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> { <. x , y >. | ( x e. ( ( dom a +o dom b ) \ dom a ) /\ E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) ) } = { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } )
29 3 28 uneq12d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( a = A /\ b = B ) ) -> ( 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 u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) )
30 fnex 
 |-  ( ( A Fn C /\ C e. On ) -> A e. _V )
31 30 ad2ant2r 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> A e. _V )
32 fnex 
 |-  ( ( B Fn D /\ D e. On ) -> B e. _V )
33 32 ad2ant2l 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> B e. _V )
34 oacl 
 |-  ( ( C e. On /\ D e. On ) -> ( C +o D ) e. On )
35 34 difexd 
 |-  ( ( C e. On /\ D e. On ) -> ( ( C +o D ) \ C ) e. _V )
36 35 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( C +o D ) \ C ) e. _V )
37 simplrl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> C e. On )
38 simplrr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> D e. On )
39 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 ) )
40 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 ) ) )
41 37 38 39 40 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 ) ) )
42 euabex 
 |-  ( E! y E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) -> { y | E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) } e. _V )
43 41 42 syl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> { y | E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) } e. _V )
44 36 43 opabex3d 
 |-  ( ( ( 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 ) ) ) } e. _V )
45 31 44 unexd 
 |-  ( ( ( 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 ) ) ) } ) e. _V )
46 2 29 31 33 45 ovmpod 
 |-  ( ( ( 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 ) ) ) } ) )