iuninc

Description: The union of an increasing collection of sets is its last element. (Contributed by Thierry Arnoux, 22-Jan-2017)

	Ref	Expression
Hypotheses	iuninc.1	$⊢ φ \to F Fn ℕ$
	iuninc.2	$⊢ (φ \land n \in ℕ) \to F (n) \subseteq F (n + 1)$
Assertion	iuninc	$⊢ (φ \land i \in ℕ) \to ⋃_{n = 1}^{i} F (n) = F (i)$

Proof

Step	Hyp	Ref	Expression
1		iuninc.1	$⊢ φ \to F Fn ℕ$
2		iuninc.2	$⊢ (φ \land n \in ℕ) \to F (n) \subseteq F (n + 1)$
3		oveq2	$⊢ j = 1 \to (1 \dots j) = (1 \dots 1)$
4	3	iuneq1d	$⊢ j = 1 \to ⋃_{n = 1}^{j} F (n) = ⋃_{n = 1}^{1} F (n)$
5		fveq2	$⊢ j = 1 \to F (j) = F (1)$
6	4 5	eqeq12d	$⊢ j = 1 \to (⋃_{n = 1}^{j} F (n) = F (j) \leftrightarrow ⋃_{n = 1}^{1} F (n) = F (1))$
7	6	imbi2d	$⊢ j = 1 \to ((φ \to ⋃_{n = 1}^{j} F (n) = F (j)) \leftrightarrow (φ \to ⋃_{n = 1}^{1} F (n) = F (1)))$
8		oveq2	$⊢ j = k \to (1 \dots j) = (1 \dots k)$
9	8	iuneq1d	$⊢ j = k \to ⋃_{n = 1}^{j} F (n) = ⋃_{n = 1}^{k} F (n)$
10		fveq2	$⊢ j = k \to F (j) = F (k)$
11	9 10	eqeq12d	$⊢ j = k \to (⋃_{n = 1}^{j} F (n) = F (j) \leftrightarrow ⋃_{n = 1}^{k} F (n) = F (k))$
12	11	imbi2d	$⊢ j = k \to ((φ \to ⋃_{n = 1}^{j} F (n) = F (j)) \leftrightarrow (φ \to ⋃_{n = 1}^{k} F (n) = F (k)))$
13		oveq2	$⊢ j = k + 1 \to (1 \dots j) = (1 \dots k + 1)$
14	13	iuneq1d	$⊢ j = k + 1 \to ⋃_{n = 1}^{j} F (n) = ⋃_{n = 1}^{k + 1} F (n)$
15		fveq2	$⊢ j = k + 1 \to F (j) = F (k + 1)$
16	14 15	eqeq12d	$⊢ j = k + 1 \to (⋃_{n = 1}^{j} F (n) = F (j) \leftrightarrow ⋃_{n = 1}^{k + 1} F (n) = F (k + 1))$
17	16	imbi2d	$⊢ j = k + 1 \to ((φ \to ⋃_{n = 1}^{j} F (n) = F (j)) \leftrightarrow (φ \to ⋃_{n = 1}^{k + 1} F (n) = F (k + 1)))$
18		oveq2	$⊢ j = i \to (1 \dots j) = (1 \dots i)$
19	18	iuneq1d	$⊢ j = i \to ⋃_{n = 1}^{j} F (n) = ⋃_{n = 1}^{i} F (n)$
20		fveq2	$⊢ j = i \to F (j) = F (i)$
21	19 20	eqeq12d	$⊢ j = i \to (⋃_{n = 1}^{j} F (n) = F (j) \leftrightarrow ⋃_{n = 1}^{i} F (n) = F (i))$
22	21	imbi2d	$⊢ j = i \to ((φ \to ⋃_{n = 1}^{j} F (n) = F (j)) \leftrightarrow (φ \to ⋃_{n = 1}^{i} F (n) = F (i)))$
23		1z	$⊢ 1 \in ℤ$
24		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
25		iuneq1	$⊢ (1 \dots 1) = \{1\} \to ⋃_{n = 1}^{1} F (n) = ⋃_{n \in \{1\}} F (n)$
26	23 24 25	mp2b	$⊢ ⋃_{n = 1}^{1} F (n) = ⋃_{n \in \{1\}} F (n)$
27		1ex	$⊢ 1 \in V$
28		fveq2	$⊢ n = 1 \to F (n) = F (1)$
29	27 28	iunxsn	$⊢ ⋃_{n \in \{1\}} F (n) = F (1)$
30	26 29	eqtri	$⊢ ⋃_{n = 1}^{1} F (n) = F (1)$
31	30	a1i	$⊢ φ \to ⋃_{n = 1}^{1} F (n) = F (1)$
32		simpll	$⊢ ((k \in ℕ \land φ) \land ⋃_{n = 1}^{k} F (n) = F (k)) \to k \in ℕ$
33		elnnuz	$⊢ k \in ℕ \leftrightarrow k \in ℤ_{\geq 1}$
34		fzsuc	$⊢ k \in ℤ_{\geq 1} \to (1 \dots k + 1) = (1 \dots k) \cup \{k + 1\}$
35	33 34	sylbi	$⊢ k \in ℕ \to (1 \dots k + 1) = (1 \dots k) \cup \{k + 1\}$
36	35	iuneq1d	$⊢ k \in ℕ \to ⋃_{n = 1}^{k + 1} F (n) = ⋃_{n \in (1 \dots k) \cup \{k + 1\}} F (n)$
37		iunxun	$⊢ ⋃_{n \in (1 \dots k) \cup \{k + 1\}} F (n) = ⋃_{n = 1}^{k} F (n) \cup ⋃_{n \in \{k + 1\}} F (n)$
38		ovex	$⊢ k + 1 \in V$
39		fveq2	$⊢ n = k + 1 \to F (n) = F (k + 1)$
40	38 39	iunxsn	$⊢ ⋃_{n \in \{k + 1\}} F (n) = F (k + 1)$
41	40	uneq2i	$⊢ ⋃_{n = 1}^{k} F (n) \cup ⋃_{n \in \{k + 1\}} F (n) = ⋃_{n = 1}^{k} F (n) \cup F (k + 1)$
42	37 41	eqtri	$⊢ ⋃_{n \in (1 \dots k) \cup \{k + 1\}} F (n) = ⋃_{n = 1}^{k} F (n) \cup F (k + 1)$
43	36 42	eqtrdi	$⊢ k \in ℕ \to ⋃_{n = 1}^{k + 1} F (n) = ⋃_{n = 1}^{k} F (n) \cup F (k + 1)$
44	32 43	syl	$⊢ ((k \in ℕ \land φ) \land ⋃_{n = 1}^{k} F (n) = F (k)) \to ⋃_{n = 1}^{k + 1} F (n) = ⋃_{n = 1}^{k} F (n) \cup F (k + 1)$
45		simpr	$⊢ ((k \in ℕ \land φ) \land ⋃_{n = 1}^{k} F (n) = F (k)) \to ⋃_{n = 1}^{k} F (n) = F (k)$
46	45	uneq1d	$⊢ ((k \in ℕ \land φ) \land ⋃_{n = 1}^{k} F (n) = F (k)) \to ⋃_{n = 1}^{k} F (n) \cup F (k + 1) = F (k) \cup F (k + 1)$
47		simplr	$⊢ ((k \in ℕ \land φ) \land ⋃_{n = 1}^{k} F (n) = F (k)) \to φ$
48	2	sbt	$⊢ [k/ n] ((φ \land n \in ℕ) \to F (n) \subseteq F (n + 1))$
49		sbim	$⊢ [k/ n] ((φ \land n \in ℕ) \to F (n) \subseteq F (n + 1)) \leftrightarrow ([k/ n] (φ \land n \in ℕ) \to [k/ n] F (n) \subseteq F (n + 1))$
50		sban	$⊢ [k/ n] (φ \land n \in ℕ) \leftrightarrow ([k/ n] φ \land [k/ n] n \in ℕ)$
51		sbv	$⊢ [k/ n] φ \leftrightarrow φ$
52		clelsb1	$⊢ [k/ n] n \in ℕ \leftrightarrow k \in ℕ$
53	51 52	anbi12i	$⊢ ([k/ n] φ \land [k/ n] n \in ℕ) \leftrightarrow (φ \land k \in ℕ)$
54	50 53	bitr2i	$⊢ (φ \land k \in ℕ) \leftrightarrow [k/ n] (φ \land n \in ℕ)$
55		sbsbc	$⊢ [k/ n] F (n) \subseteq F (n + 1) \leftrightarrow \underset{˙}{[} k / n \underset{˙}{]} F (n) \subseteq F (n + 1)$
56		sbcssg	$⊢ k \in V \to (\underset{˙}{[} k / n \underset{˙}{]} F (n) \subseteq F (n + 1) \leftrightarrow ⦋ k / n ⦌ F (n) \subseteq ⦋ k / n ⦌ F (n + 1))$
57	56	elv	$⊢ \underset{˙}{[} k / n \underset{˙}{]} F (n) \subseteq F (n + 1) \leftrightarrow ⦋ k / n ⦌ F (n) \subseteq ⦋ k / n ⦌ F (n + 1)$
58		csbfv	$⊢ ⦋ k / n ⦌ F (n) = F (k)$
59		csbfv2g	$⊢ k \in V \to ⦋ k / n ⦌ F (n + 1) = F (⦋ k / n ⦌ (n + 1))$
60	59	elv	$⊢ ⦋ k / n ⦌ F (n + 1) = F (⦋ k / n ⦌ (n + 1))$
61		csbov1g	$⊢ k \in V \to ⦋ k / n ⦌ (n + 1) = ⦋ k / n ⦌ n + 1$
62	61	elv	$⊢ ⦋ k / n ⦌ (n + 1) = ⦋ k / n ⦌ n + 1$
63	62	fveq2i	$⊢ F (⦋ k / n ⦌ (n + 1)) = F (⦋ k / n ⦌ n + 1)$
64		vex	$⊢ k \in V$
65	64	csbvargi	$⊢ ⦋ k / n ⦌ n = k$
66	65	oveq1i	$⊢ ⦋ k / n ⦌ n + 1 = k + 1$
67	66	fveq2i	$⊢ F (⦋ k / n ⦌ n + 1) = F (k + 1)$
68	60 63 67	3eqtri	$⊢ ⦋ k / n ⦌ F (n + 1) = F (k + 1)$
69	58 68	sseq12i	$⊢ ⦋ k / n ⦌ F (n) \subseteq ⦋ k / n ⦌ F (n + 1) \leftrightarrow F (k) \subseteq F (k + 1)$
70	55 57 69	3bitrri	$⊢ F (k) \subseteq F (k + 1) \leftrightarrow [k/ n] F (n) \subseteq F (n + 1)$
71	54 70	imbi12i	$⊢ ((φ \land k \in ℕ) \to F (k) \subseteq F (k + 1)) \leftrightarrow ([k/ n] (φ \land n \in ℕ) \to [k/ n] F (n) \subseteq F (n + 1))$
72	49 71	bitr4i	$⊢ [k/ n] ((φ \land n \in ℕ) \to F (n) \subseteq F (n + 1)) \leftrightarrow ((φ \land k \in ℕ) \to F (k) \subseteq F (k + 1))$
73	48 72	mpbi	$⊢ (φ \land k \in ℕ) \to F (k) \subseteq F (k + 1)$
74		ssequn1	$⊢ F (k) \subseteq F (k + 1) \leftrightarrow F (k) \cup F (k + 1) = F (k + 1)$
75	73 74	sylib	$⊢ (φ \land k \in ℕ) \to F (k) \cup F (k + 1) = F (k + 1)$
76	47 32 75	syl2anc	$⊢ ((k \in ℕ \land φ) \land ⋃_{n = 1}^{k} F (n) = F (k)) \to F (k) \cup F (k + 1) = F (k + 1)$
77	44 46 76	3eqtrd	$⊢ ((k \in ℕ \land φ) \land ⋃_{n = 1}^{k} F (n) = F (k)) \to ⋃_{n = 1}^{k + 1} F (n) = F (k + 1)$
78	77	exp31	$⊢ k \in ℕ \to (φ \to (⋃_{n = 1}^{k} F (n) = F (k) \to ⋃_{n = 1}^{k + 1} F (n) = F (k + 1)))$
79	78	a2d	$⊢ k \in ℕ \to ((φ \to ⋃_{n = 1}^{k} F (n) = F (k)) \to (φ \to ⋃_{n = 1}^{k + 1} F (n) = F (k + 1)))$
80	7 12 17 22 31 79	nnind	$⊢ i \in ℕ \to (φ \to ⋃_{n = 1}^{i} F (n) = F (i))$
81	80	impcom	$⊢ (φ \land i \in ℕ) \to ⋃_{n = 1}^{i} F (n) = F (i)$

Metamath Proof Explorer

Theorem iuninc

Proof