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

Proof

Step Hyp Ref Expression
1 tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2 nnon ⊢ ( 𝐷 ∈ ω → 𝐷 ∈ On )
3 2 anim2i ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) )
4 3 anim2i ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) )
5 1 tfsconcat0i ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ → ( 𝐴 + 𝐵 ) = 𝐵 ) )
6 4 5 syl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( 𝐴 = ∅ → ( 𝐴 + 𝐵 ) = 𝐵 ) )
7 dmeq ⊢ ( ( 𝐴 + 𝐵 ) = 𝐵 → dom ( 𝐴 + 𝐵 ) = dom 𝐵 )
8 nna0r ⊢ ( 𝐷 ∈ ω → ( ∅ +o 𝐷 ) = 𝐷 )
9 8 adantl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ∅ +o 𝐷 ) = 𝐷 )
10 9 eqeq2d ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ( 𝐶 +o 𝐷 ) = ( ∅ +o 𝐷 ) ↔ ( 𝐶 +o 𝐷 ) = 𝐷 ) )
11 eqcom ⊢ ( ( 𝐶 +o 𝐷 ) = ( ∅ +o 𝐷 ) ↔ ( ∅ +o 𝐷 ) = ( 𝐶 +o 𝐷 ) )
12 10 11 bitr3di ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ( 𝐶 +o 𝐷 ) = 𝐷 ↔ ( ∅ +o 𝐷 ) = ( 𝐶 +o 𝐷 ) ) )
13 on0eln0 ⊢ ( 𝐶 ∈ On → ( ∅ ∈ 𝐶 ↔ 𝐶 ≠ ∅ ) )
14 13 adantr ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ∅ ∈ 𝐶 ↔ 𝐶 ≠ ∅ ) )
15 df-ne ⊢ ( 𝐶 ≠ ∅ ↔ ¬ 𝐶 = ∅ )
16 14 15 bitr2di ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ¬ 𝐶 = ∅ ↔ ∅ ∈ 𝐶 ) )
17 peano1 ⊢ ∅ ∈ ω
18 nnaordr ⊢ ( ( ∅ ∈ ω ∧ 𝐶 ∈ ω ∧ 𝐷 ∈ ω ) → ( ∅ ∈ 𝐶 ↔ ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) )
19 17 18 mp3an1 ⊢ ( ( 𝐶 ∈ ω ∧ 𝐷 ∈ ω ) → ( ∅ ∈ 𝐶 ↔ ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) )
20 19 biimpd ⊢ ( ( 𝐶 ∈ ω ∧ 𝐷 ∈ ω ) → ( ∅ ∈ 𝐶 → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) )
21 20 ex ⊢ ( 𝐶 ∈ ω → ( 𝐷 ∈ ω → ( ∅ ∈ 𝐶 → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) ) )
22 21 a1i ⊢ ( 𝐶 ∈ On → ( 𝐶 ∈ ω → ( 𝐷 ∈ ω → ( ∅ ∈ 𝐶 → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) ) ) )
23 simpr ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ∧ ω ⊆ 𝐶 ) → ω ⊆ 𝐶 )
24 oaword1 ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → 𝐶 ⊆ ( 𝐶 +o 𝐷 ) )
25 3 24 syl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → 𝐶 ⊆ ( 𝐶 +o 𝐷 ) )
26 25 adantr ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ∧ ω ⊆ 𝐶 ) → 𝐶 ⊆ ( 𝐶 +o 𝐷 ) )
27 23 26 sstrd ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ∧ ω ⊆ 𝐶 ) → ω ⊆ ( 𝐶 +o 𝐷 ) )
28 id ⊢ ( 𝐷 ∈ ω → 𝐷 ∈ ω )
29 8 28 eqeltrd ⊢ ( 𝐷 ∈ ω → ( ∅ +o 𝐷 ) ∈ ω )
30 29 ad2antlr ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ∧ ω ⊆ 𝐶 ) → ( ∅ +o 𝐷 ) ∈ ω )
31 27 30 sseldd ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ∧ ω ⊆ 𝐶 ) → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) )
32 31 a1d ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ∧ ω ⊆ 𝐶 ) → ( ∅ ∈ 𝐶 → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) )
33 32 exp31 ⊢ ( 𝐶 ∈ On → ( 𝐷 ∈ ω → ( ω ⊆ 𝐶 → ( ∅ ∈ 𝐶 → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) ) ) )
34 33 com23 ⊢ ( 𝐶 ∈ On → ( ω ⊆ 𝐶 → ( 𝐷 ∈ ω → ( ∅ ∈ 𝐶 → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) ) ) )
35 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
36 ordom ⊢ Ord ω
37 ordtri2or ⊢ ( ( Ord 𝐶 ∧ Ord ω ) → ( 𝐶 ∈ ω ∨ ω ⊆ 𝐶 ) )
38 35 36 37 sylancl ⊢ ( 𝐶 ∈ On → ( 𝐶 ∈ ω ∨ ω ⊆ 𝐶 ) )
39 22 34 38 mpjaod ⊢ ( 𝐶 ∈ On → ( 𝐷 ∈ ω → ( ∅ ∈ 𝐶 → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) ) )
40 39 imp ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ∅ ∈ 𝐶 → ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) ) )
41 elneq ⊢ ( ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) → ( ∅ +o 𝐷 ) ≠ ( 𝐶 +o 𝐷 ) )
42 41 neneqd ⊢ ( ( ∅ +o 𝐷 ) ∈ ( 𝐶 +o 𝐷 ) → ¬ ( ∅ +o 𝐷 ) = ( 𝐶 +o 𝐷 ) )
43 40 42 syl6 ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ∅ ∈ 𝐶 → ¬ ( ∅ +o 𝐷 ) = ( 𝐶 +o 𝐷 ) ) )
44 16 43 sylbid ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ¬ 𝐶 = ∅ → ¬ ( ∅ +o 𝐷 ) = ( 𝐶 +o 𝐷 ) ) )
45 44 con4d ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ( ∅ +o 𝐷 ) = ( 𝐶 +o 𝐷 ) → 𝐶 = ∅ ) )
46 12 45 sylbid ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) → ( ( 𝐶 +o 𝐷 ) = 𝐷 → 𝐶 = ∅ ) )
47 46 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( ( 𝐶 +o 𝐷 ) = 𝐷 → 𝐶 = ∅ ) )
48 1 tfsconcatfn ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) Fn ( 𝐶 +o 𝐷 ) )
49 4 48 syl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( 𝐴 + 𝐵 ) Fn ( 𝐶 +o 𝐷 ) )
50 49 fndmd ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → dom ( 𝐴 + 𝐵 ) = ( 𝐶 +o 𝐷 ) )
51 fndm ⊢ ( 𝐵 Fn 𝐷 → dom 𝐵 = 𝐷 )
52 51 ad2antlr ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → dom 𝐵 = 𝐷 )
53 50 52 eqeq12d ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( dom ( 𝐴 + 𝐵 ) = dom 𝐵 ↔ ( 𝐶 +o 𝐷 ) = 𝐷 ) )
54 fnrel ⊢ ( 𝐴 Fn 𝐶 → Rel 𝐴 )
55 reldm0 ⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ dom 𝐴 = ∅ ) )
56 54 55 syl ⊢ ( 𝐴 Fn 𝐶 → ( 𝐴 = ∅ ↔ dom 𝐴 = ∅ ) )
57 fndm ⊢ ( 𝐴 Fn 𝐶 → dom 𝐴 = 𝐶 )
58 57 eqeq1d ⊢ ( 𝐴 Fn 𝐶 → ( dom 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
59 56 58 bitrd ⊢ ( 𝐴 Fn 𝐶 → ( 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
60 59 adantr ⊢ ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) → ( 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
61 60 adantr ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
62 47 53 61 3imtr4d ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( dom ( 𝐴 + 𝐵 ) = dom 𝐵 → 𝐴 = ∅ ) )
63 7 62 syl5 ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( ( 𝐴 + 𝐵 ) = 𝐵 → 𝐴 = ∅ ) )
64 6 63 impbid ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ ω ) ) → ( 𝐴 = ∅ ↔ ( 𝐴 + 𝐵 ) = 𝐵 ) )