Metamath Proof Explorer

Theorem mbfsup

Description: The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, B ( n , x ) is a function of both n and x , since it is an n -indexed sequence of functions on x . (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbfsup.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
mbfsup.2 ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) )
mbfsup.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
mbfsup.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
mbfsup.5 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ )
mbfsup.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝐵 ≤ 𝑦 )
Assertion mbfsup ( 𝜑 → 𝐺 ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfsup.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 mbfsup.2 ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) )
3 mbfsup.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 mbfsup.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5 mbfsup.5 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ )
6 mbfsup.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝐵 ≤ 𝑦 )
7 5 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
8 7 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
9 8 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ )
10 9 frnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⊆ ℝ )
11 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
12 3 11 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
13 12 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ 𝑍 )
15 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑛 ∈ 𝑍 ↦ 𝐵 )
16 15 8 dmmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) = 𝑍 )
17 14 16 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ dom ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) )
18 17 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ≠ ∅ )
19 dm0rn0 ⊢ ( dom ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) = ∅ ↔ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) = ∅ )
20 19 necon3bii ⊢ ( dom ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ≠ ∅ ↔ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ≠ ∅ )
21 18 20 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ≠ ∅ )
22 9 ffnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) Fn 𝑍 )
23 breq1 ⊢ ( 𝑧 = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) → ( 𝑧 ≤ 𝑦 ↔ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ≤ 𝑦 ) )
24 23 ralrn ⊢ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) Fn 𝑍 → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑚 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ≤ 𝑦 ) )
25 22 24 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑚 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ≤ 𝑦 ) )
26 nffvmpt1 ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 )
27 nfcv ⊢ Ⅎ 𝑛 ≤
28 nfcv ⊢ Ⅎ 𝑛 𝑦
29 26 27 28 nfbr ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ≤ 𝑦
30 nfv ⊢ Ⅎ 𝑚 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ≤ 𝑦
31 fveq2 ⊢ ( 𝑚 = 𝑛 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) )
32 31 breq1d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ≤ 𝑦 ↔ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ≤ 𝑦 ) )
33 29 30 32 cbvralw ⊢ ( ∀ 𝑚 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ≤ 𝑦 )
34 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
35 15 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝐵 ∈ ℝ ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = 𝐵 )
36 34 8 35 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = 𝐵 )
37 36 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
38 37 ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
39 33 38 syl5bb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑚 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
40 25 39 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
41 40 rexbidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
42 6 41 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
43 10 21 42 suprcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) ∈ ℝ )
44 43 2 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℝ )
45 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
46 ltso ⊢ < Or ℝ
47 46 supex ⊢ sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) ∈ V
48 2 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) ∈ V ) → ( 𝐺 ‘ 𝑥 ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) )
49 45 47 48 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) )
50 49 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑡 < ( 𝐺 ‘ 𝑥 ) ↔ 𝑡 < sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) ) )
51 10 21 42 3jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⊆ ℝ ∧ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
52 51 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⊆ ℝ ∧ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
53 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑡 ∈ ℝ )
54 suprlub ⊢ ( ( ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⊆ ℝ ∧ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑡 < sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) ↔ ∃ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑡 < 𝑧 ) )
55 52 53 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑡 < sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) ↔ ∃ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑡 < 𝑧 ) )
56 22 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) Fn 𝑍 )
57 breq2 ⊢ ( 𝑧 = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) → ( 𝑡 < 𝑧 ↔ 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ) )
58 57 rexrn ⊢ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) Fn 𝑍 → ( ∃ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑡 < 𝑧 ↔ ∃ 𝑚 ∈ 𝑍 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ) )
59 56 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑡 < 𝑧 ↔ ∃ 𝑚 ∈ 𝑍 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ) )
60 nfcv ⊢ Ⅎ 𝑛 𝑡
61 nfcv ⊢ Ⅎ 𝑛 <
62 60 61 26 nfbr ⊢ Ⅎ 𝑛 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 )
63 nfv ⊢ Ⅎ 𝑚 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 )
64 31 breq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ↔ 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
65 62 63 64 cbvrexw ⊢ ( ∃ 𝑚 ∈ 𝑍 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) )
66 15 fvmpt2i ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( I ‘ 𝐵 ) )
67 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
68 67 fvmpt2i ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( I ‘ 𝐵 ) )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( I ‘ 𝐵 ) )
70 69 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( I ‘ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
71 66 70 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
72 71 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ↔ 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
73 72 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
74 73 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
75 65 74 syl5bb ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑚 ∈ 𝑍 𝑡 < ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑚 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
76 59 75 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) 𝑡 < 𝑧 ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
77 50 55 76 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑡 < ( 𝐺 ‘ 𝑥 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
78 77 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑡 < ( 𝐺 ‘ 𝑥 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
79 nfv ⊢ Ⅎ 𝑧 ( 𝑡 < ( 𝐺 ‘ 𝑥 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
80 nfcv ⊢ Ⅎ 𝑥 𝑡
81 nfcv ⊢ Ⅎ 𝑥 <
82 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) , ℝ , < ) )
83 2 82 nfcxfr ⊢ Ⅎ 𝑥 𝐺
84 nfcv ⊢ Ⅎ 𝑥 𝑧
85 83 84 nffv ⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑧 )
86 80 81 85 nfbr ⊢ Ⅎ 𝑥 𝑡 < ( 𝐺 ‘ 𝑧 )
87 nfcv ⊢ Ⅎ 𝑥 𝑍
88 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 )
89 80 81 88 nfbr ⊢ Ⅎ 𝑥 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 )
90 87 89 nfrex ⊢ Ⅎ 𝑥 ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 )
91 86 90 nfbi ⊢ Ⅎ 𝑥 ( 𝑡 < ( 𝐺 ‘ 𝑧 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) )
92 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) )
93 92 breq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑡 < ( 𝐺 ‘ 𝑥 ) ↔ 𝑡 < ( 𝐺 ‘ 𝑧 ) ) )
94 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) )
95 94 breq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) )
96 95 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) )
97 93 96 bibi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑡 < ( 𝐺 ‘ 𝑥 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ↔ ( 𝑡 < ( 𝐺 ‘ 𝑧 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ) )
98 79 91 97 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑡 < ( 𝐺 ‘ 𝑥 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑡 < ( 𝐺 ‘ 𝑧 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) )
99 78 98 sylib ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ∀ 𝑧 ∈ 𝐴 ( 𝑡 < ( 𝐺 ‘ 𝑧 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) )
100 99 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑡 < ( 𝐺 ‘ 𝑧 ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) )
101 44 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐺 : 𝐴 ⟶ ℝ )
102 101 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
103 rexr ⊢ ( 𝑡 ∈ ℝ → 𝑡 ∈ ℝ* )
104 103 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑡 ∈ ℝ* )
105 elioopnf ⊢ ( 𝑡 ∈ ℝ* → ( ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ↔ ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ 𝑡 < ( 𝐺 ‘ 𝑧 ) ) ) )
106 104 105 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ↔ ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ 𝑡 < ( 𝐺 ‘ 𝑧 ) ) ) )
107 102 106 mpbirand ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ↔ 𝑡 < ( 𝐺 ‘ 𝑧 ) ) )
108 104 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑡 ∈ ℝ* )
109 elioopnf ⊢ ( 𝑡 ∈ ℝ* → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ) )
110 108 109 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ) )
111 7 fmpttd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
112 111 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ℝ )
113 112 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ) )
114 113 an32s ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ) )
115 114 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ) )
116 110 115 bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ↔ 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) )
117 116 rexbidva ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑛 ∈ 𝑍 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ↔ ∃ 𝑛 ∈ 𝑍 𝑡 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) )
118 100 107 117 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ↔ ∃ 𝑛 ∈ 𝑍 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) )
119 118 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑛 ∈ 𝑍 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
120 44 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
121 120 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝐺 Fn 𝐴 )
122 elpreima ⊢ ( 𝐺 Fn 𝐴 → ( 𝑧 ∈ ( ◡ 𝐺 “ ( 𝑡 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
123 121 122 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ 𝐺 “ ( 𝑡 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
124 eliun ⊢ ( 𝑧 ∈ ∪ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ↔ ∃ 𝑛 ∈ 𝑍 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) )
125 111 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
126 elpreima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 → ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
127 125 126 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
128 127 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ↔ ∃ 𝑛 ∈ 𝑍 ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
129 128 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ∃ 𝑛 ∈ 𝑍 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ↔ ∃ 𝑛 ∈ 𝑍 ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
130 r19.42v ⊢ ( ∃ 𝑛 ∈ 𝑍 ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑛 ∈ 𝑍 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) )
131 129 130 bitrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ∃ 𝑛 ∈ 𝑍 𝑧 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑛 ∈ 𝑍 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
132 124 131 syl5bb ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑧 ∈ ∪ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑛 ∈ 𝑍 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ( 𝑡 (,) +∞ ) ) ) )
133 119 123 132 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ 𝐺 “ ( 𝑡 (,) +∞ ) ) ↔ 𝑧 ∈ ∪ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ) )
134 133 eqrdv ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ◡ 𝐺 “ ( 𝑡 (,) +∞ ) ) = ∪ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) )
135 zex ⊢ ℤ ∈ V
136 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
137 ssdomg ⊢ ( ℤ ∈ V → ( ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ → ( ℤ≥ ‘ 𝑀 ) ≼ ℤ ) )
138 135 136 137 mp2 ⊢ ( ℤ≥ ‘ 𝑀 ) ≼ ℤ
139 1 138 eqbrtri ⊢ 𝑍 ≼ ℤ
140 znnen ⊢ ℤ ≈ ℕ
141 domentr ⊢ ( ( 𝑍 ≼ ℤ ∧ ℤ ≈ ℕ ) → 𝑍 ≼ ℕ )
142 139 140 141 mp2an ⊢ 𝑍 ≼ ℕ
143 mbfima ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ∈ dom vol )
144 4 111 143 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ∈ dom vol )
145 144 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ∈ dom vol )
146 145 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ∈ dom vol )
147 iunmbl2 ⊢ ( ( 𝑍 ≼ ℕ ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ∈ dom vol ) → ∪ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ∈ dom vol )
148 142 146 147 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ∪ 𝑛 ∈ 𝑍 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑡 (,) +∞ ) ) ∈ dom vol )
149 134 148 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( ◡ 𝐺 “ ( 𝑡 (,) +∞ ) ) ∈ dom vol )
150 44 149 ismbf3d ⊢ ( 𝜑 → 𝐺 ∈ MblFn )