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 nfrex
 |-  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 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 , < ) ) )
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 )