Metamath Proof Explorer

Theorem iunincfi

Description: Given a sequence of increasing sets, the union of a finite subsequence, is its last element. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses iunincfi.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
iunincfi.2 
|- ( ( ph /\ n e. ( M ..^ N ) ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )
Assertion iunincfi 
|- ( ph -> U_ n e. ( M ... N ) ( F ` n ) = ( F ` N ) )

Proof

Step Hyp Ref Expression
1 iunincfi.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 iunincfi.2 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) )
3 eliun 
 |-  ( x e. U_ n e. ( M ... N ) ( F ` n ) <-> E. n e. ( M ... N ) x e. ( F ` n ) )
4 3 biimpi 
 |-  ( x e. U_ n e. ( M ... N ) ( F ` n ) -> E. n e. ( M ... N ) x e. ( F ` n ) )
5 4 adantl 
 |-  ( ( ph /\ x e. U_ n e. ( M ... N ) ( F ` n ) ) -> E. n e. ( M ... N ) x e. ( F ` n ) )
6 elfzuz3 
 |-  ( n e. ( M ... N ) -> N e. ( ZZ>= ` n ) )
7 6 adantl 
 |-  ( ( ph /\ n e. ( M ... N ) ) -> N e. ( ZZ>= ` n ) )
8 simpll 
 |-  ( ( ( ph /\ n e. ( M ... N ) ) /\ m e. ( n ..^ N ) ) -> ph )
9 elfzuz 
 |-  ( n e. ( M ... N ) -> n e. ( ZZ>= ` M ) )
10 fzoss1 
 |-  ( n e. ( ZZ>= ` M ) -> ( n ..^ N ) C_ ( M ..^ N ) )
11 9 10 syl 
 |-  ( n e. ( M ... N ) -> ( n ..^ N ) C_ ( M ..^ N ) )
12 11 adantr 
 |-  ( ( n e. ( M ... N ) /\ m e. ( n ..^ N ) ) -> ( n ..^ N ) C_ ( M ..^ N ) )
13 simpr 
 |-  ( ( n e. ( M ... N ) /\ m e. ( n ..^ N ) ) -> m e. ( n ..^ N ) )
14 12 13 sseldd 
 |-  ( ( n e. ( M ... N ) /\ m e. ( n ..^ N ) ) -> m e. ( M ..^ N ) )
15 14 adantll 
 |-  ( ( ( ph /\ n e. ( M ... N ) ) /\ m e. ( n ..^ N ) ) -> m e. ( M ..^ N ) )
16 eleq1w 
 |-  ( n = m -> ( n e. ( M ..^ N ) <-> m e. ( M ..^ N ) ) )
17 16 anbi2d 
 |-  ( n = m -> ( ( ph /\ n e. ( M ..^ N ) ) <-> ( ph /\ m e. ( M ..^ N ) ) ) )
18 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
19 fvoveq1 
 |-  ( n = m -> ( F ` ( n + 1 ) ) = ( F ` ( m + 1 ) ) )
20 18 19 sseq12d 
 |-  ( n = m -> ( ( F ` n ) C_ ( F ` ( n + 1 ) ) <-> ( F ` m ) C_ ( F ` ( m + 1 ) ) ) )
21 17 20 imbi12d 
 |-  ( n = m -> ( ( ( ph /\ n e. ( M ..^ N ) ) -> ( F ` n ) C_ ( F ` ( n + 1 ) ) ) <-> ( ( ph /\ m e. ( M ..^ N ) ) -> ( F ` m ) C_ ( F ` ( m + 1 ) ) ) ) )
22 21 2 chvarvv 
 |-  ( ( ph /\ m e. ( M ..^ N ) ) -> ( F ` m ) C_ ( F ` ( m + 1 ) ) )
23 8 15 22 syl2anc 
 |-  ( ( ( ph /\ n e. ( M ... N ) ) /\ m e. ( n ..^ N ) ) -> ( F ` m ) C_ ( F ` ( m + 1 ) ) )
24 7 23 ssinc 
 |-  ( ( ph /\ n e. ( M ... N ) ) -> ( F ` n ) C_ ( F ` N ) )
25 24 3adant3 
 |-  ( ( ph /\ n e. ( M ... N ) /\ x e. ( F ` n ) ) -> ( F ` n ) C_ ( F ` N ) )
26 simp3 
 |-  ( ( ph /\ n e. ( M ... N ) /\ x e. ( F ` n ) ) -> x e. ( F ` n ) )
27 25 26 sseldd 
 |-  ( ( ph /\ n e. ( M ... N ) /\ x e. ( F ` n ) ) -> x e. ( F ` N ) )
28 27 3exp 
 |-  ( ph -> ( n e. ( M ... N ) -> ( x e. ( F ` n ) -> x e. ( F ` N ) ) ) )
29 28 rexlimdv 
 |-  ( ph -> ( E. n e. ( M ... N ) x e. ( F ` n ) -> x e. ( F ` N ) ) )
30 29 imp 
 |-  ( ( ph /\ E. n e. ( M ... N ) x e. ( F ` n ) ) -> x e. ( F ` N ) )
31 5 30 syldan 
 |-  ( ( ph /\ x e. U_ n e. ( M ... N ) ( F ` n ) ) -> x e. ( F ` N ) )
32 31 ralrimiva 
 |-  ( ph -> A. x e. U_ n e. ( M ... N ) ( F ` n ) x e. ( F ` N ) )
33 dfss3 
 |-  ( U_ n e. ( M ... N ) ( F ` n ) C_ ( F ` N ) <-> A. x e. U_ n e. ( M ... N ) ( F ` n ) x e. ( F ` N ) )
34 32 33 sylibr 
 |-  ( ph -> U_ n e. ( M ... N ) ( F ` n ) C_ ( F ` N ) )
35 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
36 1 35 syl 
 |-  ( ph -> N e. ( M ... N ) )
37 fveq2 
 |-  ( n = N -> ( F ` n ) = ( F ` N ) )
38 37 ssiun2s 
 |-  ( N e. ( M ... N ) -> ( F ` N ) C_ U_ n e. ( M ... N ) ( F ` n ) )
39 36 38 syl 
 |-  ( ph -> ( F ` N ) C_ U_ n e. ( M ... N ) ( F ` n ) )
40 34 39 eqssd 
 |-  ( ph -> U_ n e. ( M ... N ) ( F ` n ) = ( F ` N ) )