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 + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏𝑧 ) ) ) } ) )
Assertion tfsconcat0i ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ → ( 𝐴 + 𝐵 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 tfsconcat.op + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏𝑧 ) ) ) } ) )
2 simpr ( ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
3 fnrel ( 𝐴 Fn 𝐶 → Rel 𝐴 )
4 reldm0 ( Rel 𝐴 → ( 𝐴 = ∅ ↔ dom 𝐴 = ∅ ) )
5 3 4 syl ( 𝐴 Fn 𝐶 → ( 𝐴 = ∅ ↔ dom 𝐴 = ∅ ) )
6 fndm ( 𝐴 Fn 𝐶 → dom 𝐴 = 𝐶 )
7 6 eqeq1d ( 𝐴 Fn 𝐶 → ( dom 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
8 5 7 bitrd ( 𝐴 Fn 𝐶 → ( 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
9 8 ad2antrr ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
10 simpr ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) → 𝐵 Fn 𝐷 )
11 simpr ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → 𝐷 ∈ On )
12 10 11 anim12i ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐵 Fn 𝐷𝐷 ∈ On ) )
13 12 anim1i ( ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 = ∅ ) → ( ( 𝐵 Fn 𝐷𝐷 ∈ On ) ∧ 𝐶 = ∅ ) )
14 9 13 sylbida ( ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ( ( 𝐵 Fn 𝐷𝐷 ∈ On ) ∧ 𝐶 = ∅ ) )
15 oveq1 ( 𝐶 = ∅ → ( 𝐶 +o 𝐷 ) = ( ∅ +o 𝐷 ) )
16 id ( 𝐶 = ∅ → 𝐶 = ∅ )
17 15 16 difeq12d ( 𝐶 = ∅ → ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) = ( ( ∅ +o 𝐷 ) ∖ ∅ ) )
18 dif0 ( ( ∅ +o 𝐷 ) ∖ ∅ ) = ( ∅ +o 𝐷 )
19 17 18 eqtrdi ( 𝐶 = ∅ → ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) = ( ∅ +o 𝐷 ) )
20 19 eleq2d ( 𝐶 = ∅ → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ 𝑥 ∈ ( ∅ +o 𝐷 ) ) )
21 oveq1 ( 𝐶 = ∅ → ( 𝐶 +o 𝑧 ) = ( ∅ +o 𝑧 ) )
22 21 eqeq2d ( 𝐶 = ∅ → ( 𝑥 = ( 𝐶 +o 𝑧 ) ↔ 𝑥 = ( ∅ +o 𝑧 ) ) )
23 22 anbi1d ( 𝐶 = ∅ → ( ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ↔ ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) )
24 23 rexbidv ( 𝐶 = ∅ → ( ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ↔ ∃ 𝑧𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) )
25 20 24 anbi12d ( 𝐶 = ∅ → ( ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) ↔ ( 𝑥 ∈ ( ∅ +o 𝐷 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) ) )
26 oa0r ( 𝐷 ∈ On → ( ∅ +o 𝐷 ) = 𝐷 )
27 26 eleq2d ( 𝐷 ∈ On → ( 𝑥 ∈ ( ∅ +o 𝐷 ) ↔ 𝑥𝐷 ) )
28 onelon ( ( 𝐷 ∈ On ∧ 𝑧𝐷 ) → 𝑧 ∈ On )
29 oa0r ( 𝑧 ∈ On → ( ∅ +o 𝑧 ) = 𝑧 )
30 29 eqeq2d ( 𝑧 ∈ On → ( 𝑥 = ( ∅ +o 𝑧 ) ↔ 𝑥 = 𝑧 ) )
31 30 anbi1d ( 𝑧 ∈ On → ( ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ↔ ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) )
32 28 31 syl ( ( 𝐷 ∈ On ∧ 𝑧𝐷 ) → ( ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ↔ ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) )
33 32 rexbidva ( 𝐷 ∈ On → ( ∃ 𝑧𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ↔ ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) )
34 27 33 anbi12d ( 𝐷 ∈ On → ( ( 𝑥 ∈ ( ∅ +o 𝐷 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) ↔ ( 𝑥𝐷 ∧ ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) ) )
35 df-rex ( ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ↔ ∃ 𝑧 ( 𝑧𝐷 ∧ ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) )
36 an12 ( ( 𝑧𝐷 ∧ ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) ↔ ( 𝑥 = 𝑧 ∧ ( 𝑧𝐷𝑦 = ( 𝐵𝑧 ) ) ) )
37 eqcom ( 𝑥 = 𝑧𝑧 = 𝑥 )
38 37 anbi1i ( ( 𝑥 = 𝑧 ∧ ( 𝑧𝐷𝑦 = ( 𝐵𝑧 ) ) ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑧𝐷𝑦 = ( 𝐵𝑧 ) ) ) )
39 36 38 bitri ( ( 𝑧𝐷 ∧ ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑧𝐷𝑦 = ( 𝐵𝑧 ) ) ) )
40 39 exbii ( ∃ 𝑧 ( 𝑧𝐷 ∧ ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( 𝑧𝐷𝑦 = ( 𝐵𝑧 ) ) ) )
41 eleq1w ( 𝑧 = 𝑥 → ( 𝑧𝐷𝑥𝐷 ) )
42 fveq2 ( 𝑧 = 𝑥 → ( 𝐵𝑧 ) = ( 𝐵𝑥 ) )
43 42 eqeq2d ( 𝑧 = 𝑥 → ( 𝑦 = ( 𝐵𝑧 ) ↔ 𝑦 = ( 𝐵𝑥 ) ) )
44 41 43 anbi12d ( 𝑧 = 𝑥 → ( ( 𝑧𝐷𝑦 = ( 𝐵𝑧 ) ) ↔ ( 𝑥𝐷𝑦 = ( 𝐵𝑥 ) ) ) )
45 44 equsexvw ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( 𝑧𝐷𝑦 = ( 𝐵𝑧 ) ) ) ↔ ( 𝑥𝐷𝑦 = ( 𝐵𝑥 ) ) )
46 35 40 45 3bitri ( ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ↔ ( 𝑥𝐷𝑦 = ( 𝐵𝑥 ) ) )
47 46 baib ( 𝑥𝐷 → ( ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ↔ 𝑦 = ( 𝐵𝑥 ) ) )
48 47 adantl ( ( 𝐵 Fn 𝐷𝑥𝐷 ) → ( ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ↔ 𝑦 = ( 𝐵𝑥 ) ) )
49 eqcom ( 𝑦 = ( 𝐵𝑥 ) ↔ ( 𝐵𝑥 ) = 𝑦 )
50 48 49 bitrdi ( ( 𝐵 Fn 𝐷𝑥𝐷 ) → ( ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ↔ ( 𝐵𝑥 ) = 𝑦 ) )
51 fnbrfvb ( ( 𝐵 Fn 𝐷𝑥𝐷 ) → ( ( 𝐵𝑥 ) = 𝑦𝑥 𝐵 𝑦 ) )
52 50 51 bitrd ( ( 𝐵 Fn 𝐷𝑥𝐷 ) → ( ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ↔ 𝑥 𝐵 𝑦 ) )
53 52 pm5.32da ( 𝐵 Fn 𝐷 → ( ( 𝑥𝐷 ∧ ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) ↔ ( 𝑥𝐷𝑥 𝐵 𝑦 ) ) )
54 fnbr ( ( 𝐵 Fn 𝐷𝑥 𝐵 𝑦 ) → 𝑥𝐷 )
55 54 ex ( 𝐵 Fn 𝐷 → ( 𝑥 𝐵 𝑦𝑥𝐷 ) )
56 55 pm4.71rd ( 𝐵 Fn 𝐷 → ( 𝑥 𝐵 𝑦 ↔ ( 𝑥𝐷𝑥 𝐵 𝑦 ) ) )
57 df-br ( 𝑥 𝐵 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
58 56 57 bitr3di ( 𝐵 Fn 𝐷 → ( ( 𝑥𝐷𝑥 𝐵 𝑦 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
59 53 58 bitrd ( 𝐵 Fn 𝐷 → ( ( 𝑥𝐷 ∧ ∃ 𝑧𝐷 ( 𝑥 = 𝑧𝑦 = ( 𝐵𝑧 ) ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
60 34 59 sylan9bbr ( ( 𝐵 Fn 𝐷𝐷 ∈ On ) → ( ( 𝑥 ∈ ( ∅ +o 𝐷 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
61 25 60 sylan9bbr ( ( ( 𝐵 Fn 𝐷𝐷 ∈ On ) ∧ 𝐶 = ∅ ) → ( ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
62 61 opabbidv ( ( ( 𝐵 Fn 𝐷𝐷 ∈ On ) ∧ 𝐶 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } )
63 14 62 syl ( ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } )
64 fnrel ( 𝐵 Fn 𝐷 → Rel 𝐵 )
65 opabid2 ( Rel 𝐵 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } = 𝐵 )
66 64 65 syl ( 𝐵 Fn 𝐷 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } = 𝐵 )
67 66 adantl ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } = 𝐵 )
68 67 ad2antrr ( ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } = 𝐵 )
69 63 68 eqtrd ( ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) } = 𝐵 )
70 2 69 uneq12d ( ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) } ) = ( ∅ ∪ 𝐵 ) )
71 0un ( ∅ ∪ 𝐵 ) = 𝐵
72 70 71 eqtrdi ( ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) } ) = 𝐵 )
73 72 ex ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ → ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) } ) = 𝐵 ) )
74 1 tfsconcatun ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) = ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) } ) )
75 74 eqeq1d ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 + 𝐵 ) = 𝐵 ↔ ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵𝑧 ) ) ) } ) = 𝐵 ) )
76 73 75 sylibrd ( ( ( 𝐴 Fn 𝐶𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ → ( 𝐴 + 𝐵 ) = 𝐵 ) )