Metamath Proof Explorer


Theorem imambfm

Description: If the sigma-algebra in the range of a given function is generated by a collection of basic sets K , then to check the measurability of that function, we need only consider inverse images of basic sets a . (Contributed by Thierry Arnoux, 4-Jun-2017)

Ref Expression
Hypotheses imambfm.1 φ K V
imambfm.2 φ S ran sigAlgebra
imambfm.3 φ T = 𝛔 K
Assertion imambfm φ F S MblFn μ T F : S T a K F -1 a S

Proof

Step Hyp Ref Expression
1 imambfm.1 φ K V
2 imambfm.2 φ S ran sigAlgebra
3 imambfm.3 φ T = 𝛔 K
4 2 adantr φ F S MblFn μ T S ran sigAlgebra
5 1 sgsiga φ 𝛔 K ran sigAlgebra
6 3 5 eqeltrd φ T ran sigAlgebra
7 6 adantr φ F S MblFn μ T T ran sigAlgebra
8 simpr φ F S MblFn μ T F S MblFn μ T
9 4 7 8 mbfmf φ F S MblFn μ T F : S T
10 2 ad2antrr φ F S MblFn μ T a K S ran sigAlgebra
11 6 ad2antrr φ F S MblFn μ T a K T ran sigAlgebra
12 simplr φ F S MblFn μ T a K F S MblFn μ T
13 sssigagen K V K 𝛔 K
14 1 13 syl φ K 𝛔 K
15 14 3 sseqtrrd φ K T
16 15 ad2antrr φ F S MblFn μ T a K K T
17 simpr φ F S MblFn μ T a K a K
18 16 17 sseldd φ F S MblFn μ T a K a T
19 10 11 12 18 mbfmcnvima φ F S MblFn μ T a K F -1 a S
20 19 ralrimiva φ F S MblFn μ T a K F -1 a S
21 9 20 jca φ F S MblFn μ T F : S T a K F -1 a S
22 unielsiga T ran sigAlgebra T T
23 6 22 syl φ T T
24 23 adantr φ F : S T a K F -1 a S T T
25 unielsiga S ran sigAlgebra S S
26 2 25 syl φ S S
27 26 adantr φ F : S T a K F -1 a S S S
28 simprl φ F : S T a K F -1 a S F : S T
29 elmapg T T S S F T S F : S T
30 29 biimpar T T S S F : S T F T S
31 24 27 28 30 syl21anc φ F : S T a K F -1 a S F T S
32 3 adantr φ F : S T a K F -1 a S T = 𝛔 K
33 simpl φ F : S T a K F -1 a S φ
34 ssrab2 a T | F -1 a S T
35 pwuni T 𝒫 T
36 34 35 sstri a T | F -1 a S 𝒫 T
37 36 a1i φ F : S T a K F -1 a S a T | F -1 a S 𝒫 T
38 fimacnv F : S T F -1 T = S
39 38 ad2antrl φ F : S T a K F -1 a S F -1 T = S
40 39 27 eqeltrd φ F : S T a K F -1 a S F -1 T S
41 imaeq2 a = T F -1 a = F -1 T
42 41 eleq1d a = T F -1 a S F -1 T S
43 42 elrab T a T | F -1 a S T T F -1 T S
44 24 40 43 sylanbrc φ F : S T a K F -1 a S T a T | F -1 a S
45 6 ad2antrr φ F : S T a K F -1 a S x a T | F -1 a S T ran sigAlgebra
46 45 22 syl φ F : S T a K F -1 a S x a T | F -1 a S T T
47 elrabi x a T | F -1 a S x T
48 47 adantl φ F : S T a K F -1 a S x a T | F -1 a S x T
49 difelsiga T ran sigAlgebra T T x T T x T
50 45 46 48 49 syl3anc φ F : S T a K F -1 a S x a T | F -1 a S T x T
51 simplrl φ F : S T a K F -1 a S x a T | F -1 a S F : S T
52 ffun F : S T Fun F
53 difpreima Fun F F -1 T x = F -1 T F -1 x
54 51 52 53 3syl φ F : S T a K F -1 a S x a T | F -1 a S F -1 T x = F -1 T F -1 x
55 39 difeq1d φ F : S T a K F -1 a S F -1 T F -1 x = S F -1 x
56 55 adantr φ F : S T a K F -1 a S x a T | F -1 a S F -1 T F -1 x = S F -1 x
57 2 ad2antrr φ F : S T a K F -1 a S x a T | F -1 a S S ran sigAlgebra
58 57 25 syl φ F : S T a K F -1 a S x a T | F -1 a S S S
59 imaeq2 a = x F -1 a = F -1 x
60 59 eleq1d a = x F -1 a S F -1 x S
61 60 elrab x a T | F -1 a S x T F -1 x S
62 61 simprbi x a T | F -1 a S F -1 x S
63 62 adantl φ F : S T a K F -1 a S x a T | F -1 a S F -1 x S
64 difelsiga S ran sigAlgebra S S F -1 x S S F -1 x S
65 57 58 63 64 syl3anc φ F : S T a K F -1 a S x a T | F -1 a S S F -1 x S
66 56 65 eqeltrd φ F : S T a K F -1 a S x a T | F -1 a S F -1 T F -1 x S
67 54 66 eqeltrd φ F : S T a K F -1 a S x a T | F -1 a S F -1 T x S
68 imaeq2 a = T x F -1 a = F -1 T x
69 68 eleq1d a = T x F -1 a S F -1 T x S
70 69 elrab T x a T | F -1 a S T x T F -1 T x S
71 50 67 70 sylanbrc φ F : S T a K F -1 a S x a T | F -1 a S T x a T | F -1 a S
72 71 ralrimiva φ F : S T a K F -1 a S x a T | F -1 a S T x a T | F -1 a S
73 6 ad3antrrr φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω T ran sigAlgebra
74 sspwb a T | F -1 a S T 𝒫 a T | F -1 a S 𝒫 T
75 34 74 mpbi 𝒫 a T | F -1 a S 𝒫 T
76 75 sseli x 𝒫 a T | F -1 a S x 𝒫 T
77 76 ad2antlr φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω x 𝒫 T
78 simpr φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω x ω
79 sigaclcu T ran sigAlgebra x 𝒫 T x ω x T
80 73 77 78 79 syl3anc φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω x T
81 simpllr φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω F : S T a K F -1 a S
82 81 simpld φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω F : S T
83 unipreima Fun F F -1 x = y x F -1 y
84 82 52 83 3syl φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω F -1 x = y x F -1 y
85 2 ad3antrrr φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω S ran sigAlgebra
86 simpr φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω y x y x
87 simpllr φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω y x x 𝒫 a T | F -1 a S
88 elelpwi y x x 𝒫 a T | F -1 a S y a T | F -1 a S
89 86 87 88 syl2anc φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω y x y a T | F -1 a S
90 imaeq2 a = y F -1 a = F -1 y
91 90 eleq1d a = y F -1 a S F -1 y S
92 91 elrab y a T | F -1 a S y T F -1 y S
93 92 simprbi y a T | F -1 a S F -1 y S
94 89 93 syl φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω y x F -1 y S
95 94 ralrimiva φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω y x F -1 y S
96 nfcv _ y x
97 96 sigaclcuni S ran sigAlgebra y x F -1 y S x ω y x F -1 y S
98 85 95 78 97 syl3anc φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω y x F -1 y S
99 84 98 eqeltrd φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω F -1 x S
100 imaeq2 a = x F -1 a = F -1 x
101 100 eleq1d a = x F -1 a S F -1 x S
102 101 elrab x a T | F -1 a S x T F -1 x S
103 80 99 102 sylanbrc φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω x a T | F -1 a S
104 103 ex φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω x a T | F -1 a S
105 104 ralrimiva φ F : S T a K F -1 a S x 𝒫 a T | F -1 a S x ω x a T | F -1 a S
106 44 72 105 3jca φ F : S T a K F -1 a S T a T | F -1 a S x a T | F -1 a S T x a T | F -1 a S x 𝒫 a T | F -1 a S x ω x a T | F -1 a S
107 rabexg T ran sigAlgebra a T | F -1 a S V
108 issiga a T | F -1 a S V a T | F -1 a S sigAlgebra T a T | F -1 a S 𝒫 T T a T | F -1 a S x a T | F -1 a S T x a T | F -1 a S x 𝒫 a T | F -1 a S x ω x a T | F -1 a S
109 6 107 108 3syl φ a T | F -1 a S sigAlgebra T a T | F -1 a S 𝒫 T T a T | F -1 a S x a T | F -1 a S T x a T | F -1 a S x 𝒫 a T | F -1 a S x ω x a T | F -1 a S
110 109 biimpar φ a T | F -1 a S 𝒫 T T a T | F -1 a S x a T | F -1 a S T x a T | F -1 a S x 𝒫 a T | F -1 a S x ω x a T | F -1 a S a T | F -1 a S sigAlgebra T
111 33 37 106 110 syl12anc φ F : S T a K F -1 a S a T | F -1 a S sigAlgebra T
112 3 unieqd φ T = 𝛔 K
113 unisg K V 𝛔 K = K
114 1 113 syl φ 𝛔 K = K
115 112 114 eqtrd φ T = K
116 115 fveq2d φ sigAlgebra T = sigAlgebra K
117 116 eleq2d φ a T | F -1 a S sigAlgebra T a T | F -1 a S sigAlgebra K
118 117 adantr φ F : S T a K F -1 a S a T | F -1 a S sigAlgebra T a T | F -1 a S sigAlgebra K
119 111 118 mpbid φ F : S T a K F -1 a S a T | F -1 a S sigAlgebra K
120 15 adantr φ F : S T a K F -1 a S K T
121 simprr φ F : S T a K F -1 a S a K F -1 a S
122 ssrab K a T | F -1 a S K T a K F -1 a S
123 120 121 122 sylanbrc φ F : S T a K F -1 a S K a T | F -1 a S
124 sigagenss a T | F -1 a S sigAlgebra K K a T | F -1 a S 𝛔 K a T | F -1 a S
125 119 123 124 syl2anc φ F : S T a K F -1 a S 𝛔 K a T | F -1 a S
126 32 125 eqsstrd φ F : S T a K F -1 a S T a T | F -1 a S
127 34 a1i φ F : S T a K F -1 a S a T | F -1 a S T
128 126 127 eqssd φ F : S T a K F -1 a S T = a T | F -1 a S
129 rabid2 T = a T | F -1 a S a T F -1 a S
130 128 129 sylib φ F : S T a K F -1 a S a T F -1 a S
131 2 adantr φ F : S T a K F -1 a S S ran sigAlgebra
132 6 adantr φ F : S T a K F -1 a S T ran sigAlgebra
133 131 132 ismbfm φ F : S T a K F -1 a S F S MblFn μ T F T S a T F -1 a S
134 31 130 133 mpbir2and φ F : S T a K F -1 a S F S MblFn μ T
135 21 134 impbida φ F S MblFn μ T F : S T a K F -1 a S