iundisjcnt

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

Step	Hyp	Ref	Expression
1		iundisjcnt.0	$⊢ \underline{Ⅎ} n B$
2		iundisjcnt.1	$⊢ n = k \to A = B$
3		iundisjcnt.2	$⊢ φ \to (N = ℕ \lor N = (1 ..^M))$
4		nfcv	$⊢ \underline{Ⅎ} k A$
5	4 1 2	iundisjf	$⊢ ⋃_{n \in ℕ} A = ⋃_{n \in ℕ} (A ∖ ⋃_{k \in (1 ..^n)} B)$
6		simpr	$⊢ (φ \land N = ℕ) \to N = ℕ$
7	6	iuneq1d	$⊢ (φ \land N = ℕ) \to ⋃_{n \in N} A = ⋃_{n \in ℕ} A$
8	6	iuneq1d	$⊢ (φ \land N = ℕ) \to ⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B) = ⋃_{n \in ℕ} (A ∖ ⋃_{k \in (1 ..^n)} B)$
9	5 7 8	3eqtr4a	$⊢ (φ \land N = ℕ) \to ⋃_{n \in N} A = ⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B)$
10	1 2	iundisjfi	$⊢ ⋃_{n \in (1 ..^M)} A = ⋃_{n \in (1 ..^M)} (A ∖ ⋃_{k \in (1 ..^n)} B)$
11		simpr	$⊢ (φ \land N = (1 ..^M)) \to N = (1 ..^M)$
12	11	iuneq1d	$⊢ (φ \land N = (1 ..^M)) \to ⋃_{n \in N} A = ⋃_{n \in (1 ..^M)} A$
13	11	iuneq1d	$⊢ (φ \land N = (1 ..^M)) \to ⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B) = ⋃_{n \in (1 ..^M)} (A ∖ ⋃_{k \in (1 ..^n)} B)$
14	10 12 13	3eqtr4a	$⊢ (φ \land N = (1 ..^M)) \to ⋃_{n \in N} A = ⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B)$
15	9 14 3	mpjaodan	$⊢ φ \to ⋃_{n \in N} A = ⋃_{n \in N} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Metamath Proof Explorer