Metamath Proof Explorer

Theorem tfsconcatb0

Description: The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 25-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 tfsconcatb0 
|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( B = (/) <-> ( A .+ B ) = A ) )

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 fnrel 
 |-  ( B Fn D -> Rel B )
3 reldm0 
 |-  ( Rel B -> ( B = (/) <-> dom B = (/) ) )
4 2 3 syl 
 |-  ( B Fn D -> ( B = (/) <-> dom B = (/) ) )
5 fndm 
 |-  ( B Fn D -> dom B = D )
6 5 eqeq1d 
 |-  ( B Fn D -> ( dom B = (/) <-> D = (/) ) )
7 4 6 bitrd 
 |-  ( B Fn D -> ( B = (/) <-> D = (/) ) )
8 7 ad2antlr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( B = (/) <-> D = (/) ) )
9 rex0 
 |-  -. E. z e. (/) ( x = ( C +o z ) /\ y = ( B ` z ) )
10 rexeq 
 |-  ( D = (/) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> E. z e. (/) ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
11 10 adantl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ D = (/) ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> E. z e. (/) ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
12 9 11 mtbiri 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ D = (/) ) -> -. E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) )
13 12 intnand 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ D = (/) ) -> -. ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
14 13 alrimivv 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ D = (/) ) -> A. x A. y -. ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
15 opab0 
 |-  ( { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = (/) <-> A. x A. y -. ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) )
16 14 15 sylibr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ D = (/) ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = (/) )
17 0ss 
 |-  (/) C_ A
18 16 17 eqsstrdi 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ D = (/) ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } C_ A )
19 18 ex 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( D = (/) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } C_ A ) )
20 df-1o 
 |-  1o = suc (/)
21 simpl 
 |-  ( ( D e. On /\ -. D = (/) ) -> D e. On )
22 on0eln0 
 |-  ( D e. On -> ( (/) e. D <-> D =/= (/) ) )
23 df-ne 
 |-  ( D =/= (/) <-> -. D = (/) )
24 22 23 bitrdi 
 |-  ( D e. On -> ( (/) e. D <-> -. D = (/) ) )
25 24 biimpar 
 |-  ( ( D e. On /\ -. D = (/) ) -> (/) e. D )
26 onsucss 
 |-  ( D e. On -> ( (/) e. D -> suc (/) C_ D ) )
27 21 25 26 sylc 
 |-  ( ( D e. On /\ -. D = (/) ) -> suc (/) C_ D )
28 20 27 eqsstrid 
 |-  ( ( D e. On /\ -. D = (/) ) -> 1o C_ D )
29 28 ex 
 |-  ( D e. On -> ( -. D = (/) -> 1o C_ D ) )
30 29 adantl 
 |-  ( ( C e. On /\ D e. On ) -> ( -. D = (/) -> 1o C_ D ) )
31 30 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( -. D = (/) -> 1o C_ D ) )
32 simpr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> 1o C_ D )
33 0lt1o 
 |-  (/) e. 1o
34 33 a1i 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> (/) e. 1o )
35 32 34 sseldd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> (/) e. D )
36 oaord1 
 |-  ( ( C e. On /\ D e. On ) -> ( (/) e. D <-> C e. ( C +o D ) ) )
37 36 ad2antlr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> ( (/) e. D <-> C e. ( C +o D ) ) )
38 35 37 mpbid 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> C e. ( C +o D ) )
39 ssidd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> C C_ C )
40 oacl 
 |-  ( ( C e. On /\ D e. On ) -> ( C +o D ) e. On )
41 eloni 
 |-  ( ( C +o D ) e. On -> Ord ( C +o D ) )
42 40 41 syl 
 |-  ( ( C e. On /\ D e. On ) -> Ord ( C +o D ) )
43 eloni 
 |-  ( C e. On -> Ord C )
44 43 adantr 
 |-  ( ( C e. On /\ D e. On ) -> Ord C )
45 42 44 jca 
 |-  ( ( C e. On /\ D e. On ) -> ( Ord ( C +o D ) /\ Ord C ) )
46 45 ad2antlr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> ( Ord ( C +o D ) /\ Ord C ) )
47 ordeldif 
 |-  ( ( Ord ( C +o D ) /\ Ord C ) -> ( C e. ( ( C +o D ) \ C ) <-> ( C e. ( C +o D ) /\ C C_ C ) ) )
48 46 47 syl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> ( C e. ( ( C +o D ) \ C ) <-> ( C e. ( C +o D ) /\ C C_ C ) ) )
49 38 39 48 mpbir2and 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> C e. ( ( C +o D ) \ C ) )
50 simpl 
 |-  ( ( C e. On /\ D e. On ) -> C e. On )
51 50 ad2antlr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> C e. On )
52 oa0 
 |-  ( C e. On -> ( C +o (/) ) = C )
53 51 52 syl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> ( C +o (/) ) = C )
54 53 eqcomd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> C = ( C +o (/) ) )
55 eqidd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> ( B ` (/) ) = ( B ` (/) ) )
56 54 55 jca 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> ( C = ( C +o (/) ) /\ ( B ` (/) ) = ( B ` (/) ) ) )
57 oveq2 
 |-  ( z = (/) -> ( C +o z ) = ( C +o (/) ) )
58 57 eqeq2d 
 |-  ( z = (/) -> ( C = ( C +o z ) <-> C = ( C +o (/) ) ) )
59 fveq2 
 |-  ( z = (/) -> ( B ` z ) = ( B ` (/) ) )
60 59 eqeq2d 
 |-  ( z = (/) -> ( ( B ` (/) ) = ( B ` z ) <-> ( B ` (/) ) = ( B ` (/) ) ) )
61 58 60 anbi12d 
 |-  ( z = (/) -> ( ( C = ( C +o z ) /\ ( B ` (/) ) = ( B ` z ) ) <-> ( C = ( C +o (/) ) /\ ( B ` (/) ) = ( B ` (/) ) ) ) )
62 61 rspcev 
 |-  ( ( (/) e. D /\ ( C = ( C +o (/) ) /\ ( B ` (/) ) = ( B ` (/) ) ) ) -> E. z e. D ( C = ( C +o z ) /\ ( B ` (/) ) = ( B ` z ) ) )
63 35 56 62 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> E. z e. D ( C = ( C +o z ) /\ ( B ` (/) ) = ( B ` z ) ) )
64 fvexd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> ( B ` (/) ) e. _V )
65 eleq1 
 |-  ( x = C -> ( x e. ( ( C +o D ) \ C ) <-> C e. ( ( C +o D ) \ C ) ) )
66 65 adantr 
 |-  ( ( x = C /\ y = ( B ` (/) ) ) -> ( x e. ( ( C +o D ) \ C ) <-> C e. ( ( C +o D ) \ C ) ) )
67 eqeq1 
 |-  ( x = C -> ( x = ( C +o z ) <-> C = ( C +o z ) ) )
68 eqeq1 
 |-  ( y = ( B ` (/) ) -> ( y = ( B ` z ) <-> ( B ` (/) ) = ( B ` z ) ) )
69 67 68 bi2anan9 
 |-  ( ( x = C /\ y = ( B ` (/) ) ) -> ( ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> ( C = ( C +o z ) /\ ( B ` (/) ) = ( B ` z ) ) ) )
70 69 rexbidv 
 |-  ( ( x = C /\ y = ( B ` (/) ) ) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> E. z e. D ( C = ( C +o z ) /\ ( B ` (/) ) = ( B ` z ) ) ) )
71 66 70 anbi12d 
 |-  ( ( x = C /\ y = ( B ` (/) ) ) -> ( ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) <-> ( C e. ( ( C +o D ) \ C ) /\ E. z e. D ( C = ( C +o z ) /\ ( B ` (/) ) = ( B ` z ) ) ) ) )
72 71 opelopabga 
 |-  ( ( C e. On /\ ( B ` (/) ) e. _V ) -> ( <. C , ( B ` (/) ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } <-> ( C e. ( ( C +o D ) \ C ) /\ E. z e. D ( C = ( C +o z ) /\ ( B ` (/) ) = ( B ` z ) ) ) ) )
73 51 64 72 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> ( <. C , ( B ` (/) ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } <-> ( C e. ( ( C +o D ) \ C ) /\ E. z e. D ( C = ( C +o z ) /\ ( B ` (/) ) = ( B ` z ) ) ) ) )
74 49 63 73 mpbir2and 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ 1o C_ D ) -> <. C , ( B ` (/) ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } )
75 74 ex 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( 1o C_ D -> <. C , ( B ` (/) ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) )
76 ordirr 
 |-  ( Ord C -> -. C e. C )
77 43 76 syl 
 |-  ( C e. On -> -. C e. C )
78 77 adantr 
 |-  ( ( C e. On /\ D e. On ) -> -. C e. C )
79 78 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> -. C e. C )
80 fndm 
 |-  ( A Fn C -> dom A = C )
81 80 adantr 
 |-  ( ( A Fn C /\ B Fn D ) -> dom A = C )
82 81 adantr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> dom A = C )
83 79 82 neleqtrrd 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> -. C e. dom A )
84 50 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> C e. On )
85 fvexd 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( B ` (/) ) e. _V )
86 84 85 opeldmd 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( <. C , ( B ` (/) ) >. e. A -> C e. dom A ) )
87 83 86 mtod 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> -. <. C , ( B ` (/) ) >. e. A )
88 75 87 jctird 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( 1o C_ D -> ( <. C , ( B ` (/) ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } /\ -. <. C , ( B ` (/) ) >. e. A ) ) )
89 nelss 
 |-  ( ( <. C , ( B ` (/) ) >. e. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } /\ -. <. C , ( B ` (/) ) >. e. A ) -> -. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } C_ A )
90 88 89 syl6 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( 1o C_ D -> -. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } C_ A ) )
91 31 90 syld 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( -. D = (/) -> -. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } C_ A ) )
92 19 91 impcon4bid 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( D = (/) <-> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } C_ A ) )
93 8 92 bitrd 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( B = (/) <-> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } C_ A ) )
94 ssequn2 
 |-  ( { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } C_ A <-> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = A )
95 93 94 bitrdi 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( B = (/) <-> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = A ) )
96 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 ) ) ) } ) )
97 96 eqeq1d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( A .+ B ) = A <-> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = A ) )
98 95 97 bitr4d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( B = (/) <-> ( A .+ B ) = A ) )