Metamath Proof Explorer

Theorem iundisjfi

Description: Rewrite a countable union as a disjoint union, finite version. Cf. iundisj . (Contributed by Thierry Arnoux, 15-Feb-2017)

Ref Expression
Hypotheses iundisj3.0 
|- F/_ n B
iundisj3.1 
|- ( n = k -> A = B )
Assertion iundisjfi 
|- U_ n e. ( 1 ..^ N ) A = U_ n e. ( 1 ..^ N ) ( A \ U_ k e. ( 1 ..^ n ) B )

Proof

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