subsaliuncl

Description: A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of Fremlin1 p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	subsaliuncl.1	$⊢ φ \to S \in SAlg$
	subsaliuncl.2	$⊢ φ \to D \in V$
	subsaliuncl.3	$⊢ T = S ↾_{𝑡} D$
	subsaliuncl.4	$⊢ φ \to F : ℕ ⟶ T$
Assertion	subsaliuncl	$⊢ φ \to ⋃_{n \in ℕ} F (n) \in T$

Proof

Step	Hyp	Ref	Expression
1		subsaliuncl.1	$⊢ φ \to S \in SAlg$
2		subsaliuncl.2	$⊢ φ \to D \in V$
3		subsaliuncl.3	$⊢ T = S ↾_{𝑡} D$
4		subsaliuncl.4	$⊢ φ \to F : ℕ ⟶ T$
5		eqid	$⊢ \{x \in S \| F (n) = x \cap D\} = \{x \in S \| F (n) = x \cap D\}$
6	5 1	rabexd	$⊢ φ \to \{x \in S \| F (n) = x \cap D\} \in V$
7	6	ralrimivw	$⊢ φ \to \forall n \in ℕ \{x \in S \| F (n) = x \cap D\} \in V$
8		eqid	$⊢ (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
9	8	fnmpt	$⊢ \forall n \in ℕ \{x \in S \| F (n) = x \cap D\} \in V \to (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) Fn ℕ$
10	7 9	syl	$⊢ φ \to (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) Fn ℕ$
11		nnex	$⊢ ℕ \in V$
12		fnrndomg	$⊢ ℕ \in V \to ((n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) Fn ℕ \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ℕ)$
13	11 12	ax-mp	$⊢ (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) Fn ℕ \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ℕ$
14	10 13	syl	$⊢ φ \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ℕ$
15		nnenom	$⊢ ℕ \approx ω$
16	15	a1i	$⊢ φ \to ℕ \approx ω$
17		domentr	$⊢ (ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ℕ \land ℕ \approx ω) \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ω$
18	14 16 17	syl2anc	$⊢ φ \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ω$
19		vex	$⊢ y \in V$
20	8	elrnmpt	$⊢ y \in V \to (y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \leftrightarrow \exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\})$
21	19 20	ax-mp	$⊢ y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \leftrightarrow \exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\}$
22	21	bilani	$⊢ (φ \land y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})) \to \exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\}$
23		simp3	$⊢ (φ \land n \in ℕ \land y = \{x \in S \| F (n) = x \cap D\}) \to y = \{x \in S \| F (n) = x \cap D\}$
24	4	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to F (n) \in T$
25	24 3	eleqtrdi	$⊢ (φ \land n \in ℕ) \to F (n) \in (S ↾_{𝑡} D)$
26	2	elexd	$⊢ φ \to D \in V$
27		elrest	$⊢ (S \in SAlg \land D \in V) \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
28	1 26 27	syl2anc	$⊢ φ \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
29	28	adantr	$⊢ (φ \land n \in ℕ) \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
30	25 29	mpbid	$⊢ (φ \land n \in ℕ) \to \exists x \in S F (n) = x \cap D$
31		rabn0	$⊢ \{x \in S \| F (n) = x \cap D\} \neq \emptyset \leftrightarrow \exists x \in S F (n) = x \cap D$
32	30 31	sylibr	$⊢ (φ \land n \in ℕ) \to \{x \in S \| F (n) = x \cap D\} \neq \emptyset$
33	32	3adant3	$⊢ (φ \land n \in ℕ \land y = \{x \in S \| F (n) = x \cap D\}) \to \{x \in S \| F (n) = x \cap D\} \neq \emptyset$
34	23 33	eqnetrd	$⊢ (φ \land n \in ℕ \land y = \{x \in S \| F (n) = x \cap D\}) \to y \neq \emptyset$
35	34	3exp	$⊢ φ \to (n \in ℕ \to (y = \{x \in S \| F (n) = x \cap D\} \to y \neq \emptyset))$
36	35	rexlimdv	$⊢ φ \to (\exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\} \to y \neq \emptyset)$
37	36	adantr	$⊢ (φ \land y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})) \to (\exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\} \to y \neq \emptyset)$
38	22 37	mpd	$⊢ (φ \land y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})) \to y \neq \emptyset$
39	18 38	axccdom	$⊢ φ \to \exists f (f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \land \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y)$
40		simpl	$⊢ (φ \land (f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \land \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y)) \to φ$
41		fveq2	$⊢ n = m \to F (n) = F (m)$
42	41	eqeq1d	$⊢ n = m \to (F (n) = x \cap D \leftrightarrow F (m) = x \cap D)$
43	42	rabbidv	$⊢ n = m \to \{x \in S \| F (n) = x \cap D\} = \{x \in S \| F (m) = x \cap D\}$
44	43	cbvmptv	$⊢ (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
45	44	rneqi	$⊢ ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
46	45	fneq2i	$⊢ f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \leftrightarrow f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
47	46	biimpi	$⊢ f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \to f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
48	47	ad2antrl	$⊢ (φ \land (f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \land \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y)) \to f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
49	45	raleqi	$⊢ \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y \leftrightarrow \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y$
50	49	bilani	$⊢ (φ \land \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y) \to \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y$
51	50	adantrl	$⊢ (φ \land (f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \land \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y)) \to \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y$
52		nfv	$⊢ Ⅎ z (φ \land f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) \land \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y)$
53	1	3ad2ant1	$⊢ (φ \land f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) \land \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y) \to S \in SAlg$
54		ineq1	$⊢ x = z \to x \cap D = z \cap D$
55	54	eqeq2d	$⊢ x = z \to (F (m) = x \cap D \leftrightarrow F (m) = z \cap D)$
56	55	cbvrabv	$⊢ \{x \in S \| F (m) = x \cap D\} = \{z \in S \| F (m) = z \cap D\}$
57	56	mpteq2i	$⊢ (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) = (m \in ℕ ⟼ \{z \in S \| F (m) = z \cap D\})$
58	44 57	eqtr2i	$⊢ (m \in ℕ ⟼ \{z \in S \| F (m) = z \cap D\}) = (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
59	58	coeq2i	$⊢ f \circ (m \in ℕ ⟼ \{z \in S \| F (m) = z \cap D\}) = f \circ (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
60	46	biimpri	$⊢ f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) \to f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
61	60	3ad2ant2	$⊢ (φ \land f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) \land \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y) \to f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
62	45	eqcomi	$⊢ ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) = ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
63	62	raleqi	$⊢ \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y \leftrightarrow \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y$
64		fveq2	$⊢ y = z \to f (y) = f (z)$
65		id	$⊢ y = z \to y = z$
66	64 65	eleq12d	$⊢ y = z \to (f (y) \in y \leftrightarrow f (z) \in z)$
67	66	cbvralvw	$⊢ \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y \leftrightarrow \forall z \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (z) \in z$
68	63 67	bitri	$⊢ \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y \leftrightarrow \forall z \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (z) \in z$
69	68	biimpi	$⊢ \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y \to \forall z \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (z) \in z$
70	69	3ad2ant3	$⊢ (φ \land f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) \land \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y) \to \forall z \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (z) \in z$
71	52 53 8 59 61 70	subsaliuncllem	$⊢ (φ \land f Fn ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) \land \forall y \in ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) f (y) \in y) \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D$
72	40 48 51 71	syl3anc	$⊢ (φ \land (f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \land \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y)) \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D$
73	72	ex	$⊢ φ \to ((f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \land \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y) \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D)$
74	73	exlimdv	$⊢ φ \to (\exists f (f Fn ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) \land \forall y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) f (y) \in y) \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D)$
75	39 74	mpd	$⊢ φ \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D$
76	1	3ad2ant1	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to S \in SAlg$
77	26	3ad2ant1	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to D \in V$
78	1	adantr	$⊢ (φ \land e \in (S^{ℕ})) \to S \in SAlg$
79		nnct	$⊢ ℕ ≼ ω$
80	79	a1i	$⊢ (φ \land e \in (S^{ℕ})) \to ℕ ≼ ω$
81		elmapi	$⊢ e \in (S^{ℕ}) \to e : ℕ ⟶ S$
82	81	adantl	$⊢ (φ \land e \in (S^{ℕ})) \to e : ℕ ⟶ S$
83	82	ffvelcdmda	$⊢ ((φ \land e \in (S^{ℕ})) \land n \in ℕ) \to e (n) \in S$
84	78 80 83	saliuncl	$⊢ (φ \land e \in (S^{ℕ})) \to ⋃_{n \in ℕ} e (n) \in S$
85	84	3adant3	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to ⋃_{n \in ℕ} e (n) \in S$
86		eqid	$⊢ ⋃_{n \in ℕ} e (n) \cap D = ⋃_{n \in ℕ} e (n) \cap D$
87	76 77 85 86	elrestd	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to ⋃_{n \in ℕ} e (n) \cap D \in (S ↾_{𝑡} D)$
88		nfra1	$⊢ Ⅎ n \forall n \in ℕ F (n) = e (n) \cap D$
89		rspa	$⊢ (\forall n \in ℕ F (n) = e (n) \cap D \land n \in ℕ) \to F (n) = e (n) \cap D$
90	88 89	iuneq2df	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) = ⋃_{n \in ℕ} (e (n) \cap D)$
91		iunin1	$⊢ ⋃_{n \in ℕ} (e (n) \cap D) = ⋃_{n \in ℕ} e (n) \cap D$
92	91	a1i	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} (e (n) \cap D) = ⋃_{n \in ℕ} e (n) \cap D$
93	90 92	eqtrd	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) = ⋃_{n \in ℕ} e (n) \cap D$
94	93	3ad2ant3	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to ⋃_{n \in ℕ} F (n) = ⋃_{n \in ℕ} e (n) \cap D$
95	3	a1i	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to T = S ↾_{𝑡} D$
96	94 95	eleq12d	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to (⋃_{n \in ℕ} F (n) \in T \leftrightarrow ⋃_{n \in ℕ} e (n) \cap D \in (S ↾_{𝑡} D))$
97	87 96	mpbird	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to ⋃_{n \in ℕ} F (n) \in T$
98	97	3exp	$⊢ φ \to (e \in (S^{ℕ}) \to (\forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) \in T))$
99	98	rexlimdv	$⊢ φ \to (\exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) \in T)$
100	75 99	mpd	$⊢ φ \to ⋃_{n \in ℕ} F (n) \in T$

Metamath Proof Explorer

Theorem subsaliuncl

Proof