Theorem iundisjcnt

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

	Ref	Expression
Hypotheses	iundisjcnt.0	⊢ Ⅎ 𝑛 𝐵
	iundisjcnt.1	⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
	iundisjcnt.2	⊢ ( 𝜑 → ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝑀 ) ) )
Assertion	iundisjcnt	⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		iundisjcnt.0	⊢ Ⅎ 𝑛 𝐵
2		iundisjcnt.1	⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
3		iundisjcnt.2	⊢ ( 𝜑 → ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝑀 ) ) )
4		nfcv	⊢ Ⅎ 𝑘 𝐴
5	4 1 2	iundisjf	⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑁 = ℕ ) → 𝑁 = ℕ )
7	6	iuneq1d	⊢ ( ( 𝜑 ∧ 𝑁 = ℕ ) → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ ℕ 𝐴 )
8	6	iuneq1d	⊢ ( ( 𝜑 ∧ 𝑁 = ℕ ) → ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ∪ 𝑛 ∈ ℕ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
9	5 7 8	3eqtr4a	⊢ ( ( 𝜑 ∧ 𝑁 = ℕ ) → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
10	1 2	iundisjfi	⊢ ∪ 𝑛 ∈ ( 1 ..^ 𝑀 ) 𝐴 = ∪ 𝑛 ∈ ( 1 ..^ 𝑀 ) ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → 𝑁 = ( 1 ..^ 𝑀 ) )
12	11	iuneq1d	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ ( 1 ..^ 𝑀 ) 𝐴 )
13	11	iuneq1d	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) = ∪ 𝑛 ∈ ( 1 ..^ 𝑀 ) ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
14	10 12 13	3eqtr4a	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
15	9 14 3	mpjaodan	⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )