Metamath Proof Explorer

Theorem iundisjf

Description: Rewrite a countable union as a disjoint union. Cf. iundisj . (Contributed by Thierry Arnoux, 31-Dec-2016)

Ref Expression
Hypotheses iundisjf.1 
|- F/_ k A
iundisjf.2 
|- F/_ n B
iundisjf.3 
|- ( n = k -> A = B )
Assertion iundisjf 
|- U_ n e. NN A = U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )

Proof

Step Hyp Ref Expression
1 iundisjf.1 
 |-  F/_ k A
2 iundisjf.2 
 |-  F/_ n B
3 iundisjf.3 
 |-  ( n = k -> A = B )
4 ssrab2 
 |-  { n e. NN | x e. A } C_ NN
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 4 5 sseqtri 
 |-  { n e. NN | x e. A } C_ ( ZZ>= ` 1 )
7 rabn0 
 |-  ( { n e. NN | x e. A } =/= (/) <-> E. n e. NN x e. A )
8 7 biimpri 
 |-  ( E. n e. NN x e. A -> { n e. NN | x e. A } =/= (/) )
9 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 } )
10 6 8 9 sylancr 
 |-  ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. { n e. NN | x e. A } )
11 nfrab1 
 |-  F/_ n { n e. NN | x e. A }
12 nfcv 
 |-  F/_ n RR
13 nfcv 
 |-  F/_ n <
14 11 12 13 nfinf 
 |-  F/_ n inf ( { n e. NN | x e. A } , RR , < )
15 nfcv 
 |-  F/_ n NN
16 14 nfcsb1 
 |-  F/_ n [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A
17 16 nfcri 
 |-  F/ n x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A
18 csbeq1a 
 |-  ( n = inf ( { n e. NN | x e. A } , RR , < ) -> A = [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A )
19 18 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 ) )
20 14 15 17 19 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 ) )
21 10 20 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 ) )
22 21 simpld 
 |-  ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. NN )
23 21 simprd 
 |-  ( E. n e. NN x e. A -> x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A )
24 22 nnred 
 |-  ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. RR )
25 24 ltnrd 
 |-  ( E. n e. NN x e. A -> -. inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) )
26 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 )
27 nfcv 
 |-  F/_ k NN
28 1 nfcri 
 |-  F/ k x e. A
29 27 28 nfrexw 
 |-  F/ k E. n e. NN x e. A
30 28 27 nfrabw 
 |-  F/_ k { n e. NN | x e. A }
31 nfcv 
 |-  F/_ k RR
32 nfcv 
 |-  F/_ k <
33 30 31 32 nfinf 
 |-  F/_ k inf ( { n e. NN | x e. A } , RR , < )
34 33 32 33 nfbr 
 |-  F/ k inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < )
35 24 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 )
36 elfzouz 
 |-  ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k e. ( ZZ>= ` 1 ) )
37 36 5 eleqtrrdi 
 |-  ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k e. NN )
38 37 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 )
39 38 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 )
40 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 )
41 nfcv 
 |-  F/_ n k
42 2 nfcri 
 |-  F/ n x e. B
43 3 eleq2d 
 |-  ( n = k -> ( x e. A <-> x e. B ) )
44 41 15 42 43 elrabf 
 |-  ( k e. { n e. NN | x e. A } <-> ( k e. NN /\ x e. B ) )
45 38 40 44 sylanbrc 
 |-  ( ( ( 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 } )
46 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 )
47 6 45 46 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 )
48 elfzolt2 
 |-  ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k < inf ( { n e. NN | x e. A } , RR , < ) )
49 48 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 , < ) )
50 35 39 35 47 49 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 , < ) )
51 50 exp31 
 |-  ( 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 , < ) ) ) )
52 29 34 51 rexlimd 
 |-  ( 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 , < ) ) )
53 26 52 biimtrid 
 |-  ( 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 , < ) ) )
54 25 53 mtod 
 |-  ( E. n e. NN x e. A -> -. x e. U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B )
55 23 54 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 ) )
56 csbeq1 
 |-  ( m = inf ( { n e. NN | x e. A } , RR , < ) -> [_ m / n ]_ A = [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A )
57 33 nfeq2 
 |-  F/ k m = inf ( { n e. NN | x e. A } , RR , < )
58 nfcv 
 |-  F/_ k ( 1 ..^ m )
59 nfcv 
 |-  F/_ k 1
60 nfcv 
 |-  F/_ k ..^
61 59 60 33 nfov 
 |-  F/_ k ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) )
62 oveq2 
 |-  ( m = inf ( { n e. NN | x e. A } , RR , < ) -> ( 1 ..^ m ) = ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) )
63 eqidd 
 |-  ( m = inf ( { n e. NN | x e. A } , RR , < ) -> B = B )
64 57 58 61 62 63 iuneq12df 
 |-  ( 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 )
65 56 64 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 ) )
66 65 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 ) ) )
67 66 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 ) )
68 22 55 67 syl2anc 
 |-  ( E. n e. NN x e. A -> E. m e. NN x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) )
69 nfv 
 |-  F/ m x e. ( A \ U_ k e. ( 1 ..^ n ) B )
70 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
71 nfcv 
 |-  F/_ n ( 1 ..^ m )
72 71 2 nfiun 
 |-  F/_ n U_ k e. ( 1 ..^ m ) B
73 70 72 nfdif 
 |-  F/_ n ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B )
74 73 nfcri 
 |-  F/ n x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B )
75 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
76 oveq2 
 |-  ( n = m -> ( 1 ..^ n ) = ( 1 ..^ m ) )
77 76 iuneq1d 
 |-  ( n = m -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ m ) B )
78 75 77 difeq12d 
 |-  ( n = m -> ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) )
79 78 eleq2d 
 |-  ( n = m -> ( x e. ( A \ U_ k e. ( 1 ..^ n ) B ) <-> x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) ) )
80 69 74 79 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 ) )
81 68 80 sylibr 
 |-  ( E. n e. NN x e. A -> E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) )
82 eldifi 
 |-  ( x e. ( A \ U_ k e. ( 1 ..^ n ) B ) -> x e. A )
83 82 reximi 
 |-  ( E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) -> E. n e. NN x e. A )
84 81 83 impbii 
 |-  ( E. n e. NN x e. A <-> E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) )
85 eliun 
 |-  ( x e. U_ n e. NN A <-> E. n e. NN x e. A )
86 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 ) )
87 84 85 86 3bitr4i 
 |-  ( x e. U_ n e. NN A <-> x e. U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B ) )
88 87 eqriv 
 |-  U_ n e. NN A = U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )