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

Metamath Proof Explorer

Theorem iunincfi

Proof