Metamath Proof Explorer


Theorem fiunelros

Description: A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Hypotheses isros.1
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
fiunelros.1
|- ( ph -> S e. Q )
fiunelros.2
|- ( ph -> N e. NN )
fiunelros.3
|- ( ( ph /\ k e. ( 1 ..^ N ) ) -> B e. S )
Assertion fiunelros
|- ( ph -> U_ k e. ( 1 ..^ N ) B e. S )

Proof

Step Hyp Ref Expression
1 isros.1
 |-  Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
2 fiunelros.1
 |-  ( ph -> S e. Q )
3 fiunelros.2
 |-  ( ph -> N e. NN )
4 fiunelros.3
 |-  ( ( ph /\ k e. ( 1 ..^ N ) ) -> B e. S )
5 simpr
 |-  ( ( ph /\ N e. NN ) -> N e. NN )
6 5 nnred
 |-  ( ( ph /\ N e. NN ) -> N e. RR )
7 6 leidd
 |-  ( ( ph /\ N e. NN ) -> N <_ N )
8 breq1
 |-  ( n = 1 -> ( n <_ N <-> 1 <_ N ) )
9 oveq2
 |-  ( n = 1 -> ( 1 ..^ n ) = ( 1 ..^ 1 ) )
10 9 iuneq1d
 |-  ( n = 1 -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ 1 ) B )
11 10 eleq1d
 |-  ( n = 1 -> ( U_ k e. ( 1 ..^ n ) B e. S <-> U_ k e. ( 1 ..^ 1 ) B e. S ) )
12 8 11 imbi12d
 |-  ( n = 1 -> ( ( n <_ N -> U_ k e. ( 1 ..^ n ) B e. S ) <-> ( 1 <_ N -> U_ k e. ( 1 ..^ 1 ) B e. S ) ) )
13 breq1
 |-  ( n = i -> ( n <_ N <-> i <_ N ) )
14 oveq2
 |-  ( n = i -> ( 1 ..^ n ) = ( 1 ..^ i ) )
15 14 iuneq1d
 |-  ( n = i -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ i ) B )
16 15 eleq1d
 |-  ( n = i -> ( U_ k e. ( 1 ..^ n ) B e. S <-> U_ k e. ( 1 ..^ i ) B e. S ) )
17 13 16 imbi12d
 |-  ( n = i -> ( ( n <_ N -> U_ k e. ( 1 ..^ n ) B e. S ) <-> ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) )
18 breq1
 |-  ( n = ( i + 1 ) -> ( n <_ N <-> ( i + 1 ) <_ N ) )
19 oveq2
 |-  ( n = ( i + 1 ) -> ( 1 ..^ n ) = ( 1 ..^ ( i + 1 ) ) )
20 19 iuneq1d
 |-  ( n = ( i + 1 ) -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ ( i + 1 ) ) B )
21 20 eleq1d
 |-  ( n = ( i + 1 ) -> ( U_ k e. ( 1 ..^ n ) B e. S <-> U_ k e. ( 1 ..^ ( i + 1 ) ) B e. S ) )
22 18 21 imbi12d
 |-  ( n = ( i + 1 ) -> ( ( n <_ N -> U_ k e. ( 1 ..^ n ) B e. S ) <-> ( ( i + 1 ) <_ N -> U_ k e. ( 1 ..^ ( i + 1 ) ) B e. S ) ) )
23 breq1
 |-  ( n = N -> ( n <_ N <-> N <_ N ) )
24 oveq2
 |-  ( n = N -> ( 1 ..^ n ) = ( 1 ..^ N ) )
25 24 iuneq1d
 |-  ( n = N -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ N ) B )
26 25 eleq1d
 |-  ( n = N -> ( U_ k e. ( 1 ..^ n ) B e. S <-> U_ k e. ( 1 ..^ N ) B e. S ) )
27 23 26 imbi12d
 |-  ( n = N -> ( ( n <_ N -> U_ k e. ( 1 ..^ n ) B e. S ) <-> ( N <_ N -> U_ k e. ( 1 ..^ N ) B e. S ) ) )
28 fzo0
 |-  ( 1 ..^ 1 ) = (/)
29 iuneq1
 |-  ( ( 1 ..^ 1 ) = (/) -> U_ k e. ( 1 ..^ 1 ) B = U_ k e. (/) B )
30 28 29 ax-mp
 |-  U_ k e. ( 1 ..^ 1 ) B = U_ k e. (/) B
31 0iun
 |-  U_ k e. (/) B = (/)
32 30 31 eqtri
 |-  U_ k e. ( 1 ..^ 1 ) B = (/)
33 1 0elros
 |-  ( S e. Q -> (/) e. S )
34 2 33 syl
 |-  ( ph -> (/) e. S )
35 32 34 eqeltrid
 |-  ( ph -> U_ k e. ( 1 ..^ 1 ) B e. S )
36 35 a1d
 |-  ( ph -> ( 1 <_ N -> U_ k e. ( 1 ..^ 1 ) B e. S ) )
37 simpllr
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> i e. NN )
38 fzosplitsn
 |-  ( i e. ( ZZ>= ` 1 ) -> ( 1 ..^ ( i + 1 ) ) = ( ( 1 ..^ i ) u. { i } ) )
39 nnuz
 |-  NN = ( ZZ>= ` 1 )
40 38 39 eleq2s
 |-  ( i e. NN -> ( 1 ..^ ( i + 1 ) ) = ( ( 1 ..^ i ) u. { i } ) )
41 40 iuneq1d
 |-  ( i e. NN -> U_ k e. ( 1 ..^ ( i + 1 ) ) B = U_ k e. ( ( 1 ..^ i ) u. { i } ) B )
42 37 41 syl
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> U_ k e. ( 1 ..^ ( i + 1 ) ) B = U_ k e. ( ( 1 ..^ i ) u. { i } ) B )
43 iunxun
 |-  U_ k e. ( ( 1 ..^ i ) u. { i } ) B = ( U_ k e. ( 1 ..^ i ) B u. U_ k e. { i } B )
44 42 43 eqtrdi
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> U_ k e. ( 1 ..^ ( i + 1 ) ) B = ( U_ k e. ( 1 ..^ i ) B u. U_ k e. { i } B ) )
45 2 ad3antrrr
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> S e. Q )
46 37 nnred
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> i e. RR )
47 3 ad3antrrr
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> N e. NN )
48 47 nnred
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> N e. RR )
49 simpr
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> ( i + 1 ) <_ N )
50 nnltp1le
 |-  ( ( i e. NN /\ N e. NN ) -> ( i < N <-> ( i + 1 ) <_ N ) )
51 37 47 50 syl2anc
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> ( i < N <-> ( i + 1 ) <_ N ) )
52 49 51 mpbird
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> i < N )
53 46 48 52 ltled
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> i <_ N )
54 simplr
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) )
55 53 54 mpd
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> U_ k e. ( 1 ..^ i ) B e. S )
56 nfcsb1v
 |-  F/_ k [_ i / k ]_ B
57 csbeq1a
 |-  ( k = i -> B = [_ i / k ]_ B )
58 56 57 iunxsngf
 |-  ( i e. NN -> U_ k e. { i } B = [_ i / k ]_ B )
59 37 58 syl
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> U_ k e. { i } B = [_ i / k ]_ B )
60 simplll
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> ph )
61 elfzo1
 |-  ( i e. ( 1 ..^ N ) <-> ( i e. NN /\ N e. NN /\ i < N ) )
62 37 47 52 61 syl3anbrc
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> i e. ( 1 ..^ N ) )
63 nfv
 |-  F/ k ( ph /\ i e. ( 1 ..^ N ) )
64 nfcv
 |-  F/_ k S
65 56 64 nfel
 |-  F/ k [_ i / k ]_ B e. S
66 63 65 nfim
 |-  F/ k ( ( ph /\ i e. ( 1 ..^ N ) ) -> [_ i / k ]_ B e. S )
67 eleq1w
 |-  ( k = i -> ( k e. ( 1 ..^ N ) <-> i e. ( 1 ..^ N ) ) )
68 67 anbi2d
 |-  ( k = i -> ( ( ph /\ k e. ( 1 ..^ N ) ) <-> ( ph /\ i e. ( 1 ..^ N ) ) ) )
69 57 eleq1d
 |-  ( k = i -> ( B e. S <-> [_ i / k ]_ B e. S ) )
70 68 69 imbi12d
 |-  ( k = i -> ( ( ( ph /\ k e. ( 1 ..^ N ) ) -> B e. S ) <-> ( ( ph /\ i e. ( 1 ..^ N ) ) -> [_ i / k ]_ B e. S ) ) )
71 66 70 4 chvarfv
 |-  ( ( ph /\ i e. ( 1 ..^ N ) ) -> [_ i / k ]_ B e. S )
72 60 62 71 syl2anc
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> [_ i / k ]_ B e. S )
73 59 72 eqeltrd
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> U_ k e. { i } B e. S )
74 1 unelros
 |-  ( ( S e. Q /\ U_ k e. ( 1 ..^ i ) B e. S /\ U_ k e. { i } B e. S ) -> ( U_ k e. ( 1 ..^ i ) B u. U_ k e. { i } B ) e. S )
75 45 55 73 74 syl3anc
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> ( U_ k e. ( 1 ..^ i ) B u. U_ k e. { i } B ) e. S )
76 44 75 eqeltrd
 |-  ( ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) /\ ( i + 1 ) <_ N ) -> U_ k e. ( 1 ..^ ( i + 1 ) ) B e. S )
77 76 ex
 |-  ( ( ( ph /\ i e. NN ) /\ ( i <_ N -> U_ k e. ( 1 ..^ i ) B e. S ) ) -> ( ( i + 1 ) <_ N -> U_ k e. ( 1 ..^ ( i + 1 ) ) B e. S ) )
78 12 17 22 27 36 77 nnindd
 |-  ( ( ph /\ N e. NN ) -> ( N <_ N -> U_ k e. ( 1 ..^ N ) B e. S ) )
79 7 78 mpd
 |-  ( ( ph /\ N e. NN ) -> U_ k e. ( 1 ..^ N ) B e. S )
80 3 79 mpdan
 |-  ( ph -> U_ k e. ( 1 ..^ N ) B e. S )