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