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 34262

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 8038	. . . 4 ⊢ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆
2		1stmbfm.1	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
3		1stmbfm.2	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)
4		sxuni 34194	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
5	2, 3, 4	syl2anc 584	. . . . 5 ⊢ (𝜑 → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
6	5	feq2d 6722	. . . 4 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
7	1, 6	mpbii 233	. . 3 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆)
8		unielsiga 34129	. . . . 5 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆)
9	2, 8	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
10		sxsiga 34192	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
11	2, 3, 10	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
12		unielsiga 34129	. . . . 5 ⊢ ((𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
14	9, 13	elmapd 8880	. . 3 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
15	7, 14	mpbird 257	. 2 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)))
16		ffn 6736	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇))
17		elpreima 7078	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎)))
18	1, 16, 17	mp2b 10	. . . . . . 7 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎))
19		fvres 6925	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) = (1^st ‘𝑧))
20	19	eleq1d 2826	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ (1^st ‘𝑧) ∈ 𝑎))
21		1st2nd2 8053	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
22		xp2nd 8047	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (2^nd ‘𝑧) ∈ ∪ 𝑇)
23		elxp6 8048	. . . . . . . . . . . 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 646	. . . . . . . . . . . 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 584	. . . . . . . . 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 34125	. . . . . . . . . . 11 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆))
33		sigasspw 34117	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆) → 𝑆 ⊆ 𝒫 ∪ 𝑆)
34		pwssb 5101	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 ↔ ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
35	34	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
36	2, 32, 33, 35	4syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
37	36	r19.21bi 3251	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ ∪ 𝑆)
38		xpss1 5704	. . . . . . . . 9 ⊢ (𝑎 ⊆ ∪ 𝑆 → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
39	37, 38	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
40	39	sseld 3982	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) → 𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)))
41	40	pm4.71rd 562	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))))
42	31, 41	bitr4id 290	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
43	42	eqrdv 2735	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) = (𝑎 × ∪ 𝑇))
44	2	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
45	3	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑇 ∈ ∪ ran sigAlgebra)
46		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆)
47		eqid 2737	. . . . . . . 8 ⊢ ∪ 𝑇 = ∪ 𝑇
48		issgon 34124	. . . . . . . 8 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) ↔ (𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪ 𝑇))
49	3, 47, 48	sylanblrc 590	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (sigAlgebra‘∪ 𝑇))
50		baselsiga 34116	. . . . . . 7 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) → ∪ 𝑇 ∈ 𝑇)
51	49, 50	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑇)
52	51	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∪ 𝑇 ∈ 𝑇)
53		elsx 34195	. . . . 5 ⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) ∧ (𝑎 ∈ 𝑆 ∧ ∪ 𝑇 ∈ 𝑇)) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
54	44, 45, 46, 52, 53	syl22anc 839	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
55	43, 54	eqeltrd 2841	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
56	55	ralrimiva 3146	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
57	11, 2	ismbfm 34252	. 2 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆) ↔ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ∧ ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))))
58	15, 56, 57	mpbir2and 713	1 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ⊆ wss 3951 𝒫 cpw 4600 ⟨cop 4632 ∪ cuni 4907 × cxp 5683 ^◡ccnv 5684 ran crn 5686 ↾ cres 5687 “ cima 5688 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 1^st c1st 8012 2^nd c2nd 8013 ↑_m cmap 8866 sigAlgebracsiga 34109 ×_s csx 34189 MblFnMcmbfm 34250

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-1st 8014 df-2nd 8015 df-map 8868 df-siga 34110 df-sigagen 34140 df-sx 34190 df-mbfm 34251

This theorem is referenced by: (None)

W3C validator