Theorem iundisj2cnt

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

	Ref	Expression
Hypotheses	iundisj2cnt.0	$$⊢\underset{\_}{Ⅎ}nB$$
	iundisj2cnt.1	$$⊢n=k\to A=B$$
	iundisj2cnt.2	$$⊢\phi \to \left(N=\mathbb{N}\vee N=\left(1..^M\right)\right)$$
Assertion	iundisj2cnt	$$⊢\phi \to \underset{n\in N}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		iundisj2cnt.0	$$⊢\underset{\_}{Ⅎ}nB$$
2		iundisj2cnt.1	$$⊢n=k\to A=B$$
3		iundisj2cnt.2	$$⊢\phi \to \left(N=\mathbb{N}\vee N=\left(1..^M\right)\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
5	4 1 2	iundisj2f	$$⊢\underset{n\in \mathbb{N}}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)$$
6		disjeq1	$$⊢N=\mathbb{N}\to \left(\underset{n\in N}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)\leftrightarrow \underset{n\in \mathbb{N}}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)\right)$$
7	5 6	mpbiri	$$⊢N=\mathbb{N}\to \underset{n\in N}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)$$
8	1 2	iundisj2fi	$$⊢\underset{n\in \left(1..^M\right)}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)$$
9		disjeq1	$$⊢N=\left(1..^M\right)\to \left(\underset{n\in N}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)\leftrightarrow \underset{n\in \left(1..^M\right)}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)\right)$$
10	8 9	mpbiri	$$⊢N=\left(1..^M\right)\to \underset{n\in N}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)$$
11	7 10	jaoi	$$⊢\left(N=\mathbb{N}\vee N=\left(1..^M\right)\right)\to \underset{n\in N}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)$$
12	3 11	syl	$$⊢\phi \to \underset{n\in N}{Disj}\left(A\setminus \bigcup _{k\in \left(1..^n\right)}B\right)$$