Metamath Proof Explorer

Theorem tfsconcatrev

Description: If the domain of a transfinite sequence is an ordinal sum, the sequence can be decomposed into two sequences with domains corresponding to the addends. Theorem 2 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-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 tfsconcatrev 
|- ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> E. u e. ( ran F ^m C ) E. v e. ( ran F ^m D ) ( ( u .+ v ) = F /\ dom u = C /\ dom v = 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 dffn3 
 |-  ( F Fn ( C +o D ) <-> F : ( C +o D ) --> ran F )
3 2 biimpi 
 |-  ( F Fn ( C +o D ) -> F : ( C +o D ) --> ran F )
4 3 adantr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> F : ( C +o D ) --> ran F )
5 fndm 
 |-  ( F Fn ( C +o D ) -> dom F = ( C +o D ) )
6 5 adantr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> dom F = ( C +o D ) )
7 oacl 
 |-  ( ( C e. On /\ D e. On ) -> ( C +o D ) e. On )
8 7 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( C +o D ) e. On )
9 6 8 eqeltrd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> dom F e. On )
10 fnfun 
 |-  ( F Fn ( C +o D ) -> Fun F )
11 10 adantr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> Fun F )
12 funrnex 
 |-  ( dom F e. On -> ( Fun F -> ran F e. _V ) )
13 9 11 12 sylc 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ran F e. _V )
14 13 8 elmapd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F e. ( ran F ^m ( C +o D ) ) <-> F : ( C +o D ) --> ran F ) )
15 4 14 mpbird 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> F e. ( ran F ^m ( C +o D ) ) )
16 oaword1 
 |-  ( ( C e. On /\ D e. On ) -> C C_ ( C +o D ) )
17 16 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> C C_ ( C +o D ) )
18 elmapssres 
 |-  ( ( F e. ( ran F ^m ( C +o D ) ) /\ C C_ ( C +o D ) ) -> ( F |` C ) e. ( ran F ^m C ) )
19 15 17 18 syl2anc 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` C ) e. ( ran F ^m C ) )
20 simpl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> F Fn ( C +o D ) )
21 oaordi 
 |-  ( ( D e. On /\ C e. On ) -> ( d e. D -> ( C +o d ) e. ( C +o D ) ) )
22 21 ancoms 
 |-  ( ( C e. On /\ D e. On ) -> ( d e. D -> ( C +o d ) e. ( C +o D ) ) )
23 22 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D -> ( C +o d ) e. ( C +o D ) ) )
24 23 imp 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> ( C +o d ) e. ( C +o D ) )
25 fnfvelrn 
 |-  ( ( F Fn ( C +o D ) /\ ( C +o d ) e. ( C +o D ) ) -> ( F ` ( C +o d ) ) e. ran F )
26 20 24 25 syl2an2r 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> ( F ` ( C +o d ) ) e. ran F )
27 26 fmpttd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D |-> ( F ` ( C +o d ) ) ) : D --> ran F )
28 simprr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> D e. On )
29 13 28 elmapd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( ( d e. D |-> ( F ` ( C +o d ) ) ) e. ( ran F ^m D ) <-> ( d e. D |-> ( F ` ( C +o d ) ) ) : D --> ran F ) )
30 27 29 mpbird 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D |-> ( F ` ( C +o d ) ) ) e. ( ran F ^m D ) )
31 20 17 fnssresd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` C ) Fn C )
32 fvex 
 |-  ( F ` ( C +o d ) ) e. _V
33 eqid 
 |-  ( d e. D |-> ( F ` ( C +o d ) ) ) = ( d e. D |-> ( F ` ( C +o d ) ) )
34 32 33 fnmpti 
 |-  ( d e. D |-> ( F ` ( C +o d ) ) ) Fn D
35 34 a1i 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D |-> ( F ` ( C +o d ) ) ) Fn D )
36 simpr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( C e. On /\ D e. On ) )
37 1 tfsconcatun 
 |-  ( ( ( ( F |` C ) Fn C /\ ( d e. D |-> ( F ` ( C +o d ) ) ) Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = ( ( F |` C ) u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) } ) )
38 31 35 36 37 syl21anc 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = ( ( F |` C ) u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) } ) )
39 oveq2 
 |-  ( d = z -> ( C +o d ) = ( C +o z ) )
40 39 fveq2d 
 |-  ( d = z -> ( F ` ( C +o d ) ) = ( F ` ( C +o z ) ) )
41 fvex 
 |-  ( F ` ( C +o z ) ) e. _V
42 40 33 41 fvmpt 
 |-  ( z e. D -> ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) = ( F ` ( C +o z ) ) )
43 42 ad2antlr 
 |-  ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) = ( F ` ( C +o z ) ) )
44 fveq2 
 |-  ( x = ( C +o z ) -> ( F ` x ) = ( F ` ( C +o z ) ) )
45 44 adantl 
 |-  ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> ( F ` x ) = ( F ` ( C +o z ) ) )
46 43 45 eqtr4d 
 |-  ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) = ( F ` x ) )
47 46 eqeq2d 
 |-  ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> ( y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) <-> y = ( F ` x ) ) )
48 47 biimpd 
 |-  ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ z e. D ) /\ x = ( C +o z ) ) -> ( y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) -> y = ( F ` x ) ) )
49 48 expimpd 
 |-  ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ z e. D ) -> ( ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) -> y = ( F ` x ) ) )
50 49 rexlimdva 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) -> y = ( F ` x ) ) )
51 simplr 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( C e. On /\ D e. On ) )
52 eloni 
 |-  ( ( C +o D ) e. On -> Ord ( C +o D ) )
53 7 52 syl 
 |-  ( ( C e. On /\ D e. On ) -> Ord ( C +o D ) )
54 eloni 
 |-  ( C e. On -> Ord C )
55 54 adantr 
 |-  ( ( C e. On /\ D e. On ) -> Ord C )
56 ordeldif 
 |-  ( ( Ord ( C +o D ) /\ Ord C ) -> ( x e. ( ( C +o D ) \ C ) <-> ( x e. ( C +o D ) /\ C C_ x ) ) )
57 53 55 56 syl2anc 
 |-  ( ( C e. On /\ D e. On ) -> ( x e. ( ( C +o D ) \ C ) <-> ( x e. ( C +o D ) /\ C C_ x ) ) )
58 57 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( x e. ( ( C +o D ) \ C ) <-> ( x e. ( C +o D ) /\ C C_ x ) ) )
59 58 biimpa 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( x e. ( C +o D ) /\ C C_ x ) )
60 59 ancomd 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( C C_ x /\ x e. ( C +o D ) ) )
61 51 60 jca 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( ( C e. On /\ D e. On ) /\ ( C C_ x /\ x e. ( C +o D ) ) ) )
62 61 adantr 
 |-  ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) -> ( ( C e. On /\ D e. On ) /\ ( C C_ x /\ x e. ( C +o D ) ) ) )
63 oawordex2 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( C C_ x /\ x e. ( C +o D ) ) ) -> E. z e. D ( C +o z ) = x )
64 62 63 syl 
 |-  ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) -> E. z e. D ( C +o z ) = x )
65 simpr 
 |-  ( ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) /\ z e. D ) /\ ( C +o z ) = x ) -> ( C +o z ) = x )
66 65 eqcomd 
 |-  ( ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) /\ z e. D ) /\ ( C +o z ) = x ) -> x = ( C +o z ) )
67 65 fveq2d 
 |-  ( ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) /\ z e. D ) /\ ( C +o z ) = x ) -> ( F ` ( C +o z ) ) = ( F ` x ) )
68 42 ad2antlr 
 |-  ( ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) /\ z e. D ) /\ ( C +o z ) = x ) -> ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) = ( F ` ( C +o z ) ) )
69 simpllr 
 |-  ( ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) /\ z e. D ) /\ ( C +o z ) = x ) -> y = ( F ` x ) )
70 67 68 69 3eqtr4rd 
 |-  ( ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) /\ z e. D ) /\ ( C +o z ) = x ) -> y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) )
71 66 70 jca 
 |-  ( ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) /\ z e. D ) /\ ( C +o z ) = x ) -> ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) )
72 71 ex 
 |-  ( ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) /\ z e. D ) -> ( ( C +o z ) = x -> ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) )
73 72 reximdva 
 |-  ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) -> ( E. z e. D ( C +o z ) = x -> E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) )
74 64 73 mpd 
 |-  ( ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) /\ y = ( F ` x ) ) -> E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) )
75 74 ex 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( y = ( F ` x ) -> E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) )
76 50 75 impbid 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) <-> y = ( F ` x ) ) )
77 eldifi 
 |-  ( x e. ( ( C +o D ) \ C ) -> x e. ( C +o D ) )
78 eqcom 
 |-  ( y = ( F ` x ) <-> ( F ` x ) = y )
79 fnbrfvb 
 |-  ( ( F Fn ( C +o D ) /\ x e. ( C +o D ) ) -> ( ( F ` x ) = y <-> x F y ) )
80 78 79 bitrid 
 |-  ( ( F Fn ( C +o D ) /\ x e. ( C +o D ) ) -> ( y = ( F ` x ) <-> x F y ) )
81 20 77 80 syl2an 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( y = ( F ` x ) <-> x F y ) )
82 76 81 bitrd 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) <-> x F y ) )
83 82 pm5.32da 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) <-> ( x e. ( ( C +o D ) \ C ) /\ x F y ) ) )
84 83 opabbidv 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) } = { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ x F y ) } )
85 dfres2 
 |-  ( F |` ( ( C +o D ) \ C ) ) = { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ x F y ) }
86 84 85 eqtr4di 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) } = ( F |` ( ( C +o D ) \ C ) ) )
87 86 uneq2d 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( ( F |` C ) u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) ) ) } ) = ( ( F |` C ) u. ( F |` ( ( C +o D ) \ C ) ) ) )
88 38 87 eqtrd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = ( ( F |` C ) u. ( F |` ( ( C +o D ) \ C ) ) ) )
89 resundi 
 |-  ( F |` ( C u. ( ( C +o D ) \ C ) ) ) = ( ( F |` C ) u. ( F |` ( ( C +o D ) \ C ) ) )
90 89 a1i 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` ( C u. ( ( C +o D ) \ C ) ) ) = ( ( F |` C ) u. ( F |` ( ( C +o D ) \ C ) ) ) )
91 undif 
 |-  ( C C_ ( C +o D ) <-> ( C u. ( ( C +o D ) \ C ) ) = ( C +o D ) )
92 16 91 sylib 
 |-  ( ( C e. On /\ D e. On ) -> ( C u. ( ( C +o D ) \ C ) ) = ( C +o D ) )
93 92 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( C u. ( ( C +o D ) \ C ) ) = ( C +o D ) )
94 93 reseq2d 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` ( C u. ( ( C +o D ) \ C ) ) ) = ( F |` ( C +o D ) ) )
95 fnresdm 
 |-  ( F Fn ( C +o D ) -> ( F |` ( C +o D ) ) = F )
96 95 adantr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` ( C +o D ) ) = F )
97 94 96 eqtrd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` ( C u. ( ( C +o D ) \ C ) ) ) = F )
98 88 90 97 3eqtr2d 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = F )
99 dmres 
 |-  dom ( F |` C ) = ( C i^i dom F )
100 17 6 sseqtrrd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> C C_ dom F )
101 dfss2 
 |-  ( C C_ dom F <-> ( C i^i dom F ) = C )
102 100 101 sylib 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( C i^i dom F ) = C )
103 99 102 eqtrid 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> dom ( F |` C ) = C )
104 32 33 dmmpti 
 |-  dom ( d e. D |-> ( F ` ( C +o d ) ) ) = D
105 104 a1i 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> dom ( d e. D |-> ( F ` ( C +o d ) ) ) = D )
106 oveq1 
 |-  ( u = ( F |` C ) -> ( u .+ v ) = ( ( F |` C ) .+ v ) )
107 106 eqeq1d 
 |-  ( u = ( F |` C ) -> ( ( u .+ v ) = F <-> ( ( F |` C ) .+ v ) = F ) )
108 dmeq 
 |-  ( u = ( F |` C ) -> dom u = dom ( F |` C ) )
109 108 eqeq1d 
 |-  ( u = ( F |` C ) -> ( dom u = C <-> dom ( F |` C ) = C ) )
110 107 109 3anbi12d 
 |-  ( u = ( F |` C ) -> ( ( ( u .+ v ) = F /\ dom u = C /\ dom v = D ) <-> ( ( ( F |` C ) .+ v ) = F /\ dom ( F |` C ) = C /\ dom v = D ) ) )
111 oveq2 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> ( ( F |` C ) .+ v ) = ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) )
112 111 eqeq1d 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> ( ( ( F |` C ) .+ v ) = F <-> ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = F ) )
113 dmeq 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> dom v = dom ( d e. D |-> ( F ` ( C +o d ) ) ) )
114 113 eqeq1d 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> ( dom v = D <-> dom ( d e. D |-> ( F ` ( C +o d ) ) ) = D ) )
115 112 114 3anbi13d 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> ( ( ( ( F |` C ) .+ v ) = F /\ dom ( F |` C ) = C /\ dom v = D ) <-> ( ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = F /\ dom ( F |` C ) = C /\ dom ( d e. D |-> ( F ` ( C +o d ) ) ) = D ) ) )
116 110 115 rspc2ev 
 |-  ( ( ( F |` C ) e. ( ran F ^m C ) /\ ( d e. D |-> ( F ` ( C +o d ) ) ) e. ( ran F ^m D ) /\ ( ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = F /\ dom ( F |` C ) = C /\ dom ( d e. D |-> ( F ` ( C +o d ) ) ) = D ) ) -> E. u e. ( ran F ^m C ) E. v e. ( ran F ^m D ) ( ( u .+ v ) = F /\ dom u = C /\ dom v = D ) )
117 19 30 98 103 105 116 syl113anc 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> E. u e. ( ran F ^m C ) E. v e. ( ran F ^m D ) ( ( u .+ v ) = F /\ dom u = C /\ dom v = D ) )