fiunelros

Description: A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020)

	Ref	Expression
Hypotheses	isros.1	$⊢ Q = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s))\}$
	fiunelros.1	$⊢ φ \to S \in Q$
	fiunelros.2	$⊢ φ \to N \in ℕ$
	fiunelros.3	$⊢ (φ \land k \in (1 ..^N)) \to B \in S$
Assertion	fiunelros	$⊢ φ \to ⋃_{k \in (1 ..^N)} B \in S$

Proof

Step	Hyp	Ref	Expression
1		isros.1	$⊢ Q = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s))\}$
2		fiunelros.1	$⊢ φ \to S \in Q$
3		fiunelros.2	$⊢ φ \to N \in ℕ$
4		fiunelros.3	$⊢ (φ \land k \in (1 ..^N)) \to B \in S$
5		simpr	$⊢ (φ \land N \in ℕ) \to N \in ℕ$
6	5	nnred	$⊢ (φ \land N \in ℕ) \to N \in ℝ$
7	6	leidd	$⊢ (φ \land N \in ℕ) \to N \leq N$
8		breq1	$⊢ n = 1 \to (n \leq N \leftrightarrow 1 \leq N)$
9		oveq2	$⊢ n = 1 \to (1 ..^n) = (1 ..^1)$
10	9	iuneq1d	$⊢ n = 1 \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^1)} B$
11	10	eleq1d	$⊢ n = 1 \to (⋃_{k \in (1 ..^n)} B \in S \leftrightarrow ⋃_{k \in (1 ..^1)} B \in S)$
12	8 11	imbi12d	$⊢ n = 1 \to ((n \leq N \to ⋃_{k \in (1 ..^n)} B \in S) \leftrightarrow (1 \leq N \to ⋃_{k \in (1 ..^1)} B \in S))$
13		breq1	$⊢ n = i \to (n \leq N \leftrightarrow i \leq N)$
14		oveq2	$⊢ n = i \to (1 ..^n) = (1 ..^i)$
15	14	iuneq1d	$⊢ n = i \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^i)} B$
16	15	eleq1d	$⊢ n = i \to (⋃_{k \in (1 ..^n)} B \in S \leftrightarrow ⋃_{k \in (1 ..^i)} B \in S)$
17	13 16	imbi12d	$⊢ n = i \to ((n \leq N \to ⋃_{k \in (1 ..^n)} B \in S) \leftrightarrow (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S))$
18		breq1	$⊢ n = i + 1 \to (n \leq N \leftrightarrow i + 1 \leq N)$
19		oveq2	$⊢ n = i + 1 \to (1 ..^n) = (1 ..^i + 1)$
20	19	iuneq1d	$⊢ n = i + 1 \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^i + 1)} B$
21	20	eleq1d	$⊢ n = i + 1 \to (⋃_{k \in (1 ..^n)} B \in S \leftrightarrow ⋃_{k \in (1 ..^i + 1)} B \in S)$
22	18 21	imbi12d	$⊢ n = i + 1 \to ((n \leq N \to ⋃_{k \in (1 ..^n)} B \in S) \leftrightarrow (i + 1 \leq N \to ⋃_{k \in (1 ..^i + 1)} B \in S))$
23		breq1	$⊢ n = N \to (n \leq N \leftrightarrow N \leq N)$
24		oveq2	$⊢ n = N \to (1 ..^n) = (1 ..^N)$
25	24	iuneq1d	$⊢ n = N \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^N)} B$
26	25	eleq1d	$⊢ n = N \to (⋃_{k \in (1 ..^n)} B \in S \leftrightarrow ⋃_{k \in (1 ..^N)} B \in S)$
27	23 26	imbi12d	$⊢ n = N \to ((n \leq N \to ⋃_{k \in (1 ..^n)} B \in S) \leftrightarrow (N \leq N \to ⋃_{k \in (1 ..^N)} B \in S))$
28		fzo0	$⊢ (1 ..^1) = \emptyset$
29		iuneq1	$⊢ (1 ..^1) = \emptyset \to ⋃_{k \in (1 ..^1)} B = ⋃_{k \in \emptyset} B$
30	28 29	ax-mp	$⊢ ⋃_{k \in (1 ..^1)} B = ⋃_{k \in \emptyset} B$
31		0iun	$⊢ ⋃_{k \in \emptyset} B = \emptyset$
32	30 31	eqtri	$⊢ ⋃_{k \in (1 ..^1)} B = \emptyset$
33	1	0elros	$⊢ S \in Q \to \emptyset \in S$
34	2 33	syl	$⊢ φ \to \emptyset \in S$
35	32 34	eqeltrid	$⊢ φ \to ⋃_{k \in (1 ..^1)} B \in S$
36	35	a1d	$⊢ φ \to (1 \leq N \to ⋃_{k \in (1 ..^1)} B \in S)$
37		simpllr	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to i \in ℕ$
38		fzosplitsn	$⊢ i \in ℤ_{\geq 1} \to (1 ..^i + 1) = (1 ..^i) \cup \{i\}$
39		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
40	38 39	eleq2s	$⊢ i \in ℕ \to (1 ..^i + 1) = (1 ..^i) \cup \{i\}$
41	40	iuneq1d	$⊢ i \in ℕ \to ⋃_{k \in (1 ..^i + 1)} B = ⋃_{k \in (1 ..^i) \cup \{i\}} B$
42	37 41	syl	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to ⋃_{k \in (1 ..^i + 1)} B = ⋃_{k \in (1 ..^i) \cup \{i\}} B$
43		iunxun	$⊢ ⋃_{k \in (1 ..^i) \cup \{i\}} B = ⋃_{k \in (1 ..^i)} B \cup ⋃_{k \in \{i\}} B$
44	42 43	eqtrdi	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to ⋃_{k \in (1 ..^i + 1)} B = ⋃_{k \in (1 ..^i)} B \cup ⋃_{k \in \{i\}} B$
45	2	ad3antrrr	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to S \in Q$
46	37	nnred	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to i \in ℝ$
47	3	ad3antrrr	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to N \in ℕ$
48	47	nnred	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to N \in ℝ$
49		simpr	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to i + 1 \leq N$
50		nnltp1le	$⊢ (i \in ℕ \land N \in ℕ) \to (i < N \leftrightarrow i + 1 \leq N)$
51	37 47 50	syl2anc	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to (i < N \leftrightarrow i + 1 \leq N)$
52	49 51	mpbird	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to i < N$
53	46 48 52	ltled	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to i \leq N$
54		simplr	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)$
55	53 54	mpd	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to ⋃_{k \in (1 ..^i)} B \in S$
56		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ i / k ⦌ B$
57		csbeq1a	$⊢ k = i \to B = ⦋ i / k ⦌ B$
58	56 57	iunxsngf	$⊢ i \in ℕ \to ⋃_{k \in \{i\}} B = ⦋ i / k ⦌ B$
59	37 58	syl	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to ⋃_{k \in \{i\}} B = ⦋ i / k ⦌ B$
60		simplll	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to φ$
61		elfzo1	$⊢ i \in (1 ..^N) \leftrightarrow (i \in ℕ \land N \in ℕ \land i < N)$
62	37 47 52 61	syl3anbrc	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to i \in (1 ..^N)$
63		nfv	$⊢ Ⅎ k (φ \land i \in (1 ..^N))$
64		nfcv	$⊢ \underline{Ⅎ} k S$
65	56 64	nfel	$⊢ Ⅎ k ⦋ i / k ⦌ B \in S$
66	63 65	nfim	$⊢ Ⅎ k ((φ \land i \in (1 ..^N)) \to ⦋ i / k ⦌ B \in S)$
67		eleq1w	$⊢ k = i \to (k \in (1 ..^N) \leftrightarrow i \in (1 ..^N))$
68	67	anbi2d	$⊢ k = i \to ((φ \land k \in (1 ..^N)) \leftrightarrow (φ \land i \in (1 ..^N)))$
69	57	eleq1d	$⊢ k = i \to (B \in S \leftrightarrow ⦋ i / k ⦌ B \in S)$
70	68 69	imbi12d	$⊢ k = i \to (((φ \land k \in (1 ..^N)) \to B \in S) \leftrightarrow ((φ \land i \in (1 ..^N)) \to ⦋ i / k ⦌ B \in S))$
71	66 70 4	chvarfv	$⊢ (φ \land i \in (1 ..^N)) \to ⦋ i / k ⦌ B \in S$
72	60 62 71	syl2anc	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to ⦋ i / k ⦌ B \in S$
73	59 72	eqeltrd	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to ⋃_{k \in \{i\}} B \in S$
74	1	unelros	$⊢ (S \in Q \land ⋃_{k \in (1 ..^i)} B \in S \land ⋃_{k \in \{i\}} B \in S) \to ⋃_{k \in (1 ..^i)} B \cup ⋃_{k \in \{i\}} B \in S$
75	45 55 73 74	syl3anc	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to ⋃_{k \in (1 ..^i)} B \cup ⋃_{k \in \{i\}} B \in S$
76	44 75	eqeltrd	$⊢ (((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \land i + 1 \leq N) \to ⋃_{k \in (1 ..^i + 1)} B \in S$
77	76	ex	$⊢ ((φ \land i \in ℕ) \land (i \leq N \to ⋃_{k \in (1 ..^i)} B \in S)) \to (i + 1 \leq N \to ⋃_{k \in (1 ..^i + 1)} B \in S)$
78	12 17 22 27 36 77	nnindd	$⊢ (φ \land N \in ℕ) \to (N \leq N \to ⋃_{k \in (1 ..^N)} B \in S)$
79	7 78	mpd	$⊢ (φ \land N \in ℕ) \to ⋃_{k \in (1 ..^N)} B \in S$
80	3 79	mpdan	$⊢ φ \to ⋃_{k \in (1 ..^N)} B \in S$

Metamath Proof Explorer

Theorem fiunelros

Proof