Metamath Proof Explorer

Theorem elunirnmbfm

Description: The property of being a measurable function. (Contributed by Thierry Arnoux, 23-Jan-2017)

Ref Expression
Assertion elunirnmbfm ⊢ F ∈ ⋃ ran ⁡ MblFn μ ↔ ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ ⋃ t ⋃ s ∧ ∀ x ∈ t F -1 x ∈ s

Proof

Step Hyp Ref Expression
1 df-mbfm ⊢ MblFn μ = s ∈ ⋃ ran ⁡ sigAlgebra , t ∈ ⋃ ran ⁡ sigAlgebra ⟼ f ∈ ⋃ t ⋃ s | ∀ x ∈ t f -1 x ∈ s
2 1 mpofun ⊢ Fun ⁡ MblFn μ
3 elunirn ⊢ Fun ⁡ MblFn μ → F ∈ ⋃ ran ⁡ MblFn μ ↔ ∃ a ∈ dom ⁡ MblFn μ F ∈ MblFn μ ⁡ a
4 2 3 ax-mp ⊢ F ∈ ⋃ ran ⁡ MblFn μ ↔ ∃ a ∈ dom ⁡ MblFn μ F ∈ MblFn μ ⁡ a
5 ovex ⊢ ⋃ t ⋃ s ∈ V
6 5 rabex ⊢ f ∈ ⋃ t ⋃ s | ∀ x ∈ t f -1 x ∈ s ∈ V
7 1 6 dmmpo ⊢ dom ⁡ MblFn μ = ⋃ ran ⁡ sigAlgebra × ⋃ ran ⁡ sigAlgebra
8 7 rexeqi ⊢ ∃ a ∈ dom ⁡ MblFn μ F ∈ MblFn μ ⁡ a ↔ ∃ a ∈ ⋃ ran ⁡ sigAlgebra × ⋃ ran ⁡ sigAlgebra F ∈ MblFn μ ⁡ a
9 fveq2 ⊢ a = s t → MblFn μ ⁡ a = MblFn μ ⁡ s t
10 df-ov ⊢ s MblFn μ t = MblFn μ ⁡ s t
11 9 10 eqtr4di ⊢ a = s t → MblFn μ ⁡ a = s MblFn μ t
12 11 eleq2d ⊢ a = s t → F ∈ MblFn μ ⁡ a ↔ F ∈ s MblFn μ t
13 12 rexxp ⊢ ∃ a ∈ ⋃ ran ⁡ sigAlgebra × ⋃ ran ⁡ sigAlgebra F ∈ MblFn μ ⁡ a ↔ ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ s MblFn μ t
14 4 8 13 3bitri ⊢ F ∈ ⋃ ran ⁡ MblFn μ ↔ ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ s MblFn μ t
15 simpl ⊢ s ∈ ⋃ ran ⁡ sigAlgebra ∧ t ∈ ⋃ ran ⁡ sigAlgebra → s ∈ ⋃ ran ⁡ sigAlgebra
16 simpr ⊢ s ∈ ⋃ ran ⁡ sigAlgebra ∧ t ∈ ⋃ ran ⁡ sigAlgebra → t ∈ ⋃ ran ⁡ sigAlgebra
17 15 16 ismbfm ⊢ s ∈ ⋃ ran ⁡ sigAlgebra ∧ t ∈ ⋃ ran ⁡ sigAlgebra → F ∈ s MblFn μ t ↔ F ∈ ⋃ t ⋃ s ∧ ∀ x ∈ t F -1 x ∈ s
18 17 2rexbiia ⊢ ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ s MblFn μ t ↔ ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ ⋃ t ⋃ s ∧ ∀ x ∈ t F -1 x ∈ s
19 14 18 bitri ⊢ F ∈ ⋃ ran ⁡ MblFn μ ↔ ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ ⋃ t ⋃ s ∧ ∀ x ∈ t F -1 x ∈ s