smfpimcc

Description: Given a countable set of sigma-measurable functions, and a Borel set A there exists a choice function h that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of A . This is a generalization of the observation at the beginning of the proof of Proposition 121F of Fremlin1 p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smfpimcc.1	$⊢ \underline{Ⅎ} n F$
	smfpimcc.z	$⊢ Z = ℤ_{\geq M}$
	smfpimcc.s	$⊢ φ \to S \in SAlg$
	smfpimcc.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smfpimcc.j	$⊢ J = topGen (ran (.))$
	smfpimcc.b	$⊢ B = SalGen (J)$
	smfpimcc.a	$⊢ φ \to A \in B$
Assertion	smfpimcc	$⊢ φ \to \exists h (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n))$

Proof

Step	Hyp	Ref	Expression
1		smfpimcc.1	$⊢ \underline{Ⅎ} n F$
2		smfpimcc.z	$⊢ Z = ℤ_{\geq M}$
3		smfpimcc.s	$⊢ φ \to S \in SAlg$
4		smfpimcc.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smfpimcc.j	$⊢ J = topGen (ran (.))$
6		smfpimcc.b	$⊢ B = SalGen (J)$
7		smfpimcc.a	$⊢ φ \to A \in B$
8	2	uzct	$⊢ Z ≼ ω$
9	8	a1i	$⊢ φ \to Z ≼ ω$
10		mptct	$⊢ Z ≼ ω \to (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) ≼ ω$
11		rnct	$⊢ (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) ≼ ω \to ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) ≼ ω$
12	9 10 11	3syl	$⊢ φ \to ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) ≼ ω$
13		vex	$⊢ y \in V$
14		eqid	$⊢ (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) = (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})$
15	14	elrnmpt	$⊢ y \in V \to (y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) \leftrightarrow \exists m \in Z y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})$
16	13 15	ax-mp	$⊢ y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) \leftrightarrow \exists m \in Z y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}$
17	16	biimpi	$⊢ y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) \to \exists m \in Z y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}$
18	17	adantl	$⊢ (φ \land y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})) \to \exists m \in Z y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}$
19		simp3	$⊢ (φ \land m \in Z \land y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) \to y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}$
20	3	adantr	$⊢ (φ \land m \in Z) \to S \in SAlg$
21	4	ffvelcdmda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
22		eqid	$⊢ dom F (m) = dom F (m)$
23	7	adantr	$⊢ (φ \land m \in Z) \to A \in B$
24		eqid	$⊢ {F (m)}^{-1} [A] = {F (m)}^{-1} [A]$
25	20 21 22 5 6 23 24	smfpimbor1	$⊢ (φ \land m \in Z) \to {F (m)}^{-1} [A] \in (S ↾_{𝑡} dom F (m))$
26		fvex	$⊢ F (m) \in V$
27	26	dmex	$⊢ dom F (m) \in V$
28	27	a1i	$⊢ φ \to dom F (m) \in V$
29		elrest	$⊢ (S \in SAlg \land dom F (m) \in V) \to ({F (m)}^{-1} [A] \in (S ↾_{𝑡} dom F (m)) \leftrightarrow \exists s \in S {F (m)}^{-1} [A] = s \cap dom F (m))$
30	3 28 29	syl2anc	$⊢ φ \to ({F (m)}^{-1} [A] \in (S ↾_{𝑡} dom F (m)) \leftrightarrow \exists s \in S {F (m)}^{-1} [A] = s \cap dom F (m))$
31	30	adantr	$⊢ (φ \land m \in Z) \to ({F (m)}^{-1} [A] \in (S ↾_{𝑡} dom F (m)) \leftrightarrow \exists s \in S {F (m)}^{-1} [A] = s \cap dom F (m))$
32	25 31	mpbid	$⊢ (φ \land m \in Z) \to \exists s \in S {F (m)}^{-1} [A] = s \cap dom F (m)$
33		rabn0	$⊢ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\} \neq \emptyset \leftrightarrow \exists s \in S {F (m)}^{-1} [A] = s \cap dom F (m)$
34	32 33	sylibr	$⊢ (φ \land m \in Z) \to \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\} \neq \emptyset$
35	34	3adant3	$⊢ (φ \land m \in Z \land y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) \to \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\} \neq \emptyset$
36	19 35	eqnetrd	$⊢ (φ \land m \in Z \land y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) \to y \neq \emptyset$
37	36	3exp	$⊢ φ \to (m \in Z \to (y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\} \to y \neq \emptyset))$
38	37	rexlimdv	$⊢ φ \to (\exists m \in Z y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\} \to y \neq \emptyset)$
39	38	adantr	$⊢ (φ \land y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})) \to (\exists m \in Z y = \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\} \to y \neq \emptyset)$
40	18 39	mpd	$⊢ (φ \land y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})) \to y \neq \emptyset$
41	12 40	axccd2	$⊢ φ \to \exists f \forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y$
42		nfv	$⊢ Ⅎ m φ$
43		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})$
44	43	nfrn	$⊢ \underline{Ⅎ} m ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})$
45		nfv	$⊢ Ⅎ m f (y) \in y$
46	44 45	nfralw	$⊢ Ⅎ m \forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y$
47	42 46	nfan	$⊢ Ⅎ m (φ \land \forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y)$
48	2	fvexi	$⊢ Z \in V$
49	3	adantr	$⊢ (φ \land \forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y) \to S \in SAlg$
50		fveq2	$⊢ y = w \to f (y) = f (w)$
51		id	$⊢ y = w \to y = w$
52	50 51	eleq12d	$⊢ y = w \to (f (y) \in y \leftrightarrow f (w) \in w)$
53	52	rspccva	$⊢ (\forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y \land w \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})) \to f (w) \in w$
54	53	adantll	$⊢ ((φ \land \forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y) \land w \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})) \to f (w) \in w$
55		eqid	$⊢ (m \in Z ⟼ f (\{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\})) = (m \in Z ⟼ f (\{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}))$
56	47 48 49 54 55	smfpimcclem	$⊢ (φ \land \forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y) \to \exists h (h : Z ⟶ S \land \forall m \in Z {F (m)}^{-1} [A] = h (m) \cap dom F (m))$
57	56	ex	$⊢ φ \to (\forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y \to \exists h (h : Z ⟶ S \land \forall m \in Z {F (m)}^{-1} [A] = h (m) \cap dom F (m)))$
58	57	exlimdv	$⊢ φ \to (\exists f \forall y \in ran (m \in Z ⟼ \{s \in S \| {F (m)}^{-1} [A] = s \cap dom F (m)\}) f (y) \in y \to \exists h (h : Z ⟶ S \land \forall m \in Z {F (m)}^{-1} [A] = h (m) \cap dom F (m)))$
59	41 58	mpd	$⊢ φ \to \exists h (h : Z ⟶ S \land \forall m \in Z {F (m)}^{-1} [A] = h (m) \cap dom F (m))$
60		nfcv	$⊢ \underline{Ⅎ} n m$
61	1 60	nffv	$⊢ \underline{Ⅎ} n F (m)$
62	61	nfcnv	$⊢ \underline{Ⅎ} n {F (m)}^{-1}$
63		nfcv	$⊢ \underline{Ⅎ} n A$
64	62 63	nfima	$⊢ \underline{Ⅎ} n {F (m)}^{-1} [A]$
65		nfcv	$⊢ \underline{Ⅎ} n h (m)$
66	61	nfdm	$⊢ \underline{Ⅎ} n dom F (m)$
67	65 66	nfin	$⊢ \underline{Ⅎ} n (h (m) \cap dom F (m))$
68	64 67	nfeq	$⊢ Ⅎ n {F (m)}^{-1} [A] = h (m) \cap dom F (m)$
69		nfv	$⊢ Ⅎ m {F (n)}^{-1} [A] = h (n) \cap dom F (n)$
70		fveq2	$⊢ m = n \to F (m) = F (n)$
71	70	cnveqd	$⊢ m = n \to {F (m)}^{-1} = {F (n)}^{-1}$
72	71	imaeq1d	$⊢ m = n \to {F (m)}^{-1} [A] = {F (n)}^{-1} [A]$
73		fveq2	$⊢ m = n \to h (m) = h (n)$
74	70	dmeqd	$⊢ m = n \to dom F (m) = dom F (n)$
75	73 74	ineq12d	$⊢ m = n \to h (m) \cap dom F (m) = h (n) \cap dom F (n)$
76	72 75	eqeq12d	$⊢ m = n \to ({F (m)}^{-1} [A] = h (m) \cap dom F (m) \leftrightarrow {F (n)}^{-1} [A] = h (n) \cap dom F (n))$
77	68 69 76	cbvralw	$⊢ \forall m \in Z {F (m)}^{-1} [A] = h (m) \cap dom F (m) \leftrightarrow \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n)$
78	77	anbi2i	$⊢ (h : Z ⟶ S \land \forall m \in Z {F (m)}^{-1} [A] = h (m) \cap dom F (m)) \leftrightarrow (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n))$
79	78	exbii	$⊢ \exists h (h : Z ⟶ S \land \forall m \in Z {F (m)}^{-1} [A] = h (m) \cap dom F (m)) \leftrightarrow \exists h (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n))$
80	59 79	sylib	$⊢ φ \to \exists h (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n))$

Metamath Proof Explorer

Theorem smfpimcc

Proof