Metamath Proof Explorer

Theorem iuninc

Description: The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017)

Ref Expression
Hypotheses iuninc.1 
|- ( ph -> F Fn NN )
iuninc.2 
|- ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )
Assertion iuninc 
|- ( ( ph /\ i e. NN ) -> U_ n e. ( 1 ... i ) ( F ` n ) = ( F ` i ) )

Proof

Step Hyp Ref Expression
1 iuninc.1 
 |-  ( ph -> F Fn NN )
2 iuninc.2 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )
3 oveq2 
 |-  ( j = 1 -> ( 1 ... j ) = ( 1 ... 1 ) )
4 3 iuneq1d 
 |-  ( j = 1 -> U_ n e. ( 1 ... j ) ( F ` n ) = U_ n e. ( 1 ... 1 ) ( F ` n ) )
5 fveq2 
 |-  ( j = 1 -> ( F ` j ) = ( F ` 1 ) )
6 4 5 eqeq12d 
 |-  ( j = 1 -> ( U_ n e. ( 1 ... j ) ( F ` n ) = ( F ` j ) <-> U_ n e. ( 1 ... 1 ) ( F ` n ) = ( F ` 1 ) ) )
7 6 imbi2d 
 |-  ( j = 1 -> ( ( ph -> U_ n e. ( 1 ... j ) ( F ` n ) = ( F ` j ) ) <-> ( ph -> U_ n e. ( 1 ... 1 ) ( F ` n ) = ( F ` 1 ) ) ) )
8 oveq2 
 |-  ( j = k -> ( 1 ... j ) = ( 1 ... k ) )
9 8 iuneq1d 
 |-  ( j = k -> U_ n e. ( 1 ... j ) ( F ` n ) = U_ n e. ( 1 ... k ) ( F ` n ) )
10 fveq2 
 |-  ( j = k -> ( F ` j ) = ( F ` k ) )
11 9 10 eqeq12d 
 |-  ( j = k -> ( U_ n e. ( 1 ... j ) ( F ` n ) = ( F ` j ) <-> U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) )
12 11 imbi2d 
 |-  ( j = k -> ( ( ph -> U_ n e. ( 1 ... j ) ( F ` n ) = ( F ` j ) ) <-> ( ph -> U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) ) )
13 oveq2 
 |-  ( j = ( k + 1 ) -> ( 1 ... j ) = ( 1 ... ( k + 1 ) ) )
14 13 iuneq1d 
 |-  ( j = ( k + 1 ) -> U_ n e. ( 1 ... j ) ( F ` n ) = U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) )
15 fveq2 
 |-  ( j = ( k + 1 ) -> ( F ` j ) = ( F ` ( k + 1 ) ) )
16 14 15 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( U_ n e. ( 1 ... j ) ( F ` n ) = ( F ` j ) <-> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = ( F ` ( k + 1 ) ) ) )
17 16 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ph -> U_ n e. ( 1 ... j ) ( F ` n ) = ( F ` j ) ) <-> ( ph -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = ( F ` ( k + 1 ) ) ) ) )
18 oveq2 
 |-  ( j = i -> ( 1 ... j ) = ( 1 ... i ) )
19 18 iuneq1d 
 |-  ( j = i -> U_ n e. ( 1 ... j ) ( F ` n ) = U_ n e. ( 1 ... i ) ( F ` n ) )
20 fveq2 
 |-  ( j = i -> ( F ` j ) = ( F ` i ) )
21 19 20 eqeq12d 
 |-  ( j = i -> ( U_ n e. ( 1 ... j ) ( F ` n ) = ( F ` j ) <-> U_ n e. ( 1 ... i ) ( F ` n ) = ( F ` i ) ) )
22 21 imbi2d 
 |-  ( j = i -> ( ( ph -> U_ n e. ( 1 ... j ) ( F ` n ) = ( F ` j ) ) <-> ( ph -> U_ n e. ( 1 ... i ) ( F ` n ) = ( F ` i ) ) ) )
23 1z 
 |-  1 e. ZZ
24 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
25 iuneq1 
 |-  ( ( 1 ... 1 ) = { 1 } -> U_ n e. ( 1 ... 1 ) ( F ` n ) = U_ n e. { 1 } ( F ` n ) )
26 23 24 25 mp2b 
 |-  U_ n e. ( 1 ... 1 ) ( F ` n ) = U_ n e. { 1 } ( F ` n )
27 1ex 
 |-  1 e. _V
28 fveq2 
 |-  ( n = 1 -> ( F ` n ) = ( F ` 1 ) )
29 27 28 iunxsn 
 |-  U_ n e. { 1 } ( F ` n ) = ( F ` 1 )
30 26 29 eqtri 
 |-  U_ n e. ( 1 ... 1 ) ( F ` n ) = ( F ` 1 )
31 30 a1i 
 |-  ( ph -> U_ n e. ( 1 ... 1 ) ( F ` n ) = ( F ` 1 ) )
32 simpll 
 |-  ( ( ( k e. NN /\ ph ) /\ U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) -> k e. NN )
33 elnnuz 
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
34 fzsuc 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( 1 ... ( k + 1 ) ) = ( ( 1 ... k ) u. { ( k + 1 ) } ) )
35 33 34 sylbi 
 |-  ( k e. NN -> ( 1 ... ( k + 1 ) ) = ( ( 1 ... k ) u. { ( k + 1 ) } ) )
36 35 iuneq1d 
 |-  ( k e. NN -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = U_ n e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ( F ` n ) )
37 iunxun 
 |-  U_ n e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ( F ` n ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. U_ n e. { ( k + 1 ) } ( F ` n ) )
38 ovex 
 |-  ( k + 1 ) e. _V
39 fveq2 
 |-  ( n = ( k + 1 ) -> ( F ` n ) = ( F ` ( k + 1 ) ) )
40 38 39 iunxsn 
 |-  U_ n e. { ( k + 1 ) } ( F ` n ) = ( F ` ( k + 1 ) )
41 40 uneq2i 
 |-  ( U_ n e. ( 1 ... k ) ( F ` n ) u. U_ n e. { ( k + 1 ) } ( F ` n ) ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) )
42 37 41 eqtri 
 |-  U_ n e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ( F ` n ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) )
43 36 42 eqtrdi 
 |-  ( k e. NN -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) )
44 32 43 syl 
 |-  ( ( ( k e. NN /\ ph ) /\ U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) )
45 simpr 
 |-  ( ( ( k e. NN /\ ph ) /\ U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) -> U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) )
46 45 uneq1d 
 |-  ( ( ( k e. NN /\ ph ) /\ U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) -> ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) = ( ( F ` k ) u. ( F ` ( k + 1 ) ) ) )
47 simplr 
 |-  ( ( ( k e. NN /\ ph ) /\ U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) -> ph )
48 2 sbt 
 |-  [ k / n ] ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )
49 sbim 
 |-  ( [ k / n ] ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) ) <-> ( [ k / n ] ( ph /\ n e. NN ) -> [ k / n ] ( F ` n ) C_ ( F ` ( n + 1 ) ) ) )
50 sban 
 |-  ( [ k / n ] ( ph /\ n e. NN ) <-> ( [ k / n ] ph /\ [ k / n ] n e. NN ) )
51 sbv 
 |-  ( [ k / n ] ph <-> ph )
52 clelsb1 
 |-  ( [ k / n ] n e. NN <-> k e. NN )
53 51 52 anbi12i 
 |-  ( ( [ k / n ] ph /\ [ k / n ] n e. NN ) <-> ( ph /\ k e. NN ) )
54 50 53 bitr2i 
 |-  ( ( ph /\ k e. NN ) <-> [ k / n ] ( ph /\ n e. NN ) )
55 sbsbc 
 |-  ( [ k / n ] ( F ` n ) C_ ( F ` ( n + 1 ) ) <-> [. k / n ]. ( F ` n ) C_ ( F ` ( n + 1 ) ) )
56 sbcssg 
 |-  ( k e. _V -> ( [. k / n ]. ( F ` n ) C_ ( F ` ( n + 1 ) ) <-> [_ k / n ]_ ( F ` n ) C_ [_ k / n ]_ ( F ` ( n + 1 ) ) ) )
57 56 elv 
 |-  ( [. k / n ]. ( F ` n ) C_ ( F ` ( n + 1 ) ) <-> [_ k / n ]_ ( F ` n ) C_ [_ k / n ]_ ( F ` ( n + 1 ) ) )
58 csbfv 
 |-  [_ k / n ]_ ( F ` n ) = ( F ` k )
59 csbfv2g 
 |-  ( k e. _V -> [_ k / n ]_ ( F ` ( n + 1 ) ) = ( F ` [_ k / n ]_ ( n + 1 ) ) )
60 59 elv 
 |-  [_ k / n ]_ ( F ` ( n + 1 ) ) = ( F ` [_ k / n ]_ ( n + 1 ) )
61 csbov1g 
 |-  ( k e. _V -> [_ k / n ]_ ( n + 1 ) = ( [_ k / n ]_ n + 1 ) )
62 61 elv 
 |-  [_ k / n ]_ ( n + 1 ) = ( [_ k / n ]_ n + 1 )
63 62 fveq2i 
 |-  ( F ` [_ k / n ]_ ( n + 1 ) ) = ( F ` ( [_ k / n ]_ n + 1 ) )
64 vex 
 |-  k e. _V
65 64 csbvargi 
 |-  [_ k / n ]_ n = k
66 65 oveq1i 
 |-  ( [_ k / n ]_ n + 1 ) = ( k + 1 )
67 66 fveq2i 
 |-  ( F ` ( [_ k / n ]_ n + 1 ) ) = ( F ` ( k + 1 ) )
68 60 63 67 3eqtri 
 |-  [_ k / n ]_ ( F ` ( n + 1 ) ) = ( F ` ( k + 1 ) )
69 58 68 sseq12i 
 |-  ( [_ k / n ]_ ( F ` n ) C_ [_ k / n ]_ ( F ` ( n + 1 ) ) <-> ( F ` k ) C_ ( F ` ( k + 1 ) ) )
70 55 57 69 3bitrri 
 |-  ( ( F ` k ) C_ ( F ` ( k + 1 ) ) <-> [ k / n ] ( F ` n ) C_ ( F ` ( n + 1 ) ) )
71 54 70 imbi12i 
 |-  ( ( ( ph /\ k e. NN ) -> ( F ` k ) C_ ( F ` ( k + 1 ) ) ) <-> ( [ k / n ] ( ph /\ n e. NN ) -> [ k / n ] ( F ` n ) C_ ( F ` ( n + 1 ) ) ) )
72 49 71 bitr4i 
 |-  ( [ k / n ] ( ( ph /\ n e. NN ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) ) <-> ( ( ph /\ k e. NN ) -> ( F ` k ) C_ ( F ` ( k + 1 ) ) ) )
73 48 72 mpbi 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) C_ ( F ` ( k + 1 ) ) )
74 ssequn1 
 |-  ( ( F ` k ) C_ ( F ` ( k + 1 ) ) <-> ( ( F ` k ) u. ( F ` ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
75 73 74 sylib 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) u. ( F ` ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
76 47 32 75 syl2anc 
 |-  ( ( ( k e. NN /\ ph ) /\ U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) -> ( ( F ` k ) u. ( F ` ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
77 44 46 76 3eqtrd 
 |-  ( ( ( k e. NN /\ ph ) /\ U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = ( F ` ( k + 1 ) ) )
78 77 exp31 
 |-  ( k e. NN -> ( ph -> ( U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = ( F ` ( k + 1 ) ) ) ) )
79 78 a2d 
 |-  ( k e. NN -> ( ( ph -> U_ n e. ( 1 ... k ) ( F ` n ) = ( F ` k ) ) -> ( ph -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = ( F ` ( k + 1 ) ) ) ) )
80 7 12 17 22 31 79 nnind 
 |-  ( i e. NN -> ( ph -> U_ n e. ( 1 ... i ) ( F ` n ) = ( F ` i ) ) )
81 80 impcom 
 |-  ( ( ph /\ i e. NN ) -> U_ n e. ( 1 ... i ) ( F ` n ) = ( F ` i ) )