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