Metamath Proof Explorer


Theorem saddisj

Description: The sum of disjoint sequences is the union of the sequences. (In this case, there are no carried bits.) (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses saddisj.1 ( 𝜑𝐴 ⊆ ℕ0 )
saddisj.2 ( 𝜑𝐵 ⊆ ℕ0 )
saddisj.3 ( 𝜑 → ( 𝐴𝐵 ) = ∅ )
Assertion saddisj ( 𝜑 → ( 𝐴 sadd 𝐵 ) = ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 saddisj.1 ( 𝜑𝐴 ⊆ ℕ0 )
2 saddisj.2 ( 𝜑𝐵 ⊆ ℕ0 )
3 saddisj.3 ( 𝜑 → ( 𝐴𝐵 ) = ∅ )
4 sadcl ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
5 1 2 4 syl2anc ( 𝜑 → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
6 5 sseld ( 𝜑 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) → 𝑘 ∈ ℕ0 ) )
7 1 2 unssd ( 𝜑 → ( 𝐴𝐵 ) ⊆ ℕ0 )
8 7 sseld ( 𝜑 → ( 𝑘 ∈ ( 𝐴𝐵 ) → 𝑘 ∈ ℕ0 ) )
9 1 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝐴 ⊆ ℕ0 )
10 2 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝐵 ⊆ ℕ0 )
11 3 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐴𝐵 ) = ∅ )
12 eqid seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚𝐴 , 𝑚𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ∅ , ( 𝑥 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚𝐴 , 𝑚𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , ∅ , ( 𝑥 − 1 ) ) ) )
13 simpr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
14 9 10 11 12 13 saddisjlem ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴𝐵 ) ) )
15 14 ex ( 𝜑 → ( 𝑘 ∈ ℕ0 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴𝐵 ) ) ) )
16 6 8 15 pm5.21ndd ( 𝜑 → ( 𝑘 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑘 ∈ ( 𝐴𝐵 ) ) )
17 16 eqrdv ( 𝜑 → ( 𝐴 sadd 𝐵 ) = ( 𝐴𝐵 ) )