Metamath Proof Explorer

Theorem iundisj2cnt

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

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

Proof

Step Hyp Ref Expression
1 iundisj2cnt.0 ⊢ Ⅎ _ n B
2 iundisj2cnt.1 ⊢ n = k → A = B
3 iundisj2cnt.2 ⊢ φ → N = ℕ ∨ N = 1 ..^ M
4 nfcv ⊢ Ⅎ _ k A
5 4 1 2 iundisj2f ⊢ Disj n ∈ ℕ A ∖ ⋃ k ∈ 1 ..^ n B
6 disjeq1 ⊢ N = ℕ → Disj n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B ↔ Disj n ∈ ℕ A ∖ ⋃ k ∈ 1 ..^ n B
7 5 6 mpbiri ⊢ N = ℕ → Disj n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B
8 1 2 iundisj2fi ⊢ Disj n ∈ 1 ..^ M A ∖ ⋃ k ∈ 1 ..^ n B
9 disjeq1 ⊢ N = 1 ..^ M → Disj n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B ↔ Disj n ∈ 1 ..^ M A ∖ ⋃ k ∈ 1 ..^ n B
10 8 9 mpbiri ⊢ N = 1 ..^ M → Disj n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B
11 7 10 jaoi ⊢ N = ℕ ∨ N = 1 ..^ M → Disj n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B
12 3 11 syl ⊢ φ → Disj n ∈ N A ∖ ⋃ k ∈ 1 ..^ n B