subsaliuncllem

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	subsaliuncllem.f	$⊢ Ⅎ y φ$
	subsaliuncllem.s	$⊢ φ \to S \in V$
	subsaliuncllem.g	$⊢ G = (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
	subsaliuncllem.e	$⊢ E = H \circ G$
	subsaliuncllem.h	$⊢ φ \to H Fn ran G$
	subsaliuncllem.y	$⊢ φ \to \forall y \in ran G H (y) \in y$
Assertion	subsaliuncllem	$⊢ φ \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D$

Proof

Step	Hyp	Ref	Expression
1		subsaliuncllem.f	$⊢ Ⅎ y φ$
2		subsaliuncllem.s	$⊢ φ \to S \in V$
3		subsaliuncllem.g	$⊢ G = (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
4		subsaliuncllem.e	$⊢ E = H \circ G$
5		subsaliuncllem.h	$⊢ φ \to H Fn ran G$
6		subsaliuncllem.y	$⊢ φ \to \forall y \in ran G H (y) \in y$
7		vex	$⊢ y \in V$
8	3	elrnmpt	$⊢ y \in V \to (y \in ran G \leftrightarrow \exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\})$
9	7 8	ax-mp	$⊢ y \in ran G \leftrightarrow \exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\}$
10	9	biimpi	$⊢ y \in ran G \to \exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\}$
11		id	$⊢ y = \{x \in S \| F (n) = x \cap D\} \to y = \{x \in S \| F (n) = x \cap D\}$
12		ssrab2	$⊢ \{x \in S \| F (n) = x \cap D\} \subseteq S$
13	12	a1i	$⊢ y = \{x \in S \| F (n) = x \cap D\} \to \{x \in S \| F (n) = x \cap D\} \subseteq S$
14	11 13	eqsstrd	$⊢ y = \{x \in S \| F (n) = x \cap D\} \to y \subseteq S$
15	14	a1i	$⊢ n \in ℕ \to (y = \{x \in S \| F (n) = x \cap D\} \to y \subseteq S)$
16	15	rexlimiv	$⊢ \exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\} \to y \subseteq S$
17	16	a1i	$⊢ y \in ran G \to (\exists n \in ℕ y = \{x \in S \| F (n) = x \cap D\} \to y \subseteq S)$
18	10 17	mpd	$⊢ y \in ran G \to y \subseteq S$
19	18	adantl	$⊢ (φ \land y \in ran G) \to y \subseteq S$
20	6	r19.21bi	$⊢ (φ \land y \in ran G) \to H (y) \in y$
21	19 20	sseldd	$⊢ (φ \land y \in ran G) \to H (y) \in S$
22	21	ex	$⊢ φ \to (y \in ran G \to H (y) \in S)$
23	1 22	ralrimi	$⊢ φ \to \forall y \in ran G H (y) \in S$
24	5 23	jca	$⊢ φ \to (H Fn ran G \land \forall y \in ran G H (y) \in S)$
25		ffnfv	$⊢ H : ran G ⟶ S \leftrightarrow (H Fn ran G \land \forall y \in ran G H (y) \in S)$
26	24 25	sylibr	$⊢ φ \to H : ran G ⟶ S$
27		eqid	$⊢ \{x \in S \| F (n) = x \cap D\} = \{x \in S \| F (n) = x \cap D\}$
28	27 2	rabexd	$⊢ φ \to \{x \in S \| F (n) = x \cap D\} \in V$
29	28	ralrimivw	$⊢ φ \to \forall n \in ℕ \{x \in S \| F (n) = x \cap D\} \in V$
30	3	fnmpt	$⊢ \forall n \in ℕ \{x \in S \| F (n) = x \cap D\} \in V \to G Fn ℕ$
31	29 30	syl	$⊢ φ \to G Fn ℕ$
32		dffn3	$⊢ G Fn ℕ \leftrightarrow G : ℕ ⟶ ran G$
33	31 32	sylib	$⊢ φ \to G : ℕ ⟶ ran G$
34		fco	$⊢ (H : ran G ⟶ S \land G : ℕ ⟶ ran G) \to (H \circ G) : ℕ ⟶ S$
35	26 33 34	syl2anc	$⊢ φ \to (H \circ G) : ℕ ⟶ S$
36		nnex	$⊢ ℕ \in V$
37	36	a1i	$⊢ φ \to ℕ \in V$
38	2 37	elmapd	$⊢ φ \to (H \circ G \in (S^{ℕ}) \leftrightarrow (H \circ G) : ℕ ⟶ S)$
39	35 38	mpbird	$⊢ φ \to H \circ G \in (S^{ℕ})$
40	4 39	eqeltrid	$⊢ φ \to E \in (S^{ℕ})$
41	33	ffvelrnda	$⊢ (φ \land n \in ℕ) \to G (n) \in ran G$
42	6	adantr	$⊢ (φ \land n \in ℕ) \to \forall y \in ran G H (y) \in y$
43		fveq2	$⊢ y = G (n) \to H (y) = H (G (n))$
44		id	$⊢ y = G (n) \to y = G (n)$
45	43 44	eleq12d	$⊢ y = G (n) \to (H (y) \in y \leftrightarrow H (G (n)) \in G (n))$
46	45	rspcva	$⊢ (G (n) \in ran G \land \forall y \in ran G H (y) \in y) \to H (G (n)) \in G (n)$
47	41 42 46	syl2anc	$⊢ (φ \land n \in ℕ) \to H (G (n)) \in G (n)$
48	33	ffund	$⊢ φ \to Fun G$
49	48	adantr	$⊢ (φ \land n \in ℕ) \to Fun G$
50		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
51	3	dmeqi	$⊢ dom G = dom (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
52	51	a1i	$⊢ φ \to dom G = dom (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
53		dmmptg	$⊢ \forall n \in ℕ \{x \in S \| F (n) = x \cap D\} \in V \to dom (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = ℕ$
54	29 53	syl	$⊢ φ \to dom (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\}) = ℕ$
55	52 54	eqtrd	$⊢ φ \to dom G = ℕ$
56	55	eqcomd	$⊢ φ \to ℕ = dom G$
57	56	adantr	$⊢ (φ \land n \in ℕ) \to ℕ = dom G$
58	50 57	eleqtrd	$⊢ (φ \land n \in ℕ) \to n \in dom G$
59	49 58 4	fvcod	$⊢ (φ \land n \in ℕ) \to E (n) = H (G (n))$
60	3	a1i	$⊢ φ \to G = (n \in ℕ ⟼ \{x \in S \| F (n) = x \cap D\})$
61	28	adantr	$⊢ (φ \land n \in ℕ) \to \{x \in S \| F (n) = x \cap D\} \in V$
62	60 61	fvmpt2d	$⊢ (φ \land n \in ℕ) \to G (n) = \{x \in S \| F (n) = x \cap D\}$
63	62	eqcomd	$⊢ (φ \land n \in ℕ) \to \{x \in S \| F (n) = x \cap D\} = G (n)$
64	59 63	eleq12d	$⊢ (φ \land n \in ℕ) \to (E (n) \in \{x \in S \| F (n) = x \cap D\} \leftrightarrow H (G (n)) \in G (n))$
65	47 64	mpbird	$⊢ (φ \land n \in ℕ) \to E (n) \in \{x \in S \| F (n) = x \cap D\}$
66		ineq1	$⊢ x = E (n) \to x \cap D = E (n) \cap D$
67	66	eqeq2d	$⊢ x = E (n) \to (F (n) = x \cap D \leftrightarrow F (n) = E (n) \cap D)$
68	67	elrab	$⊢ E (n) \in \{x \in S \| F (n) = x \cap D\} \leftrightarrow (E (n) \in S \land F (n) = E (n) \cap D)$
69	65 68	sylib	$⊢ (φ \land n \in ℕ) \to (E (n) \in S \land F (n) = E (n) \cap D)$
70	69	simprd	$⊢ (φ \land n \in ℕ) \to F (n) = E (n) \cap D$
71	70	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) = E (n) \cap D$
72		fveq1	$⊢ e = E \to e (n) = E (n)$
73	72	ineq1d	$⊢ e = E \to e (n) \cap D = E (n) \cap D$
74	73	eqeq2d	$⊢ e = E \to (F (n) = e (n) \cap D \leftrightarrow F (n) = E (n) \cap D)$
75	74	ralbidv	$⊢ e = E \to (\forall n \in ℕ F (n) = e (n) \cap D \leftrightarrow \forall n \in ℕ F (n) = E (n) \cap D)$
76	75	rspcev	$⊢ (E \in (S^{ℕ}) \land \forall n \in ℕ F (n) = E (n) \cap D) \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D$
77	40 71 76	syl2anc	$⊢ φ \to \exists e \in (S^{ℕ}) \forall n \in ℕ F (n) = e (n) \cap D$

Metamath Proof Explorer

Theorem subsaliuncllem

Proof