Metamath Proof Explorer

Theorem isanmbfm

Description: The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Hypotheses mbfmf.1 ⊢ φ → S ∈ ⋃ ran ⁡ sigAlgebra
mbfmf.2 ⊢ φ → T ∈ ⋃ ran ⁡ sigAlgebra
mbfmf.3 ⊢ φ → F ∈ S MblFn μ T
Assertion isanmbfm ⊢ φ → F ∈ ⋃ ran ⁡ MblFn μ

Proof

Step Hyp Ref Expression
1 mbfmf.1 ⊢ φ → S ∈ ⋃ ran ⁡ sigAlgebra
2 mbfmf.2 ⊢ φ → T ∈ ⋃ ran ⁡ sigAlgebra
3 mbfmf.3 ⊢ φ → F ∈ S MblFn μ T
4 1 2 ismbfm ⊢ φ → F ∈ S MblFn μ T ↔ F ∈ ⋃ T ⋃ S ∧ ∀ x ∈ T F -1 x ∈ S
5 3 4 mpbid ⊢ φ → F ∈ ⋃ T ⋃ S ∧ ∀ x ∈ T F -1 x ∈ S
6 unieq ⊢ s = S → ⋃ s = ⋃ S
7 6 oveq2d ⊢ s = S → ⋃ t ⋃ s = ⋃ t ⋃ S
8 7 eleq2d ⊢ s = S → F ∈ ⋃ t ⋃ s ↔ F ∈ ⋃ t ⋃ S
9 eleq2 ⊢ s = S → F -1 x ∈ s ↔ F -1 x ∈ S
10 9 ralbidv ⊢ s = S → ∀ x ∈ t F -1 x ∈ s ↔ ∀ x ∈ t F -1 x ∈ S
11 8 10 anbi12d ⊢ s = S → F ∈ ⋃ t ⋃ s ∧ ∀ x ∈ t F -1 x ∈ s ↔ F ∈ ⋃ t ⋃ S ∧ ∀ x ∈ t F -1 x ∈ S
12 unieq ⊢ t = T → ⋃ t = ⋃ T
13 12 oveq1d ⊢ t = T → ⋃ t ⋃ S = ⋃ T ⋃ S
14 13 eleq2d ⊢ t = T → F ∈ ⋃ t ⋃ S ↔ F ∈ ⋃ T ⋃ S
15 raleq ⊢ t = T → ∀ x ∈ t F -1 x ∈ S ↔ ∀ x ∈ T F -1 x ∈ S
16 14 15 anbi12d ⊢ t = T → F ∈ ⋃ t ⋃ S ∧ ∀ x ∈ t F -1 x ∈ S ↔ F ∈ ⋃ T ⋃ S ∧ ∀ x ∈ T F -1 x ∈ S
17 11 16 rspc2ev ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ T ∈ ⋃ ran ⁡ sigAlgebra ∧ F ∈ ⋃ T ⋃ S ∧ ∀ x ∈ T F -1 x ∈ S → ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ ⋃ t ⋃ s ∧ ∀ x ∈ t F -1 x ∈ s
18 1 2 5 17 syl3anc ⊢ φ → ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ ⋃ t ⋃ s ∧ ∀ x ∈ t F -1 x ∈ s
19 elunirnmbfm ⊢ F ∈ ⋃ ran ⁡ MblFn μ ↔ ∃ s ∈ ⋃ ran ⁡ sigAlgebra ∃ t ∈ ⋃ ran ⁡ sigAlgebra F ∈ ⋃ t ⋃ s ∧ ∀ x ∈ t F -1 x ∈ s
20 18 19 sylibr ⊢ φ → F ∈ ⋃ ran ⁡ MblFn μ