subsaliuncl

Description: A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of Fremlin1 p. 35. The proof uses fnrndomnum rather than fnrndomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 26-Jun-2021) (Revised by Vincent Gonzalez, 30-Aug-2026)

	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		omelon	$⊢ ω \in On$
12		nnct	$⊢ ℕ ≼ ω$
13		ondomen	$⊢ (ω \in On \land ℕ ≼ ω) \to ℕ \in dom card$
14	11 12 13	mp2an	$⊢ ℕ \in dom card$
15		fnrndomnum	$⊢ ℕ \in dom card \to ((n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) Fn ℕ \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ℕ)$
16	14 15	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\}) ≼ ℕ$
17	10 16	syl	$⊢ φ \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ℕ$
18	12	a1i	$⊢ φ \to ℕ ≼ ω$
19		domtr	$⊢ (ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ℕ \land ℕ ≼ ω) \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ω$
20	17 18 19	syl2anc	$⊢ φ \to ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) ≼ ω$
21		vex	$⊢ y \in V$
22	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\})$
23	21 22	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\}$
24	23	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\}$
25		simp3	$⊢ (φ \land n \in ℕ \land y = \{x \in S \| F (n) = x \cap D\}) \to y = \{x \in S \| F (n) = x \cap D\}$
26	4	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to F (n) \in T$
27	26 3	eleqtrdi	$⊢ (φ \land n \in ℕ) \to F (n) \in (S ↾_{𝑡} D)$
28	2	elexd	$⊢ φ \to D \in V$
29		elrest	$⊢ (S \in SAlg \land D \in V) \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
30	1 28 29	syl2anc	$⊢ φ \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
31	30	adantr	$⊢ (φ \land n \in ℕ) \to (F (n) \in (S ↾_{𝑡} D) \leftrightarrow \exists x \in S F (n) = x \cap D)$
32	27 31	mpbid	$⊢ (φ \land n \in ℕ) \to \exists x \in S F (n) = x \cap D$
33		rabn0	$⊢ \{x \in S \| F (n) = x \cap D\} \neq \emptyset \leftrightarrow \exists x \in S F (n) = x \cap D$
34	32 33	sylibr	$⊢ (φ \land n \in ℕ) \to \{x \in S \| F (n) = x \cap D\} \neq \emptyset$
35	34	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$
36	25 35	eqnetrd	$⊢ (φ \land n \in ℕ \land y = \{x \in S \| F (n) = x \cap D\}) \to y \neq \emptyset$
37	36	3exp	$⊢ φ \to (n \in ℕ \to (y = \{x \in S \| F (n) = x \cap D\} \to y \neq \emptyset))$
38	37	rexlimdv	$⊢ φ \to (\exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\} \to y \neq \emptyset)$
39	38	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)$
40	24 39	mpd	$⊢ (φ \land y \in ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})) \to y \neq \emptyset$
41	20 40	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)$
42		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 φ$
43		fveq2	$⊢ n = m \to F (n) = F (m)$
44	43	eqeq1d	$⊢ n = m \to (F (n) = x \cap D \leftrightarrow F (m) = x \cap D)$
45	44	rabbidv	$⊢ n = m \to \{x \in S \| F (n) = x \cap D\} = \{x \in S \| F (m) = x \cap D\}$
46	45	cbvmptv	$⊢ (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
47	46	rneqi	$⊢ ran (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = ran (m \in ℕ ⟼ \{x \in S \| F (m) = x \cap D\})$
48	47	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\})$
49	48	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\})$
50	49	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\})$
51	47	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$
52	51	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$
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	46 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	48	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	47	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	42 50 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	41 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	28	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	12	a1i	$⊢ (φ \land e \in (S^{ℕ})) \to ℕ ≼ ω$
82		elmapi	$⊢ e \in (S^{ℕ}) \to e : ℕ ⟶ S$
83	82	adantl	$⊢ (φ \land e \in (S^{ℕ})) \to e : ℕ ⟶ S$
84	83	ffvelcdmda	$⊢ ((φ \land e \in (S^{ℕ})) \land n \in ℕ) \to e (n) \in S$
85	80 81 84	saliuncl	$⊢ (φ \land e \in (S^{ℕ})) \to ⋃_{n \in ℕ} e (n) \in S$
86	85	3adant3	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to ⋃_{n \in ℕ} e (n) \in S$
87		eqid	$⊢ ⋃_{n \in ℕ} e (n) \cap D = ⋃_{n \in ℕ} e (n) \cap D$
88	78 79 86 87	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)$
89		nfra1	$⊢ Ⅎ n \forall n \in ℕ F (n) = e (n) \cap D$
90		rspa	$⊢ (\forall n \in ℕ F (n) = e (n) \cap D \land n \in ℕ) \to F (n) = e (n) \cap D$
91	89 90	iuneq2df	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) = ⋃_{n \in ℕ} (e (n) \cap D)$
92		iunin1	$⊢ ⋃_{n \in ℕ} (e (n) \cap D) = ⋃_{n \in ℕ} e (n) \cap D$
93	92	a1i	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} (e (n) \cap D) = ⋃_{n \in ℕ} e (n) \cap D$
94	91 93	eqtrd	$⊢ \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) = ⋃_{n \in ℕ} e (n) \cap D$
95	94	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$
96	3	a1i	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to T = S ↾_{𝑡} D$
97	95 96	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))$
98	88 97	mpbird	$⊢ (φ \land e \in (S^{ℕ}) \land \forall n \in ℕ F (n) = e (n) \cap D) \to ⋃_{n \in ℕ} F (n) \in T$
99	98	3exp	$⊢ φ \to (e \in (S^{ℕ}) \to (\forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) \in T))$
100	99	rexlimdv	$⊢ φ \to (\exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D \to ⋃_{n \in ℕ} F (n) \in T)$
101	77 100	mpd	$⊢ φ \to ⋃_{n \in ℕ} F (n) \in T$

Metamath Proof Explorer

Theorem subsaliuncl

Proof