# Metamath Proof Explorer

## Theorem elunirnmbfm

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

Ref Expression
Assertion elunirnmbfm ( 𝐹 ran MblFnM ↔ ∃ 𝑠 ran sigAlgebra ∃ 𝑡 ran sigAlgebra ( 𝐹 ∈ ( 𝑡m 𝑠 ) ∧ ∀ 𝑥𝑡 ( 𝐹𝑥 ) ∈ 𝑠 ) )

### Proof

Step Hyp Ref Expression
1 df-mbfm MblFnM = ( 𝑠 ran sigAlgebra , 𝑡 ran sigAlgebra ↦ { 𝑓 ∈ ( 𝑡m 𝑠 ) ∣ ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑠 } )
2 1 mpofun Fun MblFnM
3 elunirn ( Fun MblFnM → ( 𝐹 ran MblFnM ↔ ∃ 𝑎 ∈ dom MblFnM 𝐹 ∈ ( MblFnM ‘ 𝑎 ) ) )
4 2 3 ax-mp ( 𝐹 ran MblFnM ↔ ∃ 𝑎 ∈ dom MblFnM 𝐹 ∈ ( MblFnM ‘ 𝑎 ) )
5 ovex ( 𝑡m 𝑠 ) ∈ V
6 5 rabex { 𝑓 ∈ ( 𝑡m 𝑠 ) ∣ ∀ 𝑥𝑡 ( 𝑓𝑥 ) ∈ 𝑠 } ∈ V
7 1 6 dmmpo dom MblFnM = ( ran sigAlgebra × ran sigAlgebra )
8 7 rexeqi ( ∃ 𝑎 ∈ dom MblFnM 𝐹 ∈ ( MblFnM ‘ 𝑎 ) ↔ ∃ 𝑎 ∈ ( ran sigAlgebra × ran sigAlgebra ) 𝐹 ∈ ( MblFnM ‘ 𝑎 ) )
9 fveq2 ( 𝑎 = ⟨ 𝑠 , 𝑡 ⟩ → ( MblFnM ‘ 𝑎 ) = ( MblFnM ‘ ⟨ 𝑠 , 𝑡 ⟩ ) )
10 df-ov ( 𝑠 MblFnM 𝑡 ) = ( MblFnM ‘ ⟨ 𝑠 , 𝑡 ⟩ )
11 9 10 syl6eqr ( 𝑎 = ⟨ 𝑠 , 𝑡 ⟩ → ( MblFnM ‘ 𝑎 ) = ( 𝑠 MblFnM 𝑡 ) )
12 11 eleq2d ( 𝑎 = ⟨ 𝑠 , 𝑡 ⟩ → ( 𝐹 ∈ ( MblFnM ‘ 𝑎 ) ↔ 𝐹 ∈ ( 𝑠 MblFnM 𝑡 ) ) )
13 12 rexxp ( ∃ 𝑎 ∈ ( ran sigAlgebra × ran sigAlgebra ) 𝐹 ∈ ( MblFnM ‘ 𝑎 ) ↔ ∃ 𝑠 ran sigAlgebra ∃ 𝑡 ran sigAlgebra 𝐹 ∈ ( 𝑠 MblFnM 𝑡 ) )
14 4 8 13 3bitri ( 𝐹 ran MblFnM ↔ ∃ 𝑠 ran sigAlgebra ∃ 𝑡 ran sigAlgebra 𝐹 ∈ ( 𝑠 MblFnM 𝑡 ) )
15 simpl ( ( 𝑠 ran sigAlgebra ∧ 𝑡 ran sigAlgebra ) → 𝑠 ran sigAlgebra )
16 simpr ( ( 𝑠 ran sigAlgebra ∧ 𝑡 ran sigAlgebra ) → 𝑡 ran sigAlgebra )
17 15 16 ismbfm ( ( 𝑠 ran sigAlgebra ∧ 𝑡 ran sigAlgebra ) → ( 𝐹 ∈ ( 𝑠 MblFnM 𝑡 ) ↔ ( 𝐹 ∈ ( 𝑡m 𝑠 ) ∧ ∀ 𝑥𝑡 ( 𝐹𝑥 ) ∈ 𝑠 ) ) )
18 17 2rexbiia ( ∃ 𝑠 ran sigAlgebra ∃ 𝑡 ran sigAlgebra 𝐹 ∈ ( 𝑠 MblFnM 𝑡 ) ↔ ∃ 𝑠 ran sigAlgebra ∃ 𝑡 ran sigAlgebra ( 𝐹 ∈ ( 𝑡m 𝑠 ) ∧ ∀ 𝑥𝑡 ( 𝐹𝑥 ) ∈ 𝑠 ) )
19 14 18 bitri ( 𝐹 ran MblFnM ↔ ∃ 𝑠 ran sigAlgebra ∃ 𝑡 ran sigAlgebra ( 𝐹 ∈ ( 𝑡m 𝑠 ) ∧ ∀ 𝑥𝑡 ( 𝐹𝑥 ) ∈ 𝑠 ) )