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	biimpi	$⊢ 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	22	adantl	$⊢ (φ \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\}$
24		simp3	$⊢ (φ \land n \in ℕ \land y = \{x \in S \| F (n) = x \cap D\}) \to y = \{x \in S \| F (n) = x \cap D\}$
25	4	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to F (n) \in T$
26	25 3	eleqtrdi	$⊢ (φ \land n \in ℕ) \to F (n) \in (S ↾_{𝑡} D)$
27	2	elexd	$⊢ φ \to D \in V$
28		elrest	$⊢ (S \in SAlg \land D \in V) \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
29	1 27 28	syl2anc	$⊢ φ \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
30	29	adantr	$⊢ (φ \land n \in ℕ) \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
31	26 30	mpbid	$⊢ (φ \land n \in ℕ) \to \exists x \in S F (n) = x \cap D$
32		rabn0	$⊢ \{x \in S \| F (n) = x \cap D\} \neq \emptyset \leftrightarrow \exists x \in S F (n) = x \cap D$
33	31 32	sylibr	$⊢ (φ \land n \in ℕ) \to \{x \in S \| F (n) = x \cap D\} \neq \emptyset$
34	33	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$
35	24 34	eqnetrd	$⊢ (φ \land n \in ℕ \land y = \{x \in S \| F (n) = x \cap D\}) \to y \neq \emptyset$
36	35	3exp	$⊢ φ \to (n \in ℕ \to (y = \{x \in S \| F (n) = x \cap D\} \to y \neq \emptyset))$
37	36	rexlimdv	$⊢ φ \to (\exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\} \to y \neq \emptyset)$
38	37	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)$
39	23 38	mpd	$⊢ (φ \land y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})) \to y \neq \emptyset$
40	18 39	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)$
41		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 φ$
42		fveq2	$⊢ n = m \to F (n) = F (m)$
43	42	eqeq1d	$⊢ n = m \to (F (n) = x \cap D \leftrightarrow F (m) = x \cap D)$
44	43	rabbidv	$⊢ n = m \to \{x \in S \| F (n) = x \cap D\} = \{x \in S \| F (m) = x \cap D\}$
45	44	cbvmptv	$⊢ (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
46	45	rneqi	$⊢ ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
47	46	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\})$
48	47	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\})$
49	48	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\})$
50	46	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$
51	50	biimpi	$⊢ \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	51	adantl	$⊢ (φ \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$
53	52	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$
54		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)$
55	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$
56		ineq1	$⊢ x = z \to x \cap D = z \cap D$
57	56	eqeq2d	$⊢ x = z \to (F (m) = x \cap D \leftrightarrow F (m) = z \cap D)$
58	57	cbvrabv	$⊢ \{x \in S \| F (m) = x \cap D\} = \{z \in S \| F (m) = z \cap D\}$
59	58	mpteq2i	$⊢ (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) = (m \in ℕ ⟼ \{z \in S \| F (m) = z \cap D\})$
60	45 59	eqtr2i	$⊢ (m \in ℕ ⟼ \{z \in S \| F (m) = z \cap D\}) = (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
61	60	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\})$
62	47	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\})$
63	62	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\})$
64	46	eqcomi	$⊢ ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\}) = ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
65	64	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$
66		fveq2	$⊢ y = z \to f (y) = f (z)$
67		id	$⊢ y = z \to y = z$
68	66 67	eleq12d	$⊢ y = z \to (f (y) \in y \leftrightarrow f (z) \in z)$
69	68	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$
70	65 69	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$
71	70	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$
72	71	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$
73	54 55 8 61 63 72	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$
74	41 49 53 73	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$
75	74	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)$
76	75	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)$
77	40 76	mpd	$⊢ φ \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D$
78	1	3ad2ant1	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to S \in SAlg$
79	27	3ad2ant1	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to D \in V$
80	1	adantr	$⊢ (φ \land e \in (S^{ℕ})) \to S \in SAlg$
81		nnct	$⊢ ℕ ≼ ω$
82	81	a1i	$⊢ (φ \land e \in (S^{ℕ})) \to ℕ ≼ ω$
83		elmapi	$⊢ e \in (S^{ℕ}) \to e : ℕ ⟶ S$
84	83	adantl	$⊢ (φ \land e \in (S^{ℕ})) \to e : ℕ ⟶ S$
85	84	ffvelcdmda	$⊢ ((φ \land e \in (S^{ℕ})) \land n \in ℕ) \to e (n) \in S$
86	80 82 85	saliuncl	$⊢ (φ \land e \in (S^{ℕ})) \to ⋃_{n \in ℕ} e (n) \in S$
87	86	3adant3	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to ⋃_{n \in ℕ} e (n) \in S$
88		eqid	$⊢ ⋃_{n \in ℕ} e (n) \cap D = ⋃_{n \in ℕ} e (n) \cap D$
89	78 79 87 88	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)$
90		nfra1	$⊢ Ⅎ n \forall n \in ℕ F (n) = e (n) \cap D$
91		rspa	$⊢ (\forall n \in ℕ F (n) = e (n) \cap D \land n \in ℕ) \to F (n) = e (n) \cap D$
92	90 91	iuneq2df	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) = ⋃_{n \in ℕ} (e (n) \cap D)$
93		iunin1	$⊢ ⋃_{n \in ℕ} (e (n) \cap D) = ⋃_{n \in ℕ} e (n) \cap D$
94	93	a1i	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} (e (n) \cap D) = ⋃_{n \in ℕ} e (n) \cap D$
95	92 94	eqtrd	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) = ⋃_{n \in ℕ} e (n) \cap D$
96	95	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$
97	3	a1i	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to T = S ↾_{𝑡} D$
98	96 97	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))$
99	89 98	mpbird	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to ⋃_{n \in ℕ} F (n) \in T$
100	99	3exp	$⊢ φ \to (e \in (S^{ℕ}) \to (\forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) \in T))$
101	100	rexlimdv	$⊢ φ \to (\exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) \in T)$
102	77 101	mpd	$⊢ φ \to ⋃_{n \in ℕ} F (n) \in T$

Metamath Proof Explorer

Theorem subsaliuncl

Proof