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 
|- F/_ n B
iundisj2cnt.1 
|- ( n = k -> A = B )
iundisj2cnt.2 
|- ( ph -> ( N = NN \/ N = ( 1 ..^ M ) ) )
Assertion iundisj2cnt 
|- ( ph -> Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )

Proof

Step Hyp Ref Expression
1 iundisj2cnt.0 
 |-  F/_ n B
2 iundisj2cnt.1 
 |-  ( n = k -> A = B )
3 iundisj2cnt.2 
 |-  ( ph -> ( N = NN \/ N = ( 1 ..^ M ) ) )
4 nfcv 
 |-  F/_ k A
5 4 1 2 iundisj2f 
 |-  Disj_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )
6 disjeq1 
 |-  ( N = NN -> ( Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) <-> Disj_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B ) ) )
7 5 6 mpbiri 
 |-  ( N = NN -> Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )
8 1 2 iundisj2fi 
 |-  Disj_ n e. ( 1 ..^ M ) ( A \ U_ k e. ( 1 ..^ n ) B )
9 disjeq1 
 |-  ( N = ( 1 ..^ M ) -> ( Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) <-> Disj_ n e. ( 1 ..^ M ) ( A \ U_ k e. ( 1 ..^ n ) B ) ) )
10 8 9 mpbiri 
 |-  ( N = ( 1 ..^ M ) -> Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )
11 7 10 jaoi 
 |-  ( ( N = NN \/ N = ( 1 ..^ M ) ) -> Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )
12 3 11 syl 
 |-  ( ph -> Disj_ n e. N ( A \ U_ k e. ( 1 ..^ n ) B ) )