Metamath Proof Explorer

Theorem tfsconcatfv2

Description: A latter 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 tfsconcatfv2 
|- ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( ( A .+ B ) ` ( C +o X ) ) = ( B ` 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 ) ` ( C +o X ) ) = ( ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) ` ( C +o X ) ) )
4 3 adantr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( ( A .+ B ) ` ( C +o X ) ) = ( ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) ` ( C +o X ) ) )
5 simplll 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> 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 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 ) ) ) }
13 12 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 ) )
14 11 13 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 ) )
15 14 adantr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> { <. 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. D ) -> ( C i^i ( ( C +o D ) \ C ) ) = (/) )
18 pm3.22 
 |-  ( ( C e. On /\ D e. On ) -> ( D e. On /\ C e. On ) )
19 18 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( D e. On /\ C e. On ) )
20 oaordi 
 |-  ( ( D e. On /\ C e. On ) -> ( X e. D -> ( C +o X ) e. ( C +o D ) ) )
21 19 20 syl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( X e. D -> ( C +o X ) e. ( C +o D ) ) )
22 21 imp 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( C +o X ) e. ( C +o D ) )
23 simplrl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> C e. On )
24 simpr 
 |-  ( ( C e. On /\ D e. On ) -> D e. On )
25 24 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> D e. On )
26 onelon 
 |-  ( ( D e. On /\ X e. D ) -> X e. On )
27 25 26 sylan 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> X e. On )
28 oaword1 
 |-  ( ( C e. On /\ X e. On ) -> C C_ ( C +o X ) )
29 23 27 28 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> C C_ ( C +o X ) )
30 oacl 
 |-  ( ( C e. On /\ D e. On ) -> ( C +o D ) e. On )
31 eloni 
 |-  ( ( C +o D ) e. On -> Ord ( C +o D ) )
32 30 31 syl 
 |-  ( ( C e. On /\ D e. On ) -> Ord ( C +o D ) )
33 eloni 
 |-  ( C e. On -> Ord C )
34 33 adantr 
 |-  ( ( C e. On /\ D e. On ) -> Ord C )
35 32 34 jca 
 |-  ( ( C e. On /\ D e. On ) -> ( Ord ( C +o D ) /\ Ord C ) )
36 35 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( Ord ( C +o D ) /\ Ord C ) )
37 36 adantr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( Ord ( C +o D ) /\ Ord C ) )
38 ordeldif 
 |-  ( ( Ord ( C +o D ) /\ Ord C ) -> ( ( C +o X ) e. ( ( C +o D ) \ C ) <-> ( ( C +o X ) e. ( C +o D ) /\ C C_ ( C +o X ) ) ) )
39 37 38 syl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( ( C +o X ) e. ( ( C +o D ) \ C ) <-> ( ( C +o X ) e. ( C +o D ) /\ C C_ ( C +o X ) ) ) )
40 22 29 39 mpbir2and 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( C +o X ) e. ( ( C +o D ) \ C ) )
41 5 15 17 40 fvun2d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) ` ( C +o X ) ) = ( { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ` ( C +o X ) ) )
42 eqid 
 |-  ( C +o X ) = ( C +o X )
43 eqid 
 |-  ( B ` X ) = ( B ` X )
44 oveq2 
 |-  ( z = X -> ( C +o z ) = ( C +o X ) )
45 44 eqeq2d 
 |-  ( z = X -> ( ( C +o X ) = ( C +o z ) <-> ( C +o X ) = ( C +o X ) ) )
46 fveq2 
 |-  ( z = X -> ( B ` z ) = ( B ` X ) )
47 46 eqeq2d 
 |-  ( z = X -> ( ( B ` X ) = ( B ` z ) <-> ( B ` X ) = ( B ` X ) ) )
48 45 47 anbi12d 
 |-  ( z = X -> ( ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) <-> ( ( C +o X ) = ( C +o X ) /\ ( B ` X ) = ( B ` X ) ) ) )
49 48 rspcev 
 |-  ( ( X e. D /\ ( ( C +o X ) = ( C +o X ) /\ ( B ` X ) = ( B ` X ) ) ) -> E. z e. D ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) )
50 42 43 49 mpanr12 
 |-  ( X e. D -> E. z e. D ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) )
51 50 adantl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> E. z e. D ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) )
52 ovex 
 |-  ( C +o X ) e. _V
53 fvex 
 |-  ( B ` X ) e. _V
54 52 53 pm3.2i 
 |-  ( ( C +o X ) e. _V /\ ( B ` X ) e. _V )
55 eleq1 
 |-  ( x = ( C +o X ) -> ( x e. ( ( C +o D ) \ C ) <-> ( C +o X ) e. ( ( C +o D ) \ C ) ) )
56 eqeq1 
 |-  ( x = ( C +o X ) -> ( x = ( C +o z ) <-> ( C +o X ) = ( C +o z ) ) )
57 56 anbi1d 
 |-  ( x = ( C +o X ) -> ( ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> ( ( C +o X ) = ( C +o z ) /\ y = ( B ` z ) ) ) )
58 57 rexbidv 
 |-  ( x = ( C +o X ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> E. z e. D ( ( C +o X ) = ( C +o z ) /\ y = ( B ` z ) ) ) )
59 55 58 anbi12d 
 |-  ( x = ( C +o X ) -> ( ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) <-> ( ( C +o X ) e. ( ( C +o D ) \ C ) /\ E. z e. D ( ( C +o X ) = ( C +o z ) /\ y = ( B ` z ) ) ) ) )
60 eqeq1 
 |-  ( y = ( B ` X ) -> ( y = ( B ` z ) <-> ( B ` X ) = ( B ` z ) ) )
61 60 anbi2d 
 |-  ( y = ( B ` X ) -> ( ( ( C +o X ) = ( C +o z ) /\ y = ( B ` z ) ) <-> ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) ) )
62 61 rexbidv 
 |-  ( y = ( B ` X ) -> ( E. z e. D ( ( C +o X ) = ( C +o z ) /\ y = ( B ` z ) ) <-> E. z e. D ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) ) )
63 62 anbi2d 
 |-  ( y = ( B ` X ) -> ( ( ( C +o X ) e. ( ( C +o D ) \ C ) /\ E. z e. D ( ( C +o X ) = ( C +o z ) /\ y = ( B ` z ) ) ) <-> ( ( C +o X ) e. ( ( C +o D ) \ C ) /\ E. z e. D ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) ) ) )
64 59 63 opelopabg 
 |-  ( ( ( C +o X ) e. _V /\ ( B ` X ) e. _V ) -> ( <. ( C +o X ) , ( B ` X ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } <-> ( ( C +o X ) e. ( ( C +o D ) \ C ) /\ E. z e. D ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) ) ) )
65 54 64 mp1i 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( <. ( C +o X ) , ( B ` X ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } <-> ( ( C +o X ) e. ( ( C +o D ) \ C ) /\ E. z e. D ( ( C +o X ) = ( C +o z ) /\ ( B ` X ) = ( B ` z ) ) ) ) )
66 40 51 65 mpbir2and 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> <. ( C +o X ) , ( B ` X ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } )
67 fnopfvb 
 |-  ( ( { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } Fn ( ( C +o D ) \ C ) /\ ( C +o X ) e. ( ( C +o D ) \ C ) ) -> ( ( { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ` ( C +o X ) ) = ( B ` X ) <-> <. ( C +o X ) , ( B ` X ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) )
68 15 40 67 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( ( { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ` ( C +o X ) ) = ( B ` X ) <-> <. ( C +o X ) , ( B ` X ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) )
69 66 68 mpbird 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ` ( C +o X ) ) = ( B ` X ) )
70 4 41 69 3eqtrd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. D ) -> ( ( A .+ B ) ` ( C +o X ) ) = ( B ` X ) )