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

Metamath Proof Explorer

Theorem iunincfi

Proof