Metamath Proof Explorer

Theorem tfsconcat0b

Description: The concatentation with the empty series leaves the finite series unchanged. (Contributed by RP, 1-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 tfsconcat0b 
|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( A = (/) <-> ( A .+ B ) = 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 nnon 
 |-  ( D e. _om -> D e. On )
3 2 anim2i 
 |-  ( ( C e. On /\ D e. _om ) -> ( C e. On /\ D e. On ) )
4 3 anim2i 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) )
5 1 tfsconcat0i 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A = (/) -> ( A .+ B ) = B ) )
6 4 5 syl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( A = (/) -> ( A .+ B ) = B ) )
7 dmeq 
 |-  ( ( A .+ B ) = B -> dom ( A .+ B ) = dom B )
8 nna0r 
 |-  ( D e. _om -> ( (/) +o D ) = D )
9 8 adantl 
 |-  ( ( C e. On /\ D e. _om ) -> ( (/) +o D ) = D )
10 9 eqeq2d 
 |-  ( ( C e. On /\ D e. _om ) -> ( ( C +o D ) = ( (/) +o D ) <-> ( C +o D ) = D ) )
11 eqcom 
 |-  ( ( C +o D ) = ( (/) +o D ) <-> ( (/) +o D ) = ( C +o D ) )
12 10 11 bitr3di 
 |-  ( ( C e. On /\ D e. _om ) -> ( ( C +o D ) = D <-> ( (/) +o D ) = ( C +o D ) ) )
13 on0eln0 
 |-  ( C e. On -> ( (/) e. C <-> C =/= (/) ) )
14 13 adantr 
 |-  ( ( C e. On /\ D e. _om ) -> ( (/) e. C <-> C =/= (/) ) )
15 df-ne 
 |-  ( C =/= (/) <-> -. C = (/) )
16 14 15 bitr2di 
 |-  ( ( C e. On /\ D e. _om ) -> ( -. C = (/) <-> (/) e. C ) )
17 peano1 
 |-  (/) e. _om
18 nnaordr 
 |-  ( ( (/) e. _om /\ C e. _om /\ D e. _om ) -> ( (/) e. C <-> ( (/) +o D ) e. ( C +o D ) ) )
19 17 18 mp3an1 
 |-  ( ( C e. _om /\ D e. _om ) -> ( (/) e. C <-> ( (/) +o D ) e. ( C +o D ) ) )
20 19 biimpd 
 |-  ( ( C e. _om /\ D e. _om ) -> ( (/) e. C -> ( (/) +o D ) e. ( C +o D ) ) )
21 20 ex 
 |-  ( C e. _om -> ( D e. _om -> ( (/) e. C -> ( (/) +o D ) e. ( C +o D ) ) ) )
22 21 a1i 
 |-  ( C e. On -> ( C e. _om -> ( D e. _om -> ( (/) e. C -> ( (/) +o D ) e. ( C +o D ) ) ) ) )
23 simpr 
 |-  ( ( ( C e. On /\ D e. _om ) /\ _om C_ C ) -> _om C_ C )
24 oaword1 
 |-  ( ( C e. On /\ D e. On ) -> C C_ ( C +o D ) )
25 3 24 syl 
 |-  ( ( C e. On /\ D e. _om ) -> C C_ ( C +o D ) )
26 25 adantr 
 |-  ( ( ( C e. On /\ D e. _om ) /\ _om C_ C ) -> C C_ ( C +o D ) )
27 23 26 sstrd 
 |-  ( ( ( C e. On /\ D e. _om ) /\ _om C_ C ) -> _om C_ ( C +o D ) )
28 id 
 |-  ( D e. _om -> D e. _om )
29 8 28 eqeltrd 
 |-  ( D e. _om -> ( (/) +o D ) e. _om )
30 29 ad2antlr 
 |-  ( ( ( C e. On /\ D e. _om ) /\ _om C_ C ) -> ( (/) +o D ) e. _om )
31 27 30 sseldd 
 |-  ( ( ( C e. On /\ D e. _om ) /\ _om C_ C ) -> ( (/) +o D ) e. ( C +o D ) )
32 31 a1d 
 |-  ( ( ( C e. On /\ D e. _om ) /\ _om C_ C ) -> ( (/) e. C -> ( (/) +o D ) e. ( C +o D ) ) )
33 32 exp31 
 |-  ( C e. On -> ( D e. _om -> ( _om C_ C -> ( (/) e. C -> ( (/) +o D ) e. ( C +o D ) ) ) ) )
34 33 com23 
 |-  ( C e. On -> ( _om C_ C -> ( D e. _om -> ( (/) e. C -> ( (/) +o D ) e. ( C +o D ) ) ) ) )
35 eloni 
 |-  ( C e. On -> Ord C )
36 ordom 
 |-  Ord _om
37 ordtri2or 
 |-  ( ( Ord C /\ Ord _om ) -> ( C e. _om \/ _om C_ C ) )
38 35 36 37 sylancl 
 |-  ( C e. On -> ( C e. _om \/ _om C_ C ) )
39 22 34 38 mpjaod 
 |-  ( C e. On -> ( D e. _om -> ( (/) e. C -> ( (/) +o D ) e. ( C +o D ) ) ) )
40 39 imp 
 |-  ( ( C e. On /\ D e. _om ) -> ( (/) e. C -> ( (/) +o D ) e. ( C +o D ) ) )
41 elneq 
 |-  ( ( (/) +o D ) e. ( C +o D ) -> ( (/) +o D ) =/= ( C +o D ) )
42 41 neneqd 
 |-  ( ( (/) +o D ) e. ( C +o D ) -> -. ( (/) +o D ) = ( C +o D ) )
43 40 42 syl6 
 |-  ( ( C e. On /\ D e. _om ) -> ( (/) e. C -> -. ( (/) +o D ) = ( C +o D ) ) )
44 16 43 sylbid 
 |-  ( ( C e. On /\ D e. _om ) -> ( -. C = (/) -> -. ( (/) +o D ) = ( C +o D ) ) )
45 44 con4d 
 |-  ( ( C e. On /\ D e. _om ) -> ( ( (/) +o D ) = ( C +o D ) -> C = (/) ) )
46 12 45 sylbid 
 |-  ( ( C e. On /\ D e. _om ) -> ( ( C +o D ) = D -> C = (/) ) )
47 46 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( ( C +o D ) = D -> C = (/) ) )
48 1 tfsconcatfn 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A .+ B ) Fn ( C +o D ) )
49 4 48 syl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( A .+ B ) Fn ( C +o D ) )
50 49 fndmd 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> dom ( A .+ B ) = ( C +o D ) )
51 fndm 
 |-  ( B Fn D -> dom B = D )
52 51 ad2antlr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> dom B = D )
53 50 52 eqeq12d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( dom ( A .+ B ) = dom B <-> ( C +o D ) = D ) )
54 fnrel 
 |-  ( A Fn C -> Rel A )
55 reldm0 
 |-  ( Rel A -> ( A = (/) <-> dom A = (/) ) )
56 54 55 syl 
 |-  ( A Fn C -> ( A = (/) <-> dom A = (/) ) )
57 fndm 
 |-  ( A Fn C -> dom A = C )
58 57 eqeq1d 
 |-  ( A Fn C -> ( dom A = (/) <-> C = (/) ) )
59 56 58 bitrd 
 |-  ( A Fn C -> ( A = (/) <-> C = (/) ) )
60 59 adantr 
 |-  ( ( A Fn C /\ B Fn D ) -> ( A = (/) <-> C = (/) ) )
61 60 adantr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( A = (/) <-> C = (/) ) )
62 47 53 61 3imtr4d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( dom ( A .+ B ) = dom B -> A = (/) ) )
63 7 62 syl5 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( ( A .+ B ) = B -> A = (/) ) )
64 6 63 impbid 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. _om ) ) -> ( A = (/) <-> ( A .+ B ) = B ) )