Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  i1fima Structured version   Unicode version

Theorem i1fima 19572
 Description: Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.)
Assertion
Ref Expression
i1fima

Proof of Theorem i1fima
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 i1ff 19570 . . 3
2 ffun 5595 . . 3
3 inpreima 5859 . . . 4
4 iunid 4148 . . . . . 6
54imaeq2i 5203 . . . . 5
6 imaiun 5994 . . . . 5
75, 6eqtr3i 2460 . . . 4
8 cnvimass 5226 . . . . . 6
9 cnvimarndm 5227 . . . . . 6
108, 9sseqtr4i 3383 . . . . 5
11 df-ss 3336 . . . . 5
1210, 11mpbi 201 . . . 4
133, 7, 123eqtr3g 2493 . . 3
141, 2, 133syl 19 . 2
15 i1frn 19571 . . . 4
16 inss2 3564 . . . 4
17 ssfi 7331 . . . 4
1815, 16, 17sylancl 645 . . 3
19 i1fmbf 19569 . . . . . 6 MblFn
2019adantr 453 . . . . 5 MblFn
211adantr 453 . . . . 5
22 frn 5599 . . . . . . . 8
231, 22syl 16 . . . . . . 7
2416, 23syl5ss 3361 . . . . . 6
2524sselda 3350 . . . . 5
26 mbfimasn 19528 . . . . 5 MblFn
2720, 21, 25, 26syl3anc 1185 . . . 4
2827ralrimiva 2791 . . 3
29 finiunmbl 19440 . . 3
3018, 28, 29syl2anc 644 . 2
3114, 30eqeltrrd 2513 1