Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  saddisj Structured version   Visualization version   GIF version

 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.)
Hypotheses
Ref Expression
saddisj.3 (𝜑 → (𝐴𝐵) = ∅)
Assertion
Ref Expression

Dummy variables 𝑘 𝑐 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 saddisj.1 . . . . 5 (𝜑𝐴 ⊆ ℕ0)
2 saddisj.2 . . . . 5 (𝜑𝐵 ⊆ ℕ0)
3 sadcl 15022 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0)
41, 2, 3syl2anc 691 . . . 4 (𝜑 → (𝐴 sadd 𝐵) ⊆ ℕ0)
54sseld 3567 . . 3 (𝜑 → (𝑘 ∈ (𝐴 sadd 𝐵) → 𝑘 ∈ ℕ0))
61, 2unssd 3751 . . . 4 (𝜑 → (𝐴𝐵) ⊆ ℕ0)
76sseld 3567 . . 3 (𝜑 → (𝑘 ∈ (𝐴𝐵) → 𝑘 ∈ ℕ0))
81adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝐴 ⊆ ℕ0)
92adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ⊆ ℕ0)
10 saddisj.3 . . . . . 6 (𝜑 → (𝐴𝐵) = ∅)
1110adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝐵) = ∅)
12 eqid 2610 . . . . 5 seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑥 − 1)))) = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑥 − 1))))
13 simpr 476 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
148, 9, 11, 12, 13saddisjlem 15024 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝑘 ∈ (𝐴 sadd 𝐵) ↔ 𝑘 ∈ (𝐴𝐵)))
1514ex 449 . . 3 (𝜑 → (𝑘 ∈ ℕ0 → (𝑘 ∈ (𝐴 sadd 𝐵) ↔ 𝑘 ∈ (𝐴𝐵))))
165, 7, 15pm5.21ndd 368 . 2 (𝜑 → (𝑘 ∈ (𝐴 sadd 𝐵) ↔ 𝑘 ∈ (𝐴𝐵)))
1716eqrdv 2608 1 (𝜑 → (𝐴 sadd 𝐵) = (𝐴𝐵))