# Metamath Proof Explorer

## Theorem 1stmbfm

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

Ref Expression
Hypotheses 1stmbfm.1 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
1stmbfm.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
Assertion 1stmbfm ${⊢}{\phi }\to {{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\in \left(\left({S}{×}_{s}{T}\right){\mathrm{MblFn}}_{\mu }{S}\right)$

### Proof

Step Hyp Ref Expression
1 1stmbfm.1 ${⊢}{\phi }\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
2 1stmbfm.2 ${⊢}{\phi }\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 f1stres ${⊢}\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right):\bigcup {S}×\bigcup {T}⟶\bigcup {S}$
4 sxuni ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to \bigcup {S}×\bigcup {T}=\bigcup \left({S}{×}_{s}{T}\right)$
5 1 2 4 syl2anc ${⊢}{\phi }\to \bigcup {S}×\bigcup {T}=\bigcup \left({S}{×}_{s}{T}\right)$
6 5 feq2d ${⊢}{\phi }\to \left(\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right):\bigcup {S}×\bigcup {T}⟶\bigcup {S}↔\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right):\bigcup \left({S}{×}_{s}{T}\right)⟶\bigcup {S}\right)$
7 3 6 mpbii ${⊢}{\phi }\to \left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right):\bigcup \left({S}{×}_{s}{T}\right)⟶\bigcup {S}$
8 unielsiga ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup {S}\in {S}$
9 1 8 syl ${⊢}{\phi }\to \bigcup {S}\in {S}$
10 sxsiga ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {S}{×}_{s}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
11 1 2 10 syl2anc ${⊢}{\phi }\to {S}{×}_{s}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
12 unielsiga ${⊢}{S}{×}_{s}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \bigcup \left({S}{×}_{s}{T}\right)\in \left({S}{×}_{s}{T}\right)$
13 11 12 syl ${⊢}{\phi }\to \bigcup \left({S}{×}_{s}{T}\right)\in \left({S}{×}_{s}{T}\right)$
14 9 13 elmapd ${⊢}{\phi }\to \left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\in \left({\bigcup {S}}^{\bigcup \left({S}{×}_{s}{T}\right)}\right)↔\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right):\bigcup \left({S}{×}_{s}{T}\right)⟶\bigcup {S}\right)$
15 7 14 mpbird ${⊢}{\phi }\to {{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\in \left({\bigcup {S}}^{\bigcup \left({S}{×}_{s}{T}\right)}\right)$
16 sgon ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to {S}\in \mathrm{sigAlgebra}\left(\bigcup {S}\right)$
17 sigasspw ${⊢}{S}\in \mathrm{sigAlgebra}\left(\bigcup {S}\right)\to {S}\subseteq 𝒫\bigcup {S}$
18 pwssb ${⊢}{S}\subseteq 𝒫\bigcup {S}↔\forall {a}\in {S}\phantom{\rule{.4em}{0ex}}{a}\subseteq \bigcup {S}$
19 18 biimpi ${⊢}{S}\subseteq 𝒫\bigcup {S}\to \forall {a}\in {S}\phantom{\rule{.4em}{0ex}}{a}\subseteq \bigcup {S}$
20 1 16 17 19 4syl ${⊢}{\phi }\to \forall {a}\in {S}\phantom{\rule{.4em}{0ex}}{a}\subseteq \bigcup {S}$
21 20 r19.21bi ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to {a}\subseteq \bigcup {S}$
22 xpss1 ${⊢}{a}\subseteq \bigcup {S}\to {a}×\bigcup {T}\subseteq \bigcup {S}×\bigcup {T}$
23 21 22 syl ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to {a}×\bigcup {T}\subseteq \bigcup {S}×\bigcup {T}$
24 23 sseld ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to \left({z}\in \left({a}×\bigcup {T}\right)\to {z}\in \left(\bigcup {S}×\bigcup {T}\right)\right)$
25 24 pm4.71rd ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to \left({z}\in \left({a}×\bigcup {T}\right)↔\left({z}\in \left(\bigcup {S}×\bigcup {T}\right)\wedge {z}\in \left({a}×\bigcup {T}\right)\right)\right)$
26 ffn ${⊢}\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right):\bigcup {S}×\bigcup {T}⟶\bigcup {S}\to \left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)Fn\left(\bigcup {S}×\bigcup {T}\right)$
27 elpreima ${⊢}\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)Fn\left(\bigcup {S}×\bigcup {T}\right)\to \left({z}\in {\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)}^{-1}\left[{a}\right]↔\left({z}\in \left(\bigcup {S}×\bigcup {T}\right)\wedge \left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)\left({z}\right)\in {a}\right)\right)$
28 3 26 27 mp2b ${⊢}{z}\in {\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)}^{-1}\left[{a}\right]↔\left({z}\in \left(\bigcup {S}×\bigcup {T}\right)\wedge \left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)\left({z}\right)\in {a}\right)$
29 fvres ${⊢}{z}\in \left(\bigcup {S}×\bigcup {T}\right)\to \left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)\left({z}\right)={1}^{st}\left({z}\right)$
30 29 eleq1d ${⊢}{z}\in \left(\bigcup {S}×\bigcup {T}\right)\to \left(\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)\left({z}\right)\in {a}↔{1}^{st}\left({z}\right)\in {a}\right)$
31 1st2nd2 ${⊢}{z}\in \left(\bigcup {S}×\bigcup {T}\right)\to {z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩$
32 xp2nd ${⊢}{z}\in \left(\bigcup {S}×\bigcup {T}\right)\to {2}^{nd}\left({z}\right)\in \bigcup {T}$
33 elxp6 ${⊢}{z}\in \left({a}×\bigcup {T}\right)↔\left({z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\wedge \left({1}^{st}\left({z}\right)\in {a}\wedge {2}^{nd}\left({z}\right)\in \bigcup {T}\right)\right)$
34 anass ${⊢}\left(\left({z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\wedge {1}^{st}\left({z}\right)\in {a}\right)\wedge {2}^{nd}\left({z}\right)\in \bigcup {T}\right)↔\left({z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\wedge \left({1}^{st}\left({z}\right)\in {a}\wedge {2}^{nd}\left({z}\right)\in \bigcup {T}\right)\right)$
35 an32 ${⊢}\left(\left({z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\wedge {1}^{st}\left({z}\right)\in {a}\right)\wedge {2}^{nd}\left({z}\right)\in \bigcup {T}\right)↔\left(\left({z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\wedge {2}^{nd}\left({z}\right)\in \bigcup {T}\right)\wedge {1}^{st}\left({z}\right)\in {a}\right)$
36 33 34 35 3bitr2i ${⊢}{z}\in \left({a}×\bigcup {T}\right)↔\left(\left({z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\wedge {2}^{nd}\left({z}\right)\in \bigcup {T}\right)\wedge {1}^{st}\left({z}\right)\in {a}\right)$
37 36 baib ${⊢}\left({z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\wedge {2}^{nd}\left({z}\right)\in \bigcup {T}\right)\to \left({z}\in \left({a}×\bigcup {T}\right)↔{1}^{st}\left({z}\right)\in {a}\right)$
38 31 32 37 syl2anc ${⊢}{z}\in \left(\bigcup {S}×\bigcup {T}\right)\to \left({z}\in \left({a}×\bigcup {T}\right)↔{1}^{st}\left({z}\right)\in {a}\right)$
39 30 38 bitr4d ${⊢}{z}\in \left(\bigcup {S}×\bigcup {T}\right)\to \left(\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)\left({z}\right)\in {a}↔{z}\in \left({a}×\bigcup {T}\right)\right)$
40 39 pm5.32i ${⊢}\left({z}\in \left(\bigcup {S}×\bigcup {T}\right)\wedge \left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)\left({z}\right)\in {a}\right)↔\left({z}\in \left(\bigcup {S}×\bigcup {T}\right)\wedge {z}\in \left({a}×\bigcup {T}\right)\right)$
41 28 40 bitri ${⊢}{z}\in {\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)}^{-1}\left[{a}\right]↔\left({z}\in \left(\bigcup {S}×\bigcup {T}\right)\wedge {z}\in \left({a}×\bigcup {T}\right)\right)$
42 25 41 syl6rbbr ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to \left({z}\in {\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)}^{-1}\left[{a}\right]↔{z}\in \left({a}×\bigcup {T}\right)\right)$
43 42 eqrdv ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to {\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)}^{-1}\left[{a}\right]={a}×\bigcup {T}$
44 1 adantr ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
45 2 adantr ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
46 simpr ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to {a}\in {S}$
47 eqid ${⊢}\bigcup {T}=\bigcup {T}$
48 issgon ${⊢}{T}\in \mathrm{sigAlgebra}\left(\bigcup {T}\right)↔\left({T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup {T}=\bigcup {T}\right)$
49 2 47 48 sylanblrc ${⊢}{\phi }\to {T}\in \mathrm{sigAlgebra}\left(\bigcup {T}\right)$
50 baselsiga ${⊢}{T}\in \mathrm{sigAlgebra}\left(\bigcup {T}\right)\to \bigcup {T}\in {T}$
51 49 50 syl ${⊢}{\phi }\to \bigcup {T}\in {T}$
52 51 adantr ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to \bigcup {T}\in {T}$
53 elsx ${⊢}\left(\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\wedge \left({a}\in {S}\wedge \bigcup {T}\in {T}\right)\right)\to {a}×\bigcup {T}\in \left({S}{×}_{s}{T}\right)$
54 44 45 46 52 53 syl22anc ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to {a}×\bigcup {T}\in \left({S}{×}_{s}{T}\right)$
55 43 54 eqeltrd ${⊢}\left({\phi }\wedge {a}\in {S}\right)\to {\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)}^{-1}\left[{a}\right]\in \left({S}{×}_{s}{T}\right)$
56 55 ralrimiva ${⊢}{\phi }\to \forall {a}\in {S}\phantom{\rule{.4em}{0ex}}{\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)}^{-1}\left[{a}\right]\in \left({S}{×}_{s}{T}\right)$
57 11 1 ismbfm ${⊢}{\phi }\to \left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\in \left(\left({S}{×}_{s}{T}\right){\mathrm{MblFn}}_{\mu }{S}\right)↔\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\in \left({\bigcup {S}}^{\bigcup \left({S}{×}_{s}{T}\right)}\right)\wedge \forall {a}\in {S}\phantom{\rule{.4em}{0ex}}{\left({{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\right)}^{-1}\left[{a}\right]\in \left({S}{×}_{s}{T}\right)\right)\right)$
58 15 56 57 mpbir2and ${⊢}{\phi }\to {{1}^{st}↾}_{\left(\bigcup {S}×\bigcup {T}\right)}\in \left(\left({S}{×}_{s}{T}\right){\mathrm{MblFn}}_{\mu }{S}\right)$