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 )