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	$⊢ φ \to N \in ℤ_{\geq M}$
	iunincfi.2	$⊢ (φ \land n \in (M ..^N)) \to F (n) \subseteq F (n + 1)$
Assertion	iunincfi	$⊢ φ \to ⋃_{n = M}^{N} F (n) = F (N)$

Proof

Step	Hyp	Ref	Expression
1		iunincfi.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		iunincfi.2	$⊢ (φ \land n \in (M ..^N)) \to F (n) \subseteq F (n + 1)$
3		eliun	$⊢ x \in ⋃_{n = M}^{N} F (n) \leftrightarrow \exists n \in (M \dots N) x \in F (n)$
4	3	biimpi	$⊢ x \in ⋃_{n = M}^{N} F (n) \to \exists n \in (M \dots N) x \in F (n)$
5	4	adantl	$⊢ (φ \land x \in ⋃_{n = M}^{N} F (n)) \to \exists n \in (M \dots N) x \in F (n)$
6		elfzuz3	$⊢ n \in (M \dots N) \to N \in ℤ_{\geq n}$
7	6	adantl	$⊢ (φ \land n \in (M \dots N)) \to N \in ℤ_{\geq n}$
8		simpll	$⊢ ((φ \land n \in (M \dots N)) \land m \in (n ..^N)) \to φ$
9		elfzuz	$⊢ n \in (M \dots N) \to n \in ℤ_{\geq M}$
10		fzoss1	$⊢ n \in ℤ_{\geq M} \to (n ..^N) \subseteq (M ..^N)$
11	9 10	syl	$⊢ n \in (M \dots N) \to (n ..^N) \subseteq (M ..^N)$
12	11	adantr	$⊢ (n \in (M \dots N) \land m \in (n ..^N)) \to (n ..^N) \subseteq (M ..^N)$
13		simpr	$⊢ (n \in (M \dots N) \land m \in (n ..^N)) \to m \in (n ..^N)$
14	12 13	sseldd	$⊢ (n \in (M \dots N) \land m \in (n ..^N)) \to m \in (M ..^N)$
15	14	adantll	$⊢ ((φ \land n \in (M \dots N)) \land m \in (n ..^N)) \to m \in (M ..^N)$
16		eleq1w	$⊢ n = m \to (n \in (M ..^N) \leftrightarrow m \in (M ..^N))$
17	16	anbi2d	$⊢ n = m \to ((φ \land n \in (M ..^N)) \leftrightarrow (φ \land m \in (M ..^N)))$
18		fveq2	$⊢ n = m \to F (n) = F (m)$
19		fvoveq1	$⊢ n = m \to F (n + 1) = F (m + 1)$
20	18 19	sseq12d	$⊢ n = m \to (F (n) \subseteq F (n + 1) \leftrightarrow F (m) \subseteq F (m + 1))$
21	17 20	imbi12d	$⊢ n = m \to (((φ \land n \in (M ..^N)) \to F (n) \subseteq F (n + 1)) \leftrightarrow ((φ \land m \in (M ..^N)) \to F (m) \subseteq F (m + 1)))$
22	21 2	chvarvv	$⊢ (φ \land m \in (M ..^N)) \to F (m) \subseteq F (m + 1)$
23	8 15 22	syl2anc	$⊢ ((φ \land n \in (M \dots N)) \land m \in (n ..^N)) \to F (m) \subseteq F (m + 1)$
24	7 23	ssinc	$⊢ (φ \land n \in (M \dots N)) \to F (n) \subseteq F (N)$
25	24	3adant3	$⊢ (φ \land n \in (M \dots N) \land x \in F (n)) \to F (n) \subseteq F (N)$
26		simp3	$⊢ (φ \land n \in (M \dots N) \land x \in F (n)) \to x \in F (n)$
27	25 26	sseldd	$⊢ (φ \land n \in (M \dots N) \land x \in F (n)) \to x \in F (N)$
28	27	3exp	$⊢ φ \to (n \in (M \dots N) \to (x \in F (n) \to x \in F (N)))$
29	28	rexlimdv	$⊢ φ \to (\exists n \in (M \dots N) x \in F (n) \to x \in F (N))$
30	29	imp	$⊢ (φ \land \exists n \in (M \dots N) x \in F (n)) \to x \in F (N)$
31	5 30	syldan	$⊢ (φ \land x \in ⋃_{n = M}^{N} F (n)) \to x \in F (N)$
32	31	ralrimiva	$⊢ φ \to \forall x \in ⋃_{n = M}^{N} F (n) x \in F (N)$
33		dfss3	$⊢ ⋃_{n = M}^{N} F (n) \subseteq F (N) \leftrightarrow \forall x \in ⋃_{n = M}^{N} F (n) x \in F (N)$
34	32 33	sylibr	$⊢ φ \to ⋃_{n = M}^{N} F (n) \subseteq F (N)$
35		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
36	1 35	syl	$⊢ φ \to N \in (M \dots N)$
37		fveq2	$⊢ n = N \to F (n) = F (N)$
38	37	ssiun2s	$⊢ N \in (M \dots N) \to F (N) \subseteq ⋃_{n = M}^{N} F (n)$
39	36 38	syl	$⊢ φ \to F (N) \subseteq ⋃_{n = M}^{N} F (n)$
40	34 39	eqssd	$⊢ φ \to ⋃_{n = M}^{N} F (n) = F (N)$

Metamath Proof Explorer

Theorem iunincfi

Proof