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 birani 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> F : ( C +o D ) --> ran F )
4 fndm 
 |-  ( F Fn ( C +o D ) -> dom F = ( C +o D ) )
5 4 adantr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> dom F = ( C +o D ) )
6 oacl 
 |-  ( ( C e. On /\ D e. On ) -> ( C +o D ) e. On )
7 6 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( C +o D ) e. On )
8 5 7 eqeltrd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> dom F e. On )
9 fnfun 
 |-  ( F Fn ( C +o D ) -> Fun F )
10 9 adantr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> Fun F )
11 funrnex 
 |-  ( dom F e. On -> ( Fun F -> ran F e. _V ) )
12 8 10 11 sylc 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ran F e. _V )
13 12 7 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 ) )
14 3 13 mpbird 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> F e. ( ran F ^m ( C +o D ) ) )
15 oaword1 
 |-  ( ( C e. On /\ D e. On ) -> C C_ ( C +o D ) )
16 15 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> C C_ ( C +o D ) )
17 elmapssres 
 |-  ( ( F e. ( ran F ^m ( C +o D ) ) /\ C C_ ( C +o D ) ) -> ( F |` C ) e. ( ran F ^m C ) )
18 14 16 17 syl2anc 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` C ) e. ( ran F ^m C ) )
19 simpl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> F Fn ( C +o D ) )
20 oaordi 
 |-  ( ( D e. On /\ C e. On ) -> ( d e. D -> ( C +o d ) e. ( C +o D ) ) )
21 20 ancoms 
 |-  ( ( C e. On /\ D e. On ) -> ( d e. D -> ( C +o d ) e. ( C +o D ) ) )
22 21 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D -> ( C +o d ) e. ( C +o D ) ) )
23 22 imp 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> ( C +o d ) e. ( C +o D ) )
24 fnfvelrn 
 |-  ( ( F Fn ( C +o D ) /\ ( C +o d ) e. ( C +o D ) ) -> ( F ` ( C +o d ) ) e. ran F )
25 19 23 24 syl2an2r 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ d e. D ) -> ( F ` ( C +o d ) ) e. ran F )
26 25 fmpttd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D |-> ( F ` ( C +o d ) ) ) : D --> ran F )
27 simprr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> D e. On )
28 12 27 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 ) )
29 26 28 mpbird 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D |-> ( F ` ( C +o d ) ) ) e. ( ran F ^m D ) )
30 19 16 fnssresd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` C ) Fn C )
31 fvex 
 |-  ( F ` ( C +o d ) ) e. _V
32 eqid 
 |-  ( d e. D |-> ( F ` ( C +o d ) ) ) = ( d e. D |-> ( F ` ( C +o d ) ) )
33 31 32 fnmpti 
 |-  ( d e. D |-> ( F ` ( C +o d ) ) ) Fn D
34 33 a1i 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( d e. D |-> ( F ` ( C +o d ) ) ) Fn D )
35 simpr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( C e. On /\ D e. On ) )
36 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 ) ) ) } ) )
37 30 34 35 36 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 ) ) ) } ) )
38 oveq2 
 |-  ( d = z -> ( C +o d ) = ( C +o z ) )
39 38 fveq2d 
 |-  ( d = z -> ( F ` ( C +o d ) ) = ( F ` ( C +o z ) ) )
40 fvex 
 |-  ( F ` ( C +o z ) ) e. _V
41 39 32 40 fvmpt 
 |-  ( z e. D -> ( ( d e. D |-> ( F ` ( C +o d ) ) ) ` z ) = ( F ` ( C +o z ) ) )
42 41 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 ) ) )
43 fveq2 
 |-  ( x = ( C +o z ) -> ( F ` x ) = ( F ` ( C +o z ) ) )
44 43 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 ) ) )
45 42 44 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 ) )
46 45 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 ) ) )
47 46 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 ) ) )
48 47 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 ) ) )
49 48 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 ) ) )
50 simplr 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( C e. On /\ D e. On ) )
51 eloni 
 |-  ( ( C +o D ) e. On -> Ord ( C +o D ) )
52 6 51 syl 
 |-  ( ( C e. On /\ D e. On ) -> Ord ( C +o D ) )
53 eloni 
 |-  ( C e. On -> Ord C )
54 53 adantr 
 |-  ( ( C e. On /\ D e. On ) -> Ord C )
55 ordeldif 
 |-  ( ( Ord ( C +o D ) /\ Ord C ) -> ( x e. ( ( C +o D ) \ C ) <-> ( x e. ( C +o D ) /\ C C_ x ) ) )
56 52 54 55 syl2anc 
 |-  ( ( C e. On /\ D e. On ) -> ( x e. ( ( C +o D ) \ C ) <-> ( x e. ( C +o D ) /\ C C_ x ) ) )
57 56 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 ) ) )
58 57 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 ) )
59 58 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 ) ) )
60 50 59 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 ) ) ) )
61 60 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 ) ) ) )
62 oawordex2 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( C C_ x /\ x e. ( C +o D ) ) ) -> E. z e. D ( C +o z ) = x )
63 61 62 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 )
64 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 )
65 64 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 ) )
66 64 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 ) )
67 41 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 ) ) )
68 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 ) )
69 66 67 68 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 ) )
70 65 69 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 ) ) )
71 70 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 ) ) ) )
72 71 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 ) ) ) )
73 63 72 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 ) ) )
74 73 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 ) ) ) )
75 49 74 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 ) ) )
76 eldifi 
 |-  ( x e. ( ( C +o D ) \ C ) -> x e. ( C +o D ) )
77 eqcom 
 |-  ( y = ( F ` x ) <-> ( F ` x ) = y )
78 fnbrfvb 
 |-  ( ( F Fn ( C +o D ) /\ x e. ( C +o D ) ) -> ( ( F ` x ) = y <-> x F y ) )
79 77 78 bitrid 
 |-  ( ( F Fn ( C +o D ) /\ x e. ( C +o D ) ) -> ( y = ( F ` x ) <-> x F y ) )
80 19 76 79 syl2an 
 |-  ( ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) /\ x e. ( ( C +o D ) \ C ) ) -> ( y = ( F ` x ) <-> x F y ) )
81 75 80 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 ) )
82 81 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 ) ) )
83 82 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 ) } )
84 dfres2 
 |-  ( F |` ( ( C +o D ) \ C ) ) = { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ x F y ) }
85 83 84 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 ) ) )
86 85 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 ) ) ) )
87 37 86 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 ) ) ) )
88 resundi 
 |-  ( F |` ( C u. ( ( C +o D ) \ C ) ) ) = ( ( F |` C ) u. ( F |` ( ( C +o D ) \ C ) ) )
89 88 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 ) ) ) )
90 undif 
 |-  ( C C_ ( C +o D ) <-> ( C u. ( ( C +o D ) \ C ) ) = ( C +o D ) )
91 15 90 sylib 
 |-  ( ( C e. On /\ D e. On ) -> ( C u. ( ( C +o D ) \ C ) ) = ( C +o D ) )
92 91 adantl 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( C u. ( ( C +o D ) \ C ) ) = ( C +o D ) )
93 92 reseq2d 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` ( C u. ( ( C +o D ) \ C ) ) ) = ( F |` ( C +o D ) ) )
94 fnresdm 
 |-  ( F Fn ( C +o D ) -> ( F |` ( C +o D ) ) = F )
95 94 adantr 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` ( C +o D ) ) = F )
96 93 95 eqtrd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( F |` ( C u. ( ( C +o D ) \ C ) ) ) = F )
97 87 89 96 3eqtr2d 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = F )
98 dmres 
 |-  dom ( F |` C ) = ( C i^i dom F )
99 16 5 sseqtrrd 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> C C_ dom F )
100 dfss2 
 |-  ( C C_ dom F <-> ( C i^i dom F ) = C )
101 99 100 sylib 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> ( C i^i dom F ) = C )
102 98 101 eqtrid 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> dom ( F |` C ) = C )
103 31 32 dmmpti 
 |-  dom ( d e. D |-> ( F ` ( C +o d ) ) ) = D
104 103 a1i 
 |-  ( ( F Fn ( C +o D ) /\ ( C e. On /\ D e. On ) ) -> dom ( d e. D |-> ( F ` ( C +o d ) ) ) = D )
105 oveq1 
 |-  ( u = ( F |` C ) -> ( u .+ v ) = ( ( F |` C ) .+ v ) )
106 105 eqeq1d 
 |-  ( u = ( F |` C ) -> ( ( u .+ v ) = F <-> ( ( F |` C ) .+ v ) = F ) )
107 dmeq 
 |-  ( u = ( F |` C ) -> dom u = dom ( F |` C ) )
108 107 eqeq1d 
 |-  ( u = ( F |` C ) -> ( dom u = C <-> dom ( F |` C ) = C ) )
109 106 108 3anbi12d 
 |-  ( u = ( F |` C ) -> ( ( ( u .+ v ) = F /\ dom u = C /\ dom v = D ) <-> ( ( ( F |` C ) .+ v ) = F /\ dom ( F |` C ) = C /\ dom v = D ) ) )
110 oveq2 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> ( ( F |` C ) .+ v ) = ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) )
111 110 eqeq1d 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> ( ( ( F |` C ) .+ v ) = F <-> ( ( F |` C ) .+ ( d e. D |-> ( F ` ( C +o d ) ) ) ) = F ) )
112 dmeq 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> dom v = dom ( d e. D |-> ( F ` ( C +o d ) ) ) )
113 112 eqeq1d 
 |-  ( v = ( d e. D |-> ( F ` ( C +o d ) ) ) -> ( dom v = D <-> dom ( d e. D |-> ( F ` ( C +o d ) ) ) = D ) )
114 111 113 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 ) ) )
115 109 114 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 ) )
116 18 29 97 102 104 115 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 ) )