Metamath Proof Explorer

Theorem iundisj

Description: Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypothesis iundisj.1 
|- ( n = k -> A = B )
Assertion iundisj 
|- U_ n e. NN A = U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )

Proof

Step Hyp Ref Expression
1 iundisj.1 
 |-  ( n = k -> A = B )
2 ssrab2 
 |-  { n e. NN | x e. A } C_ NN
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 2 3 sseqtri 
 |-  { n e. NN | x e. A } C_ ( ZZ>= ` 1 )
5 rabn0 
 |-  ( { n e. NN | x e. A } =/= (/) <-> E. n e. NN x e. A )
6 5 biimpri 
 |-  ( E. n e. NN x e. A -> { n e. NN | x e. A } =/= (/) )
7 infssuzcl 
 |-  ( ( { n e. NN | x e. A } C_ ( ZZ>= ` 1 ) /\ { n e. NN | x e. A } =/= (/) ) -> inf ( { n e. NN | x e. A } , RR , < ) e. { n e. NN | x e. A } )
8 4 6 7 sylancr 
 |-  ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. { n e. NN | x e. A } )
9 nfrab1 
 |-  F/_ n { n e. NN | x e. A }
10 nfcv 
 |-  F/_ n RR
11 nfcv 
 |-  F/_ n <
12 9 10 11 nfinf 
 |-  F/_ n inf ( { n e. NN | x e. A } , RR , < )
13 nfcv 
 |-  F/_ n NN
14 12 nfcsb1 
 |-  F/_ n [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A
15 14 nfcri 
 |-  F/ n x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A
16 csbeq1a 
 |-  ( n = inf ( { n e. NN | x e. A } , RR , < ) -> A = [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A )
17 16 eleq2d 
 |-  ( n = inf ( { n e. NN | x e. A } , RR , < ) -> ( x e. A <-> x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) )
18 12 13 15 17 elrabf 
 |-  ( inf ( { n e. NN | x e. A } , RR , < ) e. { n e. NN | x e. A } <-> ( inf ( { n e. NN | x e. A } , RR , < ) e. NN /\ x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) )
19 8 18 sylib 
 |-  ( E. n e. NN x e. A -> ( inf ( { n e. NN | x e. A } , RR , < ) e. NN /\ x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) )
20 19 simpld 
 |-  ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. NN )
21 19 simprd 
 |-  ( E. n e. NN x e. A -> x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A )
22 20 nnred 
 |-  ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. RR )
23 22 ltnrd 
 |-  ( E. n e. NN x e. A -> -. inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) )
24 eliun 
 |-  ( x e. U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B <-> E. k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) x e. B )
25 22 ad2antrr 
 |-  ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> inf ( { n e. NN | x e. A } , RR , < ) e. RR )
26 elfzouz 
 |-  ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k e. ( ZZ>= ` 1 ) )
27 26 3 eleqtrrdi 
 |-  ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k e. NN )
28 27 ad2antlr 
 |-  ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> k e. NN )
29 28 nnred 
 |-  ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> k e. RR )
30 1 eleq2d 
 |-  ( n = k -> ( x e. A <-> x e. B ) )
31 simpr 
 |-  ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> x e. B )
32 30 28 31 elrabd 
 |-  ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> k e. { n e. NN | x e. A } )
33 infssuzle 
 |-  ( ( { n e. NN | x e. A } C_ ( ZZ>= ` 1 ) /\ k e. { n e. NN | x e. A } ) -> inf ( { n e. NN | x e. A } , RR , < ) <_ k )
34 4 32 33 sylancr 
 |-  ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> inf ( { n e. NN | x e. A } , RR , < ) <_ k )
35 elfzolt2 
 |-  ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k < inf ( { n e. NN | x e. A } , RR , < ) )
36 35 ad2antlr 
 |-  ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> k < inf ( { n e. NN | x e. A } , RR , < ) )
37 25 29 25 34 36 lelttrd 
 |-  ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) )
38 37 rexlimdva2 
 |-  ( E. n e. NN x e. A -> ( E. k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) x e. B -> inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) ) )
39 24 38 syl5bi 
 |-  ( E. n e. NN x e. A -> ( x e. U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B -> inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) ) )
40 23 39 mtod 
 |-  ( E. n e. NN x e. A -> -. x e. U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B )
41 21 40 eldifd 
 |-  ( E. n e. NN x e. A -> x e. ( [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A \ U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) )
42 csbeq1 
 |-  ( m = inf ( { n e. NN | x e. A } , RR , < ) -> [_ m / n ]_ A = [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A )
43 oveq2 
 |-  ( m = inf ( { n e. NN | x e. A } , RR , < ) -> ( 1 ..^ m ) = ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) )
44 43 iuneq1d 
 |-  ( m = inf ( { n e. NN | x e. A } , RR , < ) -> U_ k e. ( 1 ..^ m ) B = U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B )
45 42 44 difeq12d 
 |-  ( m = inf ( { n e. NN | x e. A } , RR , < ) -> ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) = ( [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A \ U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) )
46 45 eleq2d 
 |-  ( m = inf ( { n e. NN | x e. A } , RR , < ) -> ( x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) <-> x e. ( [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A \ U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) ) )
47 46 rspcev 
 |-  ( ( inf ( { n e. NN | x e. A } , RR , < ) e. NN /\ x e. ( [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A \ U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) ) -> E. m e. NN x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) )
48 20 41 47 syl2anc 
 |-  ( E. n e. NN x e. A -> E. m e. NN x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) )
49 nfv 
 |-  F/ m x e. ( A \ U_ k e. ( 1 ..^ n ) B )
50 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
51 nfcv 
 |-  F/_ n U_ k e. ( 1 ..^ m ) B
52 50 51 nfdif 
 |-  F/_ n ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B )
53 52 nfcri 
 |-  F/ n x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B )
54 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
55 oveq2 
 |-  ( n = m -> ( 1 ..^ n ) = ( 1 ..^ m ) )
56 55 iuneq1d 
 |-  ( n = m -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ m ) B )
57 54 56 difeq12d 
 |-  ( n = m -> ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) )
58 57 eleq2d 
 |-  ( n = m -> ( x e. ( A \ U_ k e. ( 1 ..^ n ) B ) <-> x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) ) )
59 49 53 58 cbvrexw 
 |-  ( E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) <-> E. m e. NN x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) )
60 48 59 sylibr 
 |-  ( E. n e. NN x e. A -> E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) )
61 eldifi 
 |-  ( x e. ( A \ U_ k e. ( 1 ..^ n ) B ) -> x e. A )
62 61 reximi 
 |-  ( E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) -> E. n e. NN x e. A )
63 60 62 impbii 
 |-  ( E. n e. NN x e. A <-> E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) )
64 eliun 
 |-  ( x e. U_ n e. NN A <-> E. n e. NN x e. A )
65 eliun 
 |-  ( x e. U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B ) <-> E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) )
66 63 64 65 3bitr4i 
 |-  ( x e. U_ n e. NN A <-> x e. U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B ) )
67 66 eqriv 
 |-  U_ n e. NN A = U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )