1stmbfm - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 1stmbfm		Structured version Visualization version GIF version

Theorem 1stmbfm 34396

Description: The first projection map is measurable with regard to the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.)

**Hypotheses**
Ref	Expression
1stmbfm.1	⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
1stmbfm.2	⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)

**Assertion**
Ref	Expression
1stmbfm	⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆))

Proof of Theorem 1stmbfm Dummy variables 𝑧 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1stres 7957	. . . 4 ⊢ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆
2		1stmbfm.1	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
3		1stmbfm.2	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)
4		sxuni 34329	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
5	2, 3, 4	syl2anc 585	. . . . 5 ⊢ (𝜑 → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
6	5	feq2d 6645	. . . 4 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
7	1, 6	mpbii 233	. . 3 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆)
8		unielsiga 34264	. . . . 5 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆)
9	2, 8	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
10		sxsiga 34327	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
11	2, 3, 10	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
12		unielsiga 34264	. . . . 5 ⊢ ((𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
14	9, 13	elmapd 8779	. . 3 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
15	7, 14	mpbird 257	. 2 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)))
16		ffn 6661	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇))
17		elpreima 7003	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎)))
18	1, 16, 17	mp2b 10	. . . . . . 7 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎))
19		fvres 6852	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) = (1^st ‘𝑧))
20	19	eleq1d 2820	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ (1^st ‘𝑧) ∈ 𝑎))
21		1st2nd2 7972	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
22		xp2nd 7966	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (2^nd ‘𝑧) ∈ ∪ 𝑇)
23		elxp6 7967	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ ((1^st ‘𝑧) ∈ 𝑎 ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇)))
24		anass 468	. . . . . . . . . . . 12 ⊢ (((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (1^st ‘𝑧) ∈ 𝑎) ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ↔ (𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ ((1^st ‘𝑧) ∈ 𝑎 ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇)))
25		an32 647	. . . . . . . . . . . 12 ⊢ (((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (1^st ‘𝑧) ∈ 𝑎) ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ↔ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ∧ (1^st ‘𝑧) ∈ 𝑎))
26	23, 24, 25	3bitr2i 299	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ∧ (1^st ‘𝑧) ∈ 𝑎))
27	26	baib 535	. . . . . . . . . 10 ⊢ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1^st ‘𝑧) ∈ 𝑎))
28	21, 22, 27	syl2anc 585	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1^st ‘𝑧) ∈ 𝑎))
29	20, 28	bitr4d 282	. . . . . . . 8 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
30	29	pm5.32i 574	. . . . . . 7 ⊢ ((𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
31	18, 30	bitri 275	. . . . . 6 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
32		sgon 34260	. . . . . . . . . . 11 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆))
33		sigasspw 34252	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆) → 𝑆 ⊆ 𝒫 ∪ 𝑆)
34		pwssb 5055	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 ↔ ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
35	34	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
36	2, 32, 33, 35	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
37	36	r19.21bi 3227	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ ∪ 𝑆)
38		xpss1 5642	. . . . . . . . 9 ⊢ (𝑎 ⊆ ∪ 𝑆 → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
39	37, 38	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
40	39	sseld 3931	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) → 𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)))
41	40	pm4.71rd 562	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))))
42	31, 41	bitr4id 290	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
43	42	eqrdv 2733	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) = (𝑎 × ∪ 𝑇))
44	2	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
45	3	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑇 ∈ ∪ ran sigAlgebra)
46		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆)
47		eqid 2735	. . . . . . . 8 ⊢ ∪ 𝑇 = ∪ 𝑇
48		issgon 34259	. . . . . . . 8 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) ↔ (𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪ 𝑇))
49	3, 47, 48	sylanblrc 591	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (sigAlgebra‘∪ 𝑇))
50		baselsiga 34251	. . . . . . 7 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) → ∪ 𝑇 ∈ 𝑇)
51	49, 50	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑇)
52	51	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∪ 𝑇 ∈ 𝑇)
53		elsx 34330	. . . . 5 ⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) ∧ (𝑎 ∈ 𝑆 ∧ ∪ 𝑇 ∈ 𝑇)) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
54	44, 45, 46, 52, 53	syl22anc 839	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
55	43, 54	eqeltrd 2835	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
56	55	ralrimiva 3127	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
57	11, 2	ismbfm 34387	. 2 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆) ↔ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ∧ ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))))
58	15, 56, 57	mpbir2and 714	1 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3050 ⊆ wss 3900 𝒫 cpw 4553 ⟨cop 4585 ∪ cuni 4862 × cxp 5621 ^◡ccnv 5622 ran crn 5624 ↾ cres 5625 “ cima 5626 Fn wfn 6486 ⟶wf 6487 ‘cfv 6491 (class class class)co 7358 1^st c1st 7931 2^nd c2nd 7932 ↑_m cmap 8765 sigAlgebracsiga 34244 ×_s csx 34324 MblFnMcmbfm 34385

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2183 ax-ext 2707 ax-rep 5223 ax-sep 5240 ax-nul 5250 ax-pow 5309 ax-pr 5376 ax-un 7680

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-reu 3350 df-rab 3399 df-v 3441 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4285 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4902 df-iun 4947 df-br 5098 df-opab 5160 df-mpt 5179 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6447 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-ov 7361 df-oprab 7362 df-mpo 7363 df-1st 7933 df-2nd 7934 df-map 8767 df-siga 34245 df-sigagen 34275 df-sx 34325 df-mbfm 34386

This theorem is referenced by: (None)

W3C validator