| Step | Hyp | Ref
| Expression |
| 1 | | mbfimaopn.2 |
. . . . . . . 8
⊢ 𝐺 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) |
| 2 | | eqid 2737 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 3 | | mbfimaopn.1 |
. . . . . . . 8
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 4 | 1, 2, 3 | cnrehmeo 24984 |
. . . . . . 7
⊢ 𝐺 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) |
| 5 | | hmeocn 23768 |
. . . . . . 7
⊢ (𝐺 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,)))Homeo𝐽) → 𝐺 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽)) |
| 6 | 4, 5 | ax-mp 5 |
. . . . . 6
⊢ 𝐺 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) |
| 7 | | cnima 23273 |
. . . . . 6
⊢ ((𝐺 ∈ (((topGen‘ran (,))
×t (topGen‘ran (,))) Cn 𝐽) ∧ 𝐴 ∈ 𝐽) → (◡𝐺 “ 𝐴) ∈ ((topGen‘ran (,))
×t (topGen‘ran (,)))) |
| 8 | 6, 7 | mpan 690 |
. . . . 5
⊢ (𝐴 ∈ 𝐽 → (◡𝐺 “ 𝐴) ∈ ((topGen‘ran (,))
×t (topGen‘ran (,)))) |
| 9 | | mbfimaopn.3 |
. . . . . . . . 9
⊢ 𝐵 = ((,) “ (ℚ ×
ℚ)) |
| 10 | 9 | fveq2i 6909 |
. . . . . . . 8
⊢
(topGen‘𝐵) =
(topGen‘((,) “ (ℚ × ℚ))) |
| 11 | 10 | tgqioo 24821 |
. . . . . . 7
⊢
(topGen‘ran (,)) = (topGen‘𝐵) |
| 12 | 11, 11 | oveq12i 7443 |
. . . . . 6
⊢
((topGen‘ran (,)) ×t (topGen‘ran (,))) =
((topGen‘𝐵)
×t (topGen‘𝐵)) |
| 13 | | qtopbas 24780 |
. . . . . . . 8
⊢ ((,)
“ (ℚ × ℚ)) ∈ TopBases |
| 14 | 9, 13 | eqeltri 2837 |
. . . . . . 7
⊢ 𝐵 ∈
TopBases |
| 15 | | txbasval 23614 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ∈ TopBases) →
((topGen‘𝐵)
×t (topGen‘𝐵)) = (𝐵 ×t 𝐵)) |
| 16 | 14, 14, 15 | mp2an 692 |
. . . . . 6
⊢
((topGen‘𝐵)
×t (topGen‘𝐵)) = (𝐵 ×t 𝐵) |
| 17 | | mbfimaopn.4 |
. . . . . . . 8
⊢ 𝐾 = ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) |
| 18 | 17 | txval 23572 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ∈ TopBases) → (𝐵 ×t 𝐵) = (topGen‘𝐾)) |
| 19 | 14, 14, 18 | mp2an 692 |
. . . . . 6
⊢ (𝐵 ×t 𝐵) = (topGen‘𝐾) |
| 20 | 12, 16, 19 | 3eqtri 2769 |
. . . . 5
⊢
((topGen‘ran (,)) ×t (topGen‘ran (,))) =
(topGen‘𝐾) |
| 21 | 8, 20 | eleqtrdi 2851 |
. . . 4
⊢ (𝐴 ∈ 𝐽 → (◡𝐺 “ 𝐴) ∈ (topGen‘𝐾)) |
| 22 | 17 | txbas 23575 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ∈ TopBases) → 𝐾 ∈
TopBases) |
| 23 | 14, 14, 22 | mp2an 692 |
. . . . 5
⊢ 𝐾 ∈
TopBases |
| 24 | | eltg3 22969 |
. . . . 5
⊢ (𝐾 ∈ TopBases → ((◡𝐺 “ 𝐴) ∈ (topGen‘𝐾) ↔ ∃𝑡(𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡))) |
| 25 | 23, 24 | ax-mp 5 |
. . . 4
⊢ ((◡𝐺 “ 𝐴) ∈ (topGen‘𝐾) ↔ ∃𝑡(𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) |
| 26 | 21, 25 | sylib 218 |
. . 3
⊢ (𝐴 ∈ 𝐽 → ∃𝑡(𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) |
| 27 | 26 | adantl 481 |
. 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → ∃𝑡(𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) |
| 28 | 1 | cnref1o 13027 |
. . . . . . . 8
⊢ 𝐺:(ℝ ×
ℝ)–1-1-onto→ℂ |
| 29 | | f1ofo 6855 |
. . . . . . . 8
⊢ (𝐺:(ℝ ×
ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)–onto→ℂ) |
| 30 | 28, 29 | ax-mp 5 |
. . . . . . 7
⊢ 𝐺:(ℝ ×
ℝ)–onto→ℂ |
| 31 | | elssuni 4937 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽) |
| 32 | 3 | cnfldtopon 24803 |
. . . . . . . . . 10
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 33 | 32 | toponunii 22922 |
. . . . . . . . 9
⊢ ℂ =
∪ 𝐽 |
| 34 | 31, 33 | sseqtrrdi 4025 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ℂ) |
| 35 | 34 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → 𝐴 ⊆ ℂ) |
| 36 | | foimacnv 6865 |
. . . . . . 7
⊢ ((𝐺:(ℝ ×
ℝ)–onto→ℂ ∧
𝐴 ⊆ ℂ) →
(𝐺 “ (◡𝐺 “ 𝐴)) = 𝐴) |
| 37 | 30, 35, 36 | sylancr 587 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → (𝐺 “ (◡𝐺 “ 𝐴)) = 𝐴) |
| 38 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → (◡𝐺 “ 𝐴) = ∪ 𝑡) |
| 39 | 38 | imaeq2d 6078 |
. . . . . . 7
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → (𝐺 “ (◡𝐺 “ 𝐴)) = (𝐺 “ ∪ 𝑡)) |
| 40 | | imauni 7266 |
. . . . . . 7
⊢ (𝐺 “ ∪ 𝑡) =
∪ 𝑤 ∈ 𝑡 (𝐺 “ 𝑤) |
| 41 | 39, 40 | eqtrdi 2793 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → (𝐺 “ (◡𝐺 “ 𝐴)) = ∪
𝑤 ∈ 𝑡 (𝐺 “ 𝑤)) |
| 42 | 37, 41 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → 𝐴 = ∪ 𝑤 ∈ 𝑡 (𝐺 “ 𝑤)) |
| 43 | 42 | imaeq2d 6078 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → (◡𝐹 “ 𝐴) = (◡𝐹 “ ∪
𝑤 ∈ 𝑡 (𝐺 “ 𝑤))) |
| 44 | | imaiun 7265 |
. . . 4
⊢ (◡𝐹 “ ∪
𝑤 ∈ 𝑡 (𝐺 “ 𝑤)) = ∪
𝑤 ∈ 𝑡 (◡𝐹 “ (𝐺 “ 𝑤)) |
| 45 | 43, 44 | eqtrdi 2793 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → (◡𝐹 “ 𝐴) = ∪
𝑤 ∈ 𝑡 (◡𝐹 “ (𝐺 “ 𝑤))) |
| 46 | | ssdomg 9040 |
. . . . . . 7
⊢ (𝐾 ∈ TopBases → (𝑡 ⊆ 𝐾 → 𝑡 ≼ 𝐾)) |
| 47 | 23, 46 | ax-mp 5 |
. . . . . 6
⊢ (𝑡 ⊆ 𝐾 → 𝑡 ≼ 𝐾) |
| 48 | | omelon 9686 |
. . . . . . . . . . 11
⊢ ω
∈ On |
| 49 | | nnenom 14021 |
. . . . . . . . . . . 12
⊢ ℕ
≈ ω |
| 50 | 49 | ensymi 9044 |
. . . . . . . . . . 11
⊢ ω
≈ ℕ |
| 51 | | isnumi 9986 |
. . . . . . . . . . 11
⊢ ((ω
∈ On ∧ ω ≈ ℕ) → ℕ ∈ dom
card) |
| 52 | 48, 50, 51 | mp2an 692 |
. . . . . . . . . 10
⊢ ℕ
∈ dom card |
| 53 | | qnnen 16249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℚ
≈ ℕ |
| 54 | | xpen 9180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℚ
≈ ℕ ∧ ℚ ≈ ℕ) → (ℚ × ℚ)
≈ (ℕ × ℕ)) |
| 55 | 53, 53, 54 | mp2an 692 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℚ
× ℚ) ≈ (ℕ × ℕ) |
| 56 | | xpnnen 16247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℕ
× ℕ) ≈ ℕ |
| 57 | 55, 56 | entri 9048 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℚ
× ℚ) ≈ ℕ |
| 58 | 57, 49 | entr2i 9049 |
. . . . . . . . . . . . . . . . 17
⊢ ω
≈ (ℚ × ℚ) |
| 59 | | isnumi 9986 |
. . . . . . . . . . . . . . . . 17
⊢ ((ω
∈ On ∧ ω ≈ (ℚ × ℚ)) → (ℚ
× ℚ) ∈ dom card) |
| 60 | 48, 58, 59 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (ℚ
× ℚ) ∈ dom card |
| 61 | | ioof 13487 |
. . . . . . . . . . . . . . . . . 18
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 62 | | ffun 6739 |
. . . . . . . . . . . . . . . . . 18
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → Fun (,)) |
| 63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ Fun
(,) |
| 64 | | qssre 13001 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℚ
⊆ ℝ |
| 65 | | ressxr 11305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℝ
⊆ ℝ* |
| 66 | 64, 65 | sstri 3993 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℚ
⊆ ℝ* |
| 67 | | xpss12 5700 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℚ
⊆ ℝ* ∧ ℚ ⊆ ℝ*) →
(ℚ × ℚ) ⊆ (ℝ* ×
ℝ*)) |
| 68 | 66, 66, 67 | mp2an 692 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℚ
× ℚ) ⊆ (ℝ* ×
ℝ*) |
| 69 | 61 | fdmi 6747 |
. . . . . . . . . . . . . . . . . 18
⊢ dom (,) =
(ℝ* × ℝ*) |
| 70 | 68, 69 | sseqtrri 4033 |
. . . . . . . . . . . . . . . . 17
⊢ (ℚ
× ℚ) ⊆ dom (,) |
| 71 | | fores 6830 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun (,)
∧ (ℚ × ℚ) ⊆ dom (,)) → ((,) ↾ (ℚ
× ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ ×
ℚ))) |
| 72 | 63, 70, 71 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ ((,)
↾ (ℚ × ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ ×
ℚ)) |
| 73 | | fodomnum 10097 |
. . . . . . . . . . . . . . . 16
⊢ ((ℚ
× ℚ) ∈ dom card → (((,) ↾ (ℚ ×
ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ × ℚ)) →
((,) “ (ℚ × ℚ)) ≼ (ℚ ×
ℚ))) |
| 74 | 60, 72, 73 | mp2 9 |
. . . . . . . . . . . . . . 15
⊢ ((,)
“ (ℚ × ℚ)) ≼ (ℚ ×
ℚ) |
| 75 | 9, 74 | eqbrtri 5164 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ≼ (ℚ ×
ℚ) |
| 76 | | domentr 9053 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ≼ (ℚ ×
ℚ) ∧ (ℚ × ℚ) ≈ ℕ) → 𝐵 ≼
ℕ) |
| 77 | 75, 57, 76 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ 𝐵 ≼
ℕ |
| 78 | 14 | elexi 3503 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈ V |
| 79 | 78 | xpdom1 9111 |
. . . . . . . . . . . . 13
⊢ (𝐵 ≼ ℕ → (𝐵 × 𝐵) ≼ (ℕ × 𝐵)) |
| 80 | 77, 79 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐵 × 𝐵) ≼ (ℕ × 𝐵) |
| 81 | | nnex 12272 |
. . . . . . . . . . . . . 14
⊢ ℕ
∈ V |
| 82 | 81 | xpdom2 9107 |
. . . . . . . . . . . . 13
⊢ (𝐵 ≼ ℕ → (ℕ
× 𝐵) ≼ (ℕ
× ℕ)) |
| 83 | 77, 82 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (ℕ
× 𝐵) ≼ (ℕ
× ℕ) |
| 84 | | domtr 9047 |
. . . . . . . . . . . 12
⊢ (((𝐵 × 𝐵) ≼ (ℕ × 𝐵) ∧ (ℕ × 𝐵) ≼ (ℕ × ℕ)) →
(𝐵 × 𝐵) ≼ (ℕ ×
ℕ)) |
| 85 | 80, 83, 84 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝐵 × 𝐵) ≼ (ℕ ×
ℕ) |
| 86 | | domentr 9053 |
. . . . . . . . . . 11
⊢ (((𝐵 × 𝐵) ≼ (ℕ × ℕ) ∧
(ℕ × ℕ) ≈ ℕ) → (𝐵 × 𝐵) ≼ ℕ) |
| 87 | 85, 56, 86 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝐵 × 𝐵) ≼ ℕ |
| 88 | | numdom 10078 |
. . . . . . . . . 10
⊢ ((ℕ
∈ dom card ∧ (𝐵
× 𝐵) ≼ ℕ)
→ (𝐵 × 𝐵) ∈ dom
card) |
| 89 | 52, 87, 88 | mp2an 692 |
. . . . . . . . 9
⊢ (𝐵 × 𝐵) ∈ dom card |
| 90 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) |
| 91 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 92 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
| 93 | 91, 92 | xpex 7773 |
. . . . . . . . . . 11
⊢ (𝑥 × 𝑦) ∈ V |
| 94 | 90, 93 | fnmpoi 8095 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) Fn (𝐵 × 𝐵) |
| 95 | | dffn4 6826 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) Fn (𝐵 × 𝐵) ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)):(𝐵 × 𝐵)–onto→ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦))) |
| 96 | 94, 95 | mpbi 230 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)):(𝐵 × 𝐵)–onto→ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) |
| 97 | | fodomnum 10097 |
. . . . . . . . 9
⊢ ((𝐵 × 𝐵) ∈ dom card → ((𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)):(𝐵 × 𝐵)–onto→ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) → ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ≼ (𝐵 × 𝐵))) |
| 98 | 89, 96, 97 | mp2 9 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ≼ (𝐵 × 𝐵) |
| 99 | | domtr 9047 |
. . . . . . . 8
⊢ ((ran
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ≼ (𝐵 × 𝐵) ∧ (𝐵 × 𝐵) ≼ ℕ) → ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ≼ ℕ) |
| 100 | 98, 87, 99 | mp2an 692 |
. . . . . . 7
⊢ ran
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ≼ ℕ |
| 101 | 17, 100 | eqbrtri 5164 |
. . . . . 6
⊢ 𝐾 ≼
ℕ |
| 102 | | domtr 9047 |
. . . . . 6
⊢ ((𝑡 ≼ 𝐾 ∧ 𝐾 ≼ ℕ) → 𝑡 ≼ ℕ) |
| 103 | 47, 101, 102 | sylancl 586 |
. . . . 5
⊢ (𝑡 ⊆ 𝐾 → 𝑡 ≼ ℕ) |
| 104 | 103 | ad2antrl 728 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → 𝑡 ≼ ℕ) |
| 105 | 17 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐾 ↔ 𝑤 ∈ ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦))) |
| 106 | 90, 93 | elrnmpo 7569 |
. . . . . . . . 9
⊢ (𝑤 ∈ ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑤 = (𝑥 × 𝑦)) |
| 107 | 105, 106 | bitri 275 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝐾 ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑤 = (𝑥 × 𝑦)) |
| 108 | | elin 3967 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∩ (◡(ℑ ∘ 𝐹) “ 𝑦)) ↔ (𝑧 ∈ (◡(ℜ ∘ 𝐹) “ 𝑥) ∧ 𝑧 ∈ (◡(ℑ ∘ 𝐹) “ 𝑦))) |
| 109 | | mbff 25660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
| 110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:dom 𝐹⟶ℂ) |
| 111 | | fvco3 7008 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → ((ℜ ∘ 𝐹)‘𝑧) = (ℜ‘(𝐹‘𝑧))) |
| 112 | 110, 111 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → ((ℜ ∘ 𝐹)‘𝑧) = (ℜ‘(𝐹‘𝑧))) |
| 113 | 112 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → (((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥 ↔ (ℜ‘(𝐹‘𝑧)) ∈ 𝑥)) |
| 114 | | fvco3 7008 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑧 ∈ dom 𝐹) → ((ℑ ∘ 𝐹)‘𝑧) = (ℑ‘(𝐹‘𝑧))) |
| 115 | 110, 114 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → ((ℑ ∘ 𝐹)‘𝑧) = (ℑ‘(𝐹‘𝑧))) |
| 116 | 115 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → (((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦 ↔ (ℑ‘(𝐹‘𝑧)) ∈ 𝑦)) |
| 117 | 113, 116 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → ((((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦) ↔ ((ℜ‘(𝐹‘𝑧)) ∈ 𝑥 ∧ (ℑ‘(𝐹‘𝑧)) ∈ 𝑦))) |
| 118 | 110 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
| 119 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = (𝐹‘𝑧) → (ℜ‘𝑤) = (ℜ‘(𝐹‘𝑧))) |
| 120 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = (𝐹‘𝑧) → (ℑ‘𝑤) = (ℑ‘(𝐹‘𝑧))) |
| 121 | 119, 120 | opeq12d 4881 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (𝐹‘𝑧) → 〈(ℜ‘𝑤), (ℑ‘𝑤)〉 =
〈(ℜ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧))〉) |
| 122 | 1 | cnrecnv 15204 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ◡𝐺 = (𝑤 ∈ ℂ ↦
〈(ℜ‘𝑤),
(ℑ‘𝑤)〉) |
| 123 | | opex 5469 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈(ℜ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧))〉 ∈ V |
| 124 | 121, 122,
123 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑧) ∈ ℂ → (◡𝐺‘(𝐹‘𝑧)) = 〈(ℜ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧))〉) |
| 125 | 118, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → (◡𝐺‘(𝐹‘𝑧)) = 〈(ℜ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧))〉) |
| 126 | 125 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → ((◡𝐺‘(𝐹‘𝑧)) ∈ (𝑥 × 𝑦) ↔ 〈(ℜ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧))〉 ∈ (𝑥 × 𝑦))) |
| 127 | 118 | biantrurd 532 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → ((◡𝐺‘(𝐹‘𝑧)) ∈ (𝑥 × 𝑦) ↔ ((𝐹‘𝑧) ∈ ℂ ∧ (◡𝐺‘(𝐹‘𝑧)) ∈ (𝑥 × 𝑦)))) |
| 128 | 126, 127 | bitr3d 281 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → (〈(ℜ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧))〉 ∈ (𝑥 × 𝑦) ↔ ((𝐹‘𝑧) ∈ ℂ ∧ (◡𝐺‘(𝐹‘𝑧)) ∈ (𝑥 × 𝑦)))) |
| 129 | | opelxp 5721 |
. . . . . . . . . . . . . . . . 17
⊢
(〈(ℜ‘(𝐹‘𝑧)), (ℑ‘(𝐹‘𝑧))〉 ∈ (𝑥 × 𝑦) ↔ ((ℜ‘(𝐹‘𝑧)) ∈ 𝑥 ∧ (ℑ‘(𝐹‘𝑧)) ∈ 𝑦)) |
| 130 | | f1ocnv 6860 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺:(ℝ ×
ℝ)–1-1-onto→ℂ → ◡𝐺:ℂ–1-1-onto→(ℝ × ℝ)) |
| 131 | | f1ofn 6849 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → ◡𝐺 Fn ℂ) |
| 132 | 28, 130, 131 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
⊢ ◡𝐺 Fn ℂ |
| 133 | | elpreima 7078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝐺 Fn ℂ → ((𝐹‘𝑧) ∈ (◡◡𝐺 “ (𝑥 × 𝑦)) ↔ ((𝐹‘𝑧) ∈ ℂ ∧ (◡𝐺‘(𝐹‘𝑧)) ∈ (𝑥 × 𝑦)))) |
| 134 | 132, 133 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑧) ∈ (◡◡𝐺 “ (𝑥 × 𝑦)) ↔ ((𝐹‘𝑧) ∈ ℂ ∧ (◡𝐺‘(𝐹‘𝑧)) ∈ (𝑥 × 𝑦))) |
| 135 | | imacnvcnv 6226 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡◡𝐺 “ (𝑥 × 𝑦)) = (𝐺 “ (𝑥 × 𝑦)) |
| 136 | 135 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑧) ∈ (◡◡𝐺 “ (𝑥 × 𝑦)) ↔ (𝐹‘𝑧) ∈ (𝐺 “ (𝑥 × 𝑦))) |
| 137 | 134, 136 | bitr3i 277 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (◡𝐺‘(𝐹‘𝑧)) ∈ (𝑥 × 𝑦)) ↔ (𝐹‘𝑧) ∈ (𝐺 “ (𝑥 × 𝑦))) |
| 138 | 128, 129,
137 | 3bitr3g 313 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → (((ℜ‘(𝐹‘𝑧)) ∈ 𝑥 ∧ (ℑ‘(𝐹‘𝑧)) ∈ 𝑦) ↔ (𝐹‘𝑧) ∈ (𝐺 “ (𝑥 × 𝑦)))) |
| 139 | 117, 138 | bitrd 279 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ dom 𝐹) → ((((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦) ↔ (𝐹‘𝑧) ∈ (𝐺 “ (𝑥 × 𝑦)))) |
| 140 | 139 | pm5.32da 579 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ dom 𝐹 ∧ (((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦)) ↔ (𝑧 ∈ dom 𝐹 ∧ (𝐹‘𝑧) ∈ (𝐺 “ (𝑥 × 𝑦))))) |
| 141 | | ref 15151 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℜ:ℂ⟶ℝ |
| 142 | | fco 6760 |
. . . . . . . . . . . . . . . . . . 19
⊢
((ℜ:ℂ⟶ℝ ∧ 𝐹:dom 𝐹⟶ℂ) → (ℜ ∘
𝐹):dom 𝐹⟶ℝ) |
| 143 | 141, 109,
142 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ MblFn → (ℜ
∘ 𝐹):dom 𝐹⟶ℝ) |
| 144 | | ffn 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℜ
∘ 𝐹):dom 𝐹⟶ℝ → (ℜ
∘ 𝐹) Fn dom 𝐹) |
| 145 | | elpreima 7078 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℜ
∘ 𝐹) Fn dom 𝐹 → (𝑧 ∈ (◡(ℜ ∘ 𝐹) “ 𝑥) ↔ (𝑧 ∈ dom 𝐹 ∧ ((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥))) |
| 146 | 143, 144,
145 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ MblFn → (𝑧 ∈ (◡(ℜ ∘ 𝐹) “ 𝑥) ↔ (𝑧 ∈ dom 𝐹 ∧ ((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥))) |
| 147 | | imf 15152 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℑ:ℂ⟶ℝ |
| 148 | | fco 6760 |
. . . . . . . . . . . . . . . . . . 19
⊢
((ℑ:ℂ⟶ℝ ∧ 𝐹:dom 𝐹⟶ℂ) → (ℑ ∘
𝐹):dom 𝐹⟶ℝ) |
| 149 | 147, 109,
148 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ MblFn → (ℑ
∘ 𝐹):dom 𝐹⟶ℝ) |
| 150 | | ffn 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℑ
∘ 𝐹):dom 𝐹⟶ℝ → (ℑ
∘ 𝐹) Fn dom 𝐹) |
| 151 | | elpreima 7078 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℑ
∘ 𝐹) Fn dom 𝐹 → (𝑧 ∈ (◡(ℑ ∘ 𝐹) “ 𝑦) ↔ (𝑧 ∈ dom 𝐹 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦))) |
| 152 | 149, 150,
151 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ MblFn → (𝑧 ∈ (◡(ℑ ∘ 𝐹) “ 𝑦) ↔ (𝑧 ∈ dom 𝐹 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦))) |
| 153 | 146, 152 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ MblFn → ((𝑧 ∈ (◡(ℜ ∘ 𝐹) “ 𝑥) ∧ 𝑧 ∈ (◡(ℑ ∘ 𝐹) “ 𝑦)) ↔ ((𝑧 ∈ dom 𝐹 ∧ ((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥) ∧ (𝑧 ∈ dom 𝐹 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦)))) |
| 154 | | anandi 676 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ dom 𝐹 ∧ (((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦)) ↔ ((𝑧 ∈ dom 𝐹 ∧ ((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥) ∧ (𝑧 ∈ dom 𝐹 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦))) |
| 155 | 153, 154 | bitr4di 289 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ MblFn → ((𝑧 ∈ (◡(ℜ ∘ 𝐹) “ 𝑥) ∧ 𝑧 ∈ (◡(ℑ ∘ 𝐹) “ 𝑦)) ↔ (𝑧 ∈ dom 𝐹 ∧ (((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦)))) |
| 156 | 155 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ (◡(ℜ ∘ 𝐹) “ 𝑥) ∧ 𝑧 ∈ (◡(ℑ ∘ 𝐹) “ 𝑦)) ↔ (𝑧 ∈ dom 𝐹 ∧ (((ℜ ∘ 𝐹)‘𝑧) ∈ 𝑥 ∧ ((ℑ ∘ 𝐹)‘𝑧) ∈ 𝑦)))) |
| 157 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹) |
| 158 | | elpreima 7078 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn dom 𝐹 → (𝑧 ∈ (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦))) ↔ (𝑧 ∈ dom 𝐹 ∧ (𝐹‘𝑧) ∈ (𝐺 “ (𝑥 × 𝑦))))) |
| 159 | 109, 157,
158 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ MblFn → (𝑧 ∈ (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦))) ↔ (𝑧 ∈ dom 𝐹 ∧ (𝐹‘𝑧) ∈ (𝐺 “ (𝑥 × 𝑦))))) |
| 160 | 159 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦))) ↔ (𝑧 ∈ dom 𝐹 ∧ (𝐹‘𝑧) ∈ (𝐺 “ (𝑥 × 𝑦))))) |
| 161 | 140, 156,
160 | 3bitr4d 311 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 ∈ (◡(ℜ ∘ 𝐹) “ 𝑥) ∧ 𝑧 ∈ (◡(ℑ ∘ 𝐹) “ 𝑦)) ↔ 𝑧 ∈ (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦))))) |
| 162 | 108, 161 | bitrid 283 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑧 ∈ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∩ (◡(ℑ ∘ 𝐹) “ 𝑦)) ↔ 𝑧 ∈ (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦))))) |
| 163 | 162 | eqrdv 2735 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((◡(ℜ ∘ 𝐹) “ 𝑥) ∩ (◡(ℑ ∘ 𝐹) “ 𝑦)) = (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦)))) |
| 164 | | ismbfcn 25664 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:dom 𝐹⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ
∘ 𝐹) ∈
MblFn))) |
| 165 | 109, 164 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ MblFn → (𝐹 ∈ MblFn ↔ ((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℑ ∘ 𝐹)
∈ MblFn))) |
| 166 | 165 | ibi 267 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ MblFn → ((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℑ ∘ 𝐹)
∈ MblFn)) |
| 167 | 166 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ MblFn → (ℜ
∘ 𝐹) ∈
MblFn) |
| 168 | | ismbf 25663 |
. . . . . . . . . . . . . . . 16
⊢ ((ℜ
∘ 𝐹):dom 𝐹⟶ℝ → ((ℜ
∘ 𝐹) ∈ MblFn
↔ ∀𝑥 ∈ ran
(,)(◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)) |
| 169 | 143, 168 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ MblFn → ((ℜ
∘ 𝐹) ∈ MblFn
↔ ∀𝑥 ∈ ran
(,)(◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)) |
| 170 | 167, 169 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ MblFn →
∀𝑥 ∈ ran
(,)(◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
| 171 | 170 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ ran (,)(◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
| 172 | | imassrn 6089 |
. . . . . . . . . . . . . . 15
⊢ ((,)
“ (ℚ × ℚ)) ⊆ ran (,) |
| 173 | 9, 172 | eqsstri 4030 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ⊆ ran
(,) |
| 174 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
| 175 | 173, 174 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ ran (,)) |
| 176 | | rsp 3247 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
ran (,)(◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol → (𝑥 ∈ ran (,) → (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)) |
| 177 | 171, 175,
176 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
| 178 | 166 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ MblFn → (ℑ
∘ 𝐹) ∈
MblFn) |
| 179 | | ismbf 25663 |
. . . . . . . . . . . . . . . 16
⊢ ((ℑ
∘ 𝐹):dom 𝐹⟶ℝ → ((ℑ
∘ 𝐹) ∈ MblFn
↔ ∀𝑦 ∈ ran
(,)(◡(ℑ ∘ 𝐹) “ 𝑦) ∈ dom vol)) |
| 180 | 149, 179 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ MblFn → ((ℑ
∘ 𝐹) ∈ MblFn
↔ ∀𝑦 ∈ ran
(,)(◡(ℑ ∘ 𝐹) “ 𝑦) ∈ dom vol)) |
| 181 | 178, 180 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ MblFn →
∀𝑦 ∈ ran
(,)(◡(ℑ ∘ 𝐹) “ 𝑦) ∈ dom vol) |
| 182 | 181 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑦 ∈ ran (,)(◡(ℑ ∘ 𝐹) “ 𝑦) ∈ dom vol) |
| 183 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
| 184 | 173, 183 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ ran (,)) |
| 185 | | rsp 3247 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
ran (,)(◡(ℑ ∘ 𝐹) “ 𝑦) ∈ dom vol → (𝑦 ∈ ran (,) → (◡(ℑ ∘ 𝐹) “ 𝑦) ∈ dom vol)) |
| 186 | 182, 184,
185 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (◡(ℑ ∘ 𝐹) “ 𝑦) ∈ dom vol) |
| 187 | | inmbl 25577 |
. . . . . . . . . . . 12
⊢ (((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑦) ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ 𝑥) ∩ (◡(ℑ ∘ 𝐹) “ 𝑦)) ∈ dom vol) |
| 188 | 177, 186,
187 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((◡(ℜ ∘ 𝐹) “ 𝑥) ∩ (◡(ℑ ∘ 𝐹) “ 𝑦)) ∈ dom vol) |
| 189 | 163, 188 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦))) ∈ dom vol) |
| 190 | | imaeq2 6074 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑥 × 𝑦) → (𝐺 “ 𝑤) = (𝐺 “ (𝑥 × 𝑦))) |
| 191 | 190 | imaeq2d 6078 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑥 × 𝑦) → (◡𝐹 “ (𝐺 “ 𝑤)) = (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦)))) |
| 192 | 191 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 × 𝑦) → ((◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol ↔ (◡𝐹 “ (𝐺 “ (𝑥 × 𝑦))) ∈ dom vol)) |
| 193 | 189, 192 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝐹 ∈ MblFn ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑤 = (𝑥 × 𝑦) → (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol)) |
| 194 | 193 | rexlimdvva 3213 |
. . . . . . . 8
⊢ (𝐹 ∈ MblFn →
(∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑤 = (𝑥 × 𝑦) → (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol)) |
| 195 | 107, 194 | biimtrid 242 |
. . . . . . 7
⊢ (𝐹 ∈ MblFn → (𝑤 ∈ 𝐾 → (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol)) |
| 196 | 195 | ralrimiv 3145 |
. . . . . 6
⊢ (𝐹 ∈ MblFn →
∀𝑤 ∈ 𝐾 (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol) |
| 197 | | ssralv 4052 |
. . . . . 6
⊢ (𝑡 ⊆ 𝐾 → (∀𝑤 ∈ 𝐾 (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol → ∀𝑤 ∈ 𝑡 (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol)) |
| 198 | 196, 197 | mpan9 506 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝑡 ⊆ 𝐾) → ∀𝑤 ∈ 𝑡 (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol) |
| 199 | 198 | ad2ant2r 747 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → ∀𝑤 ∈ 𝑡 (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol) |
| 200 | | iunmbl2 25592 |
. . . 4
⊢ ((𝑡 ≼ ℕ ∧
∀𝑤 ∈ 𝑡 (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol) → ∪ 𝑤 ∈ 𝑡 (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol) |
| 201 | 104, 199,
200 | syl2anc 584 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → ∪ 𝑤 ∈ 𝑡 (◡𝐹 “ (𝐺 “ 𝑤)) ∈ dom vol) |
| 202 | 45, 201 | eqeltrd 2841 |
. 2
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) ∧ (𝑡 ⊆ 𝐾 ∧ (◡𝐺 “ 𝐴) = ∪ 𝑡)) → (◡𝐹 “ 𝐴) ∈ dom vol) |
| 203 | 27, 202 | exlimddv 1935 |
1
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol) |