Theorem iundisj2cnt

Description: A countable disjoint union is disjoint. Cf. iundisj2 . (Contributed by Thierry Arnoux, 16-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		iundisj2cnt.0	⊢ Ⅎ 𝑛 𝐵
2		iundisj2cnt.1	⊢ ( 𝑛 = 𝑘 → 𝐴 = 𝐵 )
3		iundisj2cnt.2	⊢ ( 𝜑 → ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝑀 ) ) )
4		nfcv	⊢ Ⅎ 𝑘 𝐴
5	4 1 2	iundisj2f	⊢ Disj 𝑛 ∈ ℕ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )
6		disjeq1	⊢ ( 𝑁 = ℕ → ( Disj 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ↔ Disj 𝑛 ∈ ℕ ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )
7	5 6	mpbiri	⊢ ( 𝑁 = ℕ → Disj 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
8	1 2	iundisj2fi	⊢ Disj 𝑛 ∈ ( 1 ..^ 𝑀 ) ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 )
9		disjeq1	⊢ ( 𝑁 = ( 1 ..^ 𝑀 ) → ( Disj 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ↔ Disj 𝑛 ∈ ( 1 ..^ 𝑀 ) ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) ) )
10	8 9	mpbiri	⊢ ( 𝑁 = ( 1 ..^ 𝑀 ) → Disj 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
11	7 10	jaoi	⊢ ( ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝑀 ) ) → Disj 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )
12	3 11	syl	⊢ ( 𝜑 → Disj 𝑛 ∈ 𝑁 ( 𝐴 ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝐵 ) )