Metamath Proof Explorer

Theorem tfsconcatrn

Description: The range of the concatenation of two transfinite series. (Contributed by RP, 24-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 tfsconcatrn 
|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran ( A .+ B ) = ( ran A u. ran B ) )

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 rneqd 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran ( A .+ B ) = ran ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) )
4 rnun 
 |-  ran ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = ( ran A u. ran { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } )
5 4 a1i 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = ( ran A u. ran { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) )
6 df-rex 
 |-  ( E. x e. ( ( C +o D ) \ C ) E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> E. x ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
7 pm3.22 
 |-  ( ( C e. On /\ D e. On ) -> ( D e. On /\ C e. On ) )
8 7 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( D e. On /\ C e. On ) )
9 oaordi 
 |-  ( ( D e. On /\ C e. On ) -> ( d e. D -> ( C +o d ) e. ( C +o D ) ) )
10 8 9 syl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D -> ( C +o d ) e. ( C +o D ) ) )
11 10 imp 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> ( C +o d ) e. ( C +o D ) )
12 simplrl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> C e. On )
13 simprr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> D e. On )
14 onelon 
 |-  ( ( D e. On /\ d e. D ) -> d e. On )
15 13 14 sylan 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> d e. On )
16 oaword1 
 |-  ( ( C e. On /\ d e. On ) -> C C_ ( C +o d ) )
17 12 15 16 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> C C_ ( C +o d ) )
18 oacl 
 |-  ( ( C e. On /\ D e. On ) -> ( C +o D ) e. On )
19 18 ad2antlr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> ( C +o D ) e. On )
20 eloni 
 |-  ( ( C +o D ) e. On -> Ord ( C +o D ) )
21 19 20 syl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> Ord ( C +o D ) )
22 eloni 
 |-  ( C e. On -> Ord C )
23 12 22 syl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> Ord C )
24 ordeldif 
 |-  ( ( Ord ( C +o D ) /\ Ord C ) -> ( ( C +o d ) e. ( ( C +o D ) \ C ) <-> ( ( C +o d ) e. ( C +o D ) /\ C C_ ( C +o d ) ) ) )
25 21 23 24 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> ( ( C +o d ) e. ( ( C +o D ) \ C ) <-> ( ( C +o d ) e. ( C +o D ) /\ C C_ ( C +o d ) ) ) )
26 11 17 25 mpbir2and 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> ( C +o d ) e. ( ( C +o D ) \ C ) )
27 simpr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( C e. On /\ D e. On ) )
28 27 adantr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( C e. On /\ D e. On ) )
29 18 20 syl 
 |-  ( ( C e. On /\ D e. On ) -> Ord ( C +o D ) )
30 22 adantr 
 |-  ( ( C e. On /\ D e. On ) -> Ord C )
31 29 30 jca 
 |-  ( ( C e. On /\ D e. On ) -> ( Ord ( C +o D ) /\ Ord C ) )
32 31 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( Ord ( C +o D ) /\ Ord C ) )
33 ordeldif 
 |-  ( ( Ord ( C +o D ) /\ Ord C ) -> ( x e. ( ( C +o D ) \ C ) <-> ( x e. ( C +o D ) /\ C C_ x ) ) )
34 32 33 syl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( x e. ( ( C +o D ) \ C ) <-> ( x e. ( C +o D ) /\ C C_ x ) ) )
35 34 biimpa 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( x e. ( C +o D ) /\ C C_ x ) )
36 35 ancomd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( C C_ x /\ x e. ( C +o D ) ) )
37 oawordex2 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( C C_ x /\ x e. ( C +o D ) ) ) -> E. d e. D ( C +o d ) = x )
38 28 36 37 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> E. d e. D ( C +o d ) = x )
39 eqcom 
 |-  ( ( C +o d ) = x <-> x = ( C +o d ) )
40 39 rexbii 
 |-  ( E. d e. D ( C +o d ) = x <-> E. d e. D x = ( C +o d ) )
41 38 40 sylib 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> E. d e. D x = ( C +o d ) )
42 simpr 
 |-  ( ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> x = ( C +o z ) )
43 simpll3 
 |-  ( ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> x = ( C +o d ) )
44 42 43 eqtr3d 
 |-  ( ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> ( C +o z ) = ( C +o d ) )
45 simp1rl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> C e. On )
46 45 adantr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) -> C e. On )
47 simp1rr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> D e. On )
48 onelon 
 |-  ( ( D e. On /\ z e. D ) -> z e. On )
49 47 48 sylan 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) -> z e. On )
50 simp2 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> d e. D )
51 47 50 14 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> d e. On )
52 51 adantr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) -> d e. On )
53 46 49 52 3jca 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) -> ( C e. On /\ z e. On /\ d e. On ) )
54 53 adantr 
 |-  ( ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> ( C e. On /\ z e. On /\ d e. On ) )
55 oacan 
 |-  ( ( C e. On /\ z e. On /\ d e. On ) -> ( ( C +o z ) = ( C +o d ) <-> z = d ) )
56 54 55 syl 
 |-  ( ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> ( ( C +o z ) = ( C +o d ) <-> z = d ) )
57 44 56 mpbid 
 |-  ( ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> z = d )
58 velsn 
 |-  ( z e. { d } <-> z = d )
59 57 58 sylibr 
 |-  ( ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> z e. { d } )
60 59 ex 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) -> ( x = ( C +o z ) -> z e. { d } ) )
61 60 adantrd 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ z e. D ) -> ( ( x = ( C +o z ) /\ y = ( B ` z ) ) -> z e. { d } ) )
62 61 expimpd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> ( ( z e. D /\ ( x = ( C +o z ) /\ y = ( B ` z ) ) ) -> z e. { d } ) )
63 simprr 
 |-  ( ( z e. D /\ ( x = ( C +o z ) /\ y = ( B ` z ) ) ) -> y = ( B ` z ) )
64 62 63 jca2 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> ( ( z e. D /\ ( x = ( C +o z ) /\ y = ( B ` z ) ) ) -> ( z e. { d } /\ y = ( B ` z ) ) ) )
65 64 reximdv2 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) -> E. z e. { d } y = ( B ` z ) ) )
66 vex 
 |-  d e. _V
67 fveq2 
 |-  ( z = d -> ( B ` z ) = ( B ` d ) )
68 67 eqeq2d 
 |-  ( z = d -> ( y = ( B ` z ) <-> y = ( B ` d ) ) )
69 66 68 rexsn 
 |-  ( E. z e. { d } y = ( B ` z ) <-> y = ( B ` d ) )
70 65 69 imbitrdi 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) -> y = ( B ` d ) ) )
71 50 adantr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ y = ( B ` d ) ) -> d e. D )
72 simpl3 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ y = ( B ` d ) ) -> x = ( C +o d ) )
73 simpr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ y = ( B ` d ) ) -> y = ( B ` d ) )
74 oveq2 
 |-  ( z = d -> ( C +o z ) = ( C +o d ) )
75 74 eqeq2d 
 |-  ( z = d -> ( x = ( C +o z ) <-> x = ( C +o d ) ) )
76 75 68 anbi12d 
 |-  ( z = d -> ( ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> ( x = ( C +o d ) /\ y = ( B ` d ) ) ) )
77 76 rspcev 
 |-  ( ( d e. D /\ ( x = ( C +o d ) /\ y = ( B ` d ) ) ) -> E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) )
78 71 72 73 77 syl12anc 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) /\ y = ( B ` d ) ) -> E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) )
79 78 ex 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> ( y = ( B ` d ) -> E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
80 70 79 impbid 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D /\ x = ( C +o d ) ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> y = ( B ` d ) ) )
81 26 41 80 rexxfrd2 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( E. x e. ( ( C +o D ) \ C ) E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> E. d e. D y = ( B ` d ) ) )
82 6 81 bitr3id 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( E. x ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) <-> E. d e. D y = ( B ` d ) ) )
83 82 abbidv 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> { y | E. x ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = { y | E. d e. D y = ( B ` d ) } )
84 rnopab 
 |-  ran { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = { y | E. x ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) }
85 84 a1i 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = { y | E. x ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } )
86 fnrnfv 
 |-  ( B Fn D -> ran B = { y | E. d e. D y = ( B ` d ) } )
87 86 ad2antlr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran B = { y | E. d e. D y = ( B ` d ) } )
88 83 85 87 3eqtr4d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = ran B )
89 88 uneq2d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ran A u. ran { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = ( ran A u. ran B ) )
90 3 5 89 3eqtrd 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran ( A .+ B ) = ( ran A u. ran B ) )