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 34959

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 8046	. . . 4 ⊢ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆
2		1stmbfm.1	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
3		1stmbfm.2	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)
4		sxuni 34893	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
5	2, 3, 4	syl2anc 596	. . . . 5 ⊢ (𝜑 → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×_s 𝑇))
6	5	feq2d 6712	. . . 4 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
7	1, 6	mpbii 236	. . 3 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆)
8		unielsiga 34827	. . . . 5 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆)
9	2, 8	syl 18	. . . 4 ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
10		sxsiga 34891	. . . . . 6 ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
11	2, 3, 10	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra)
12		unielsiga 34827	. . . . 5 ⊢ ((𝑆 ×_s 𝑇) ∈ ∪ ran sigAlgebra → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
13	11, 12	syl 18	. . . 4 ⊢ (𝜑 → ∪ (𝑆 ×_s 𝑇) ∈ (𝑆 ×_s 𝑇))
14	9, 13	elmapd 8885	. . 3 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ↔ (1^st ↾ (∪ 𝑆 × ∪ 𝑇)):∪ (𝑆 ×_s 𝑇)⟶∪ 𝑆))
15	7, 14	mpbird 260	. 2 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)))
16		ffn 6728	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪ 𝑆 × ∪ 𝑇)⟶∪ 𝑆 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇))
17		elpreima 7077	. . . . . . . 8 ⊢ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎)))
18	1, 16, 17	mp2b 10	. . . . . . 7 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎))
19		fvres 6924	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) = (1^st ‘𝑧))
20	19	eleq1d 2849	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ (1^st ‘𝑧) ∈ 𝑎))
21		1st2nd2 8061	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
22		xp2nd 8055	. . . . . . . . . 10 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (2^nd ‘𝑧) ∈ ∪ 𝑇)
23		elxp6 8056	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ ((1^st ‘𝑧) ∈ 𝑎 ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇)))
24		anass 474	. . . . . . . . . . . 12 ⊢ (((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (1^st ‘𝑧) ∈ 𝑎) ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ↔ (𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ ((1^st ‘𝑧) ∈ 𝑎 ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇)))
25		an32 659	. . . . . . . . . . . 12 ⊢ (((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (1^st ‘𝑧) ∈ 𝑎) ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ↔ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ∧ (1^st ‘𝑧) ∈ 𝑎))
26	23, 24, 25	3bitr2i 302	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) ∧ (1^st ‘𝑧) ∈ 𝑎))
27	26	baib 545	. . . . . . . . . 10 ⊢ ((𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∧ (2^nd ‘𝑧) ∈ ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1^st ‘𝑧) ∈ 𝑎))
28	21, 22, 27	syl2anc 596	. . . . . . . . 9 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1^st ‘𝑧) ∈ 𝑎))
29	20, 28	bitr4d 285	. . . . . . . 8 ⊢ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) → (((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
30	29	pm5.32i 585	. . . . . . 7 ⊢ ((𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
31	18, 30	bitri 278	. . . . . 6 ⊢ (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
32		sgon 34823	. . . . . . . . . . 11 ⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆))
33		sigasspw 34815	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆) → 𝑆 ⊆ 𝒫 ∪ 𝑆)
34		pwssb 5064	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 ↔ ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
35	34	biimpi 219	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
36	2, 32, 33, 35	4syl 20	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆)
37	36	r19.21bi 3258	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ ∪ 𝑆)
38		xpss1 5674	. . . . . . . . 9 ⊢ (𝑎 ⊆ ∪ 𝑆 → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
39	37, 38	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆 × ∪ 𝑇))
40	39	sseld 3912	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) → 𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)))
41	40	pm4.71rd 572	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇) ∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))))
42	31, 41	bitr4id 293	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇)))
43	42	eqrdv 2761	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) = (𝑎 × ∪ 𝑇))
44	2	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
45	3	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑇 ∈ ∪ ran sigAlgebra)
46		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆)
47		eqid 2763	. . . . . . . 8 ⊢ ∪ 𝑇 = ∪ 𝑇
48		issgon 34822	. . . . . . . 8 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) ↔ (𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪ 𝑇))
49	3, 47, 48	sylanblrc 602	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (sigAlgebra‘∪ 𝑇))
50		baselsiga 34814	. . . . . . 7 ⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇) → ∪ 𝑇 ∈ 𝑇)
51	49, 50	syl 18	. . . . . 6 ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑇)
52	51	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∪ 𝑇 ∈ 𝑇)
53		elsx 34894	. . . . 5 ⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) ∧ (𝑎 ∈ 𝑆 ∧ ∪ 𝑇 ∈ 𝑇)) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
54	44, 45, 46, 52, 53	syl22anc 852	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×_s 𝑇))
55	43, 54	eqeltrd 2864	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
56	55	ralrimiva 3158	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))
57	11, 2	ismbfm 34951	. 2 ⊢ (𝜑 → ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆) ↔ ((1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆 ↑_m ∪ (𝑆 ×_s 𝑇)) ∧ ∀𝑎 ∈ 𝑆 (^◡(1^st ↾ (∪ 𝑆 × ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×_s 𝑇))))
58	15, 56, 57	mpbir2and 726	1 ⊢ (𝜑 → (1^st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×_s 𝑇)MblFnM𝑆))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 ⊆ wss 3900 𝒫 cpw 4560 ⟨cop 4838 ∪ cuni 4870 × cxp 5653 ^◡ccnv 5654 ran crn 5656 ↾ cres 5657 “ cima 5658 Fn wfn 6550 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 1^st c1st 8020 2^nd c2nd 8021 ↑_m cmap 8872 sigAlgebracsiga 34807 ×_s csx 34888 MblFnMcmbfm 34949

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-ov 7443 df-oprab 7444 df-mpo 7445 df-1st 8022 df-2nd 8023 df-map 8874 df-siga 34808 df-sigagen 34839 df-sx 34889 df-mbfm 34950

This theorem is used by: (None)

W3C validator