Metamath Proof Explorer

Theorem iundisjcnt

Description: Rewrite a countable union as a disjoint union. (Contributed by Thierry Arnoux, 16-Feb-2017)

Ref Expression
Hypotheses iundisjcnt.0 ⊢ Ⅎ _ n B
iundisjcnt.1 ⊢ n = k → A = B
iundisjcnt.2 ⊢ φ → N = ℕ ∨ N = 1 ..^ M
Assertion iundisjcnt ⊢ φ → ⋃ n ∈ N A = ⋃ n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B

Proof

Step Hyp Ref Expression
1 iundisjcnt.0 ⊢ Ⅎ _ n B
2 iundisjcnt.1 ⊢ n = k → A = B
3 iundisjcnt.2 ⊢ φ → N = ℕ ∨ N = 1 ..^ M
4 nfcv ⊢ Ⅎ _ k A
5 4 1 2 iundisjf ⊢ ⋃ n ∈ ℕ A = ⋃ n ∈ ℕ A ∖ ⋃ k ∈ 1 ..^ n B
6 simpr ⊢ φ ∧ N = ℕ → N = ℕ
7 6 iuneq1d ⊢ φ ∧ N = ℕ → ⋃ n ∈ N A = ⋃ n ∈ ℕ A
8 6 iuneq1d ⊢ φ ∧ N = ℕ → ⋃ n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B = ⋃ n ∈ ℕ A ∖ ⋃ k ∈ 1 ..^ n B
9 5 7 8 3eqtr4a ⊢ φ ∧ N = ℕ → ⋃ n ∈ N A = ⋃ n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B
10 1 2 iundisjfi ⊢ ⋃ n ∈ 1 ..^ M A = ⋃ n ∈ 1 ..^ M A ∖ ⋃ k ∈ 1 ..^ n B
11 simpr ⊢ φ ∧ N = 1 ..^ M → N = 1 ..^ M
12 11 iuneq1d ⊢ φ ∧ N = 1 ..^ M → ⋃ n ∈ N A = ⋃ n ∈ 1 ..^ M A
13 11 iuneq1d ⊢ φ ∧ N = 1 ..^ M → ⋃ n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B = ⋃ n ∈ 1 ..^ M A ∖ ⋃ k ∈ 1 ..^ n B
14 10 12 13 3eqtr4a ⊢ φ ∧ N = 1 ..^ M → ⋃ n ∈ N A = ⋃ n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B
15 9 14 3 mpjaodan ⊢ φ → ⋃ n ∈ N A = ⋃ n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B