Theorem 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	⊢ Ⅎ 𝑦 𝜑
	subsaliuncllem.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	subsaliuncllem.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
	subsaliuncllem.e	⊢ 𝐸 = ( 𝐻 ∘ 𝐺 )
	subsaliuncllem.h	⊢ ( 𝜑 → 𝐻 Fn ran 𝐺 )
	subsaliuncllem.y	⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝐺 ( 𝐻 ‘ 𝑦 ) ∈ 𝑦 )
Assertion	subsaliuncllem	⊢ ( 𝜑 → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		subsaliuncllem.f	⊢ Ⅎ 𝑦 𝜑
2		subsaliuncllem.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3		subsaliuncllem.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
4		subsaliuncllem.e	⊢ 𝐸 = ( 𝐻 ∘ 𝐺 )
5		subsaliuncllem.h	⊢ ( 𝜑 → 𝐻 Fn ran 𝐺 )
6		subsaliuncllem.y	⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝐺 ( 𝐻 ‘ 𝑦 ) ∈ 𝑦 )
7		vex	⊢ 𝑦 ∈ V
8	3	elrnmpt	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
9	7 8	ax-mp	⊢ ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
10	9	biimpi	⊢ ( 𝑦 ∈ ran 𝐺 → ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
11		id	⊢ ( 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
12		ssrab2	⊢ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ⊆ 𝑆
13	12	a1i	⊢ ( 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ⊆ 𝑆 )
14	11 13	eqsstrd	⊢ ( 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ⊆ 𝑆 )
15	14	a1i	⊢ ( 𝑛 ∈ ℕ → ( 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ⊆ 𝑆 ) )
16	15	rexlimiv	⊢ ( ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ⊆ 𝑆 )
17	16	a1i	⊢ ( 𝑦 ∈ ran 𝐺 → ( ∃ 𝑛 ∈ ℕ 𝑦 = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } → 𝑦 ⊆ 𝑆 ) )
18	10 17	mpd	⊢ ( 𝑦 ∈ ran 𝐺 → 𝑦 ⊆ 𝑆 )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐺 ) → 𝑦 ⊆ 𝑆 )
20	6	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐺 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝑦 )
21	19 20	sseldd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐺 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝑆 )
22	21	ex	⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐺 → ( 𝐻 ‘ 𝑦 ) ∈ 𝑆 ) )
23	1 22	ralrimi	⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝐺 ( 𝐻 ‘ 𝑦 ) ∈ 𝑆 )
24	5 23	jca	⊢ ( 𝜑 → ( 𝐻 Fn ran 𝐺 ∧ ∀ 𝑦 ∈ ran 𝐺 ( 𝐻 ‘ 𝑦 ) ∈ 𝑆 ) )
25		ffnfv	⊢ ( 𝐻 : ran 𝐺 ⟶ 𝑆 ↔ ( 𝐻 Fn ran 𝐺 ∧ ∀ 𝑦 ∈ ran 𝐺 ( 𝐻 ‘ 𝑦 ) ∈ 𝑆 ) )
26	24 25	sylibr	⊢ ( 𝜑 → 𝐻 : ran 𝐺 ⟶ 𝑆 )
27		eqid	⊢ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) }
28	27 2	rabexd	⊢ ( 𝜑 → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ∈ V )
29	28	ralrimivw	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ∈ V )
30	3	fnmpt	⊢ ( ∀ 𝑛 ∈ ℕ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ∈ V → 𝐺 Fn ℕ )
31	29 30	syl	⊢ ( 𝜑 → 𝐺 Fn ℕ )
32		dffn3	⊢ ( 𝐺 Fn ℕ ↔ 𝐺 : ℕ ⟶ ran 𝐺 )
33	31 32	sylib	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ran 𝐺 )
34		fco	⊢ ( ( 𝐻 : ran 𝐺 ⟶ 𝑆 ∧ 𝐺 : ℕ ⟶ ran 𝐺 ) → ( 𝐻 ∘ 𝐺 ) : ℕ ⟶ 𝑆 )
35	26 33 34	syl2anc	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) : ℕ ⟶ 𝑆 )
36		nnex	⊢ ℕ ∈ V
37	36	a1i	⊢ ( 𝜑 → ℕ ∈ V )
38	2 37	elmapd	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐺 ) ∈ ( 𝑆 ↑m ℕ ) ↔ ( 𝐻 ∘ 𝐺 ) : ℕ ⟶ 𝑆 ) )
39	35 38	mpbird	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) ∈ ( 𝑆 ↑m ℕ ) )
40	4 39	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑆 ↑m ℕ ) )
41	33	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ran 𝐺 )
42	6	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑦 ∈ ran 𝐺 ( 𝐻 ‘ 𝑦 ) ∈ 𝑦 )
43		fveq2	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑛 ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑛 ) ) )
44		id	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑛 ) → 𝑦 = ( 𝐺 ‘ 𝑛 ) )
45	43 44	eleq12d	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑛 ) → ( ( 𝐻 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝐻 ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ( 𝐺 ‘ 𝑛 ) ) )
46	45	rspcva	⊢ ( ( ( 𝐺 ‘ 𝑛 ) ∈ ran 𝐺 ∧ ∀ 𝑦 ∈ ran 𝐺 ( 𝐻 ‘ 𝑦 ) ∈ 𝑦 ) → ( 𝐻 ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ( 𝐺 ‘ 𝑛 ) )
47	41 42 46	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐻 ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ( 𝐺 ‘ 𝑛 ) )
48	33	ffund	⊢ ( 𝜑 → Fun 𝐺 )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Fun 𝐺 )
50		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
51	3	dmeqi	⊢ dom 𝐺 = dom ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
52	51	a1i	⊢ ( 𝜑 → dom 𝐺 = dom ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
53		dmmptg	⊢ ( ∀ 𝑛 ∈ ℕ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ∈ V → dom ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) = ℕ )
54	29 53	syl	⊢ ( 𝜑 → dom ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) = ℕ )
55	52 54	eqtrd	⊢ ( 𝜑 → dom 𝐺 = ℕ )
56	55	eqcomd	⊢ ( 𝜑 → ℕ = dom 𝐺 )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ℕ = dom 𝐺 )
58	50 57	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ dom 𝐺 )
59	49 58 4	fvcod	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) = ( 𝐻 ‘ ( 𝐺 ‘ 𝑛 ) ) )
60	3	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ) )
61	28	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ∈ V )
62	60 61	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
63	62	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } = ( 𝐺 ‘ 𝑛 ) )
64	59 63	eleq12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ↔ ( 𝐻 ‘ ( 𝐺 ‘ 𝑛 ) ) ∈ ( 𝐺 ‘ 𝑛 ) ) )
65	47 64	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } )
66		ineq1	⊢ ( 𝑥 = ( 𝐸 ‘ 𝑛 ) → ( 𝑥 ∩ 𝐷 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) )
67	66	eqeq2d	⊢ ( 𝑥 = ( 𝐸 ‘ 𝑛 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) ↔ ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) ) )
68	67	elrab	⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ { 𝑥 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∩ 𝐷 ) } ↔ ( ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) ) )
69	65 68	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) ) )
70	69	simprd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) )
71	70	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) )
72		fveq1	⊢ ( 𝑒 = 𝐸 → ( 𝑒 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑛 ) )
73	72	ineq1d	⊢ ( 𝑒 = 𝐸 → ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) )
74	73	eqeq2d	⊢ ( 𝑒 = 𝐸 → ( ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ↔ ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) ) )
75	74	ralbidv	⊢ ( 𝑒 = 𝐸 → ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) ↔ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) ) )
76	75	rspcev	⊢ ( ( 𝐸 ∈ ( 𝑆 ↑m ℕ ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∩ 𝐷 ) ) → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )
77	40 71 76	syl2anc	⊢ ( 𝜑 → ∃ 𝑒 ∈ ( 𝑆 ↑m ℕ ) ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑒 ‘ 𝑛 ) ∩ 𝐷 ) )