Metamath Proof Explorer

Theorem tfsconcat0i

Description: The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 28-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 tfsconcat0i 
|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( 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 simpr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ A = (/) ) -> A = (/) )
3 fnrel 
 |-  ( A Fn C -> Rel A )
4 reldm0 
 |-  ( Rel A -> ( A = (/) <-> dom A = (/) ) )
5 3 4 syl 
 |-  ( A Fn C -> ( A = (/) <-> dom A = (/) ) )
6 fndm 
 |-  ( A Fn C -> dom A = C )
7 6 eqeq1d 
 |-  ( A Fn C -> ( dom A = (/) <-> C = (/) ) )
8 5 7 bitrd 
 |-  ( A Fn C -> ( A = (/) <-> C = (/) ) )
9 8 ad2antrr 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A = (/) <-> C = (/) ) )
10 simpr 
 |-  ( ( A Fn C /\ B Fn D ) -> B Fn D )
11 simpr 
 |-  ( ( C e. On /\ D e. On ) -> D e. On )
12 10 11 anim12i 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( B Fn D /\ D e. On ) )
13 12 anim1i 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ C = (/) ) -> ( ( B Fn D /\ D e. On ) /\ C = (/) ) )
14 9 13 sylbida 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ A = (/) ) -> ( ( B Fn D /\ D e. On ) /\ C = (/) ) )
15 oveq1 
 |-  ( C = (/) -> ( C +o D ) = ( (/) +o D ) )
16 id 
 |-  ( C = (/) -> C = (/) )
17 15 16 difeq12d 
 |-  ( C = (/) -> ( ( C +o D ) \ C ) = ( ( (/) +o D ) \ (/) ) )
18 dif0 
 |-  ( ( (/) +o D ) \ (/) ) = ( (/) +o D )
19 17 18 eqtrdi 
 |-  ( C = (/) -> ( ( C +o D ) \ C ) = ( (/) +o D ) )
20 19 eleq2d 
 |-  ( C = (/) -> ( x e. ( ( C +o D ) \ C ) <-> x e. ( (/) +o D ) ) )
21 oveq1 
 |-  ( C = (/) -> ( C +o z ) = ( (/) +o z ) )
22 21 eqeq2d 
 |-  ( C = (/) -> ( x = ( C +o z ) <-> x = ( (/) +o z ) ) )
23 22 anbi1d 
 |-  ( C = (/) -> ( ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> ( x = ( (/) +o z ) /\ y = ( B ` z ) ) ) )
24 23 rexbidv 
 |-  ( C = (/) -> ( E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) <-> E. z e. D ( x = ( (/) +o z ) /\ y = ( B ` z ) ) ) )
25 20 24 anbi12d 
 |-  ( C = (/) -> ( ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) <-> ( x e. ( (/) +o D ) /\ E. z e. D ( x = ( (/) +o z ) /\ y = ( B ` z ) ) ) ) )
26 oa0r 
 |-  ( D e. On -> ( (/) +o D ) = D )
27 26 eleq2d 
 |-  ( D e. On -> ( x e. ( (/) +o D ) <-> x e. D ) )
28 onelon 
 |-  ( ( D e. On /\ z e. D ) -> z e. On )
29 oa0r 
 |-  ( z e. On -> ( (/) +o z ) = z )
30 29 eqeq2d 
 |-  ( z e. On -> ( x = ( (/) +o z ) <-> x = z ) )
31 30 anbi1d 
 |-  ( z e. On -> ( ( x = ( (/) +o z ) /\ y = ( B ` z ) ) <-> ( x = z /\ y = ( B ` z ) ) ) )
32 28 31 syl 
 |-  ( ( D e. On /\ z e. D ) -> ( ( x = ( (/) +o z ) /\ y = ( B ` z ) ) <-> ( x = z /\ y = ( B ` z ) ) ) )
33 32 rexbidva 
 |-  ( D e. On -> ( E. z e. D ( x = ( (/) +o z ) /\ y = ( B ` z ) ) <-> E. z e. D ( x = z /\ y = ( B ` z ) ) ) )
34 27 33 anbi12d 
 |-  ( D e. On -> ( ( x e. ( (/) +o D ) /\ E. z e. D ( x = ( (/) +o z ) /\ y = ( B ` z ) ) ) <-> ( x e. D /\ E. z e. D ( x = z /\ y = ( B ` z ) ) ) ) )
35 df-rex 
 |-  ( E. z e. D ( x = z /\ y = ( B ` z ) ) <-> E. z ( z e. D /\ ( x = z /\ y = ( B ` z ) ) ) )
36 an12 
 |-  ( ( z e. D /\ ( x = z /\ y = ( B ` z ) ) ) <-> ( x = z /\ ( z e. D /\ y = ( B ` z ) ) ) )
37 eqcom 
 |-  ( x = z <-> z = x )
38 37 anbi1i 
 |-  ( ( x = z /\ ( z e. D /\ y = ( B ` z ) ) ) <-> ( z = x /\ ( z e. D /\ y = ( B ` z ) ) ) )
39 36 38 bitri 
 |-  ( ( z e. D /\ ( x = z /\ y = ( B ` z ) ) ) <-> ( z = x /\ ( z e. D /\ y = ( B ` z ) ) ) )
40 39 exbii 
 |-  ( E. z ( z e. D /\ ( x = z /\ y = ( B ` z ) ) ) <-> E. z ( z = x /\ ( z e. D /\ y = ( B ` z ) ) ) )
41 eleq1w 
 |-  ( z = x -> ( z e. D <-> x e. D ) )
42 fveq2 
 |-  ( z = x -> ( B ` z ) = ( B ` x ) )
43 42 eqeq2d 
 |-  ( z = x -> ( y = ( B ` z ) <-> y = ( B ` x ) ) )
44 41 43 anbi12d 
 |-  ( z = x -> ( ( z e. D /\ y = ( B ` z ) ) <-> ( x e. D /\ y = ( B ` x ) ) ) )
45 44 equsexvw 
 |-  ( E. z ( z = x /\ ( z e. D /\ y = ( B ` z ) ) ) <-> ( x e. D /\ y = ( B ` x ) ) )
46 35 40 45 3bitri 
 |-  ( E. z e. D ( x = z /\ y = ( B ` z ) ) <-> ( x e. D /\ y = ( B ` x ) ) )
47 46 baib 
 |-  ( x e. D -> ( E. z e. D ( x = z /\ y = ( B ` z ) ) <-> y = ( B ` x ) ) )
48 47 adantl 
 |-  ( ( B Fn D /\ x e. D ) -> ( E. z e. D ( x = z /\ y = ( B ` z ) ) <-> y = ( B ` x ) ) )
49 eqcom 
 |-  ( y = ( B ` x ) <-> ( B ` x ) = y )
50 48 49 bitrdi 
 |-  ( ( B Fn D /\ x e. D ) -> ( E. z e. D ( x = z /\ y = ( B ` z ) ) <-> ( B ` x ) = y ) )
51 fnbrfvb 
 |-  ( ( B Fn D /\ x e. D ) -> ( ( B ` x ) = y <-> x B y ) )
52 50 51 bitrd 
 |-  ( ( B Fn D /\ x e. D ) -> ( E. z e. D ( x = z /\ y = ( B ` z ) ) <-> x B y ) )
53 52 pm5.32da 
 |-  ( B Fn D -> ( ( x e. D /\ E. z e. D ( x = z /\ y = ( B ` z ) ) ) <-> ( x e. D /\ x B y ) ) )
54 fnbr 
 |-  ( ( B Fn D /\ x B y ) -> x e. D )
55 54 ex 
 |-  ( B Fn D -> ( x B y -> x e. D ) )
56 55 pm4.71rd 
 |-  ( B Fn D -> ( x B y <-> ( x e. D /\ x B y ) ) )
57 df-br 
 |-  ( x B y <-> <. x , y >. e. B )
58 56 57 bitr3di 
 |-  ( B Fn D -> ( ( x e. D /\ x B y ) <-> <. x , y >. e. B ) )
59 53 58 bitrd 
 |-  ( B Fn D -> ( ( x e. D /\ E. z e. D ( x = z /\ y = ( B ` z ) ) ) <-> <. x , y >. e. B ) )
60 34 59 sylan9bbr 
 |-  ( ( B Fn D /\ D e. On ) -> ( ( x e. ( (/) +o D ) /\ E. z e. D ( x = ( (/) +o z ) /\ y = ( B ` z ) ) ) <-> <. x , y >. e. B ) )
61 25 60 sylan9bbr 
 |-  ( ( ( B Fn D /\ D e. On ) /\ C = (/) ) -> ( ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) <-> <. x , y >. e. B ) )
62 61 opabbidv 
 |-  ( ( ( B Fn D /\ D e. On ) /\ C = (/) ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = { <. x , y >. | <. x , y >. e. B } )
63 14 62 syl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ A = (/) ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = { <. x , y >. | <. x , y >. e. B } )
64 fnrel 
 |-  ( B Fn D -> Rel B )
65 opabid2 
 |-  ( Rel B -> { <. x , y >. | <. x , y >. e. B } = B )
66 64 65 syl 
 |-  ( B Fn D -> { <. x , y >. | <. x , y >. e. B } = B )
67 66 adantl 
 |-  ( ( A Fn C /\ B Fn D ) -> { <. x , y >. | <. x , y >. e. B } = B )
68 67 ad2antrr 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ A = (/) ) -> { <. x , y >. | <. x , y >. e. B } = B )
69 63 68 eqtrd 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ A = (/) ) -> { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } = B )
70 2 69 uneq12d 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ A = (/) ) -> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = ( (/) u. B ) )
71 0un 
 |-  ( (/) u. B ) = B
72 70 71 eqtrdi 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ A = (/) ) -> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = B )
73 72 ex 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A = (/) -> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = B ) )
74 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 ) ) ) } ) )
75 74 eqeq1d 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( A .+ B ) = B <-> ( A u. { <. x , y >. | ( x e. ( ( C +o D ) \ C ) /\ E. z e. D ( x = ( C +o z ) /\ y = ( B ` z ) ) ) } ) = B ) )
76 73 75 sylibrd 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A = (/) -> ( A .+ B ) = B ) )