| 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
|
eqtr4di |
⊢ ( 𝑎 = ⟨ 𝑠 , 𝑡 ⟩ → ( 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 ∪ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑡 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝑠 ) ) |