Theorem iundisjcnt

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

	Ref	Expression
Hypotheses	iundisjcnt.0	|- F/_ n B
	iundisjcnt.1	|- ( n = k -> A = B )
	iundisjcnt.2	|- ( ph -> ( N = NN \/ N = ( 1 ..^ M ) ) )
Assertion	iundisjcnt	|- ( ph -> U_ n e. N A = U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )

Proof

Step	Hyp	Ref	Expression
1		iundisjcnt.0	|- F/_ n B
2		iundisjcnt.1	|- ( n = k -> A = B )
3		iundisjcnt.2	|- ( ph -> ( N = NN \/ N = ( 1 ..^ M ) ) )
4		nfcv	|- F/_ k A
5	4 1 2	iundisjf	|- U_ n e. NN A = U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )
6		simpr	|- ( ( ph /\ N = NN ) -> N = NN )
7	6	iuneq1d	|- ( ( ph /\ N = NN ) -> U_ n e. N A = U_ n e. NN A )
8	6	iuneq1d	|- ( ( ph /\ N = NN ) -> U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) = U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B ) )
9	5 7 8	3eqtr4a	|- ( ( ph /\ N = NN ) -> U_ n e. N A = U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )
10	1 2	iundisjfi	|- U_ n e. ( 1 ..^ M ) A = U_ n e. ( 1 ..^ M ) ( A \ U_ k e. ( 1 ..^ n ) B )
11		simpr	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> N = ( 1 ..^ M ) )
12	11	iuneq1d	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ n e. N A = U_ n e. ( 1 ..^ M ) A )
13	11	iuneq1d	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) = U_ n e. ( 1 ..^ M ) ( A \ U_ k e. ( 1 ..^ n ) B ) )
14	10 12 13	3eqtr4a	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ n e. N A = U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )
15	9 14 3	mpjaodan	|- ( ph -> U_ n e. N A = U_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )