Metamath Proof Explorer


Theorem mbfinf

Description: The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 13-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 mbfinf.1 𝑍 = ( ℤ𝑀 )
2 mbfinf.2 𝐺 = ( 𝑥𝐴 ↦ inf ( ran ( 𝑛𝑍𝐵 ) , ℝ , < ) )
3 mbfinf.3 ( 𝜑𝑀 ∈ ℤ )
4 mbfinf.4 ( ( 𝜑𝑛𝑍 ) → ( 𝑥𝐴𝐵 ) ∈ MblFn )
5 mbfinf.5 ( ( 𝜑 ∧ ( 𝑛𝑍𝑥𝐴 ) ) → 𝐵 ∈ ℝ )
6 mbfinf.6 ( ( 𝜑𝑥𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛𝑍 𝑦𝐵 )
7 5 anass1rs ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑛𝑍 ) → 𝐵 ∈ ℝ )
8 7 fmpttd ( ( 𝜑𝑥𝐴 ) → ( 𝑛𝑍𝐵 ) : 𝑍 ⟶ ℝ )
9 8 frnd ( ( 𝜑𝑥𝐴 ) → ran ( 𝑛𝑍𝐵 ) ⊆ ℝ )
10 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
11 3 10 syl ( 𝜑𝑀 ∈ ( ℤ𝑀 ) )
12 11 1 eleqtrrdi ( 𝜑𝑀𝑍 )
13 12 adantr ( ( 𝜑𝑥𝐴 ) → 𝑀𝑍 )
14 eqid ( 𝑛𝑍𝐵 ) = ( 𝑛𝑍𝐵 )
15 14 7 dmmptd ( ( 𝜑𝑥𝐴 ) → dom ( 𝑛𝑍𝐵 ) = 𝑍 )
16 13 15 eleqtrrd ( ( 𝜑𝑥𝐴 ) → 𝑀 ∈ dom ( 𝑛𝑍𝐵 ) )
17 16 ne0d ( ( 𝜑𝑥𝐴 ) → dom ( 𝑛𝑍𝐵 ) ≠ ∅ )
18 dm0rn0 ( dom ( 𝑛𝑍𝐵 ) = ∅ ↔ ran ( 𝑛𝑍𝐵 ) = ∅ )
19 18 necon3bii ( dom ( 𝑛𝑍𝐵 ) ≠ ∅ ↔ ran ( 𝑛𝑍𝐵 ) ≠ ∅ )
20 17 19 sylib ( ( 𝜑𝑥𝐴 ) → ran ( 𝑛𝑍𝐵 ) ≠ ∅ )
21 8 ffnd ( ( 𝜑𝑥𝐴 ) → ( 𝑛𝑍𝐵 ) Fn 𝑍 )
22 breq2 ( 𝑧 = ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) → ( 𝑦𝑧𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) ) )
23 22 ralrn ( ( 𝑛𝑍𝐵 ) Fn 𝑍 → ( ∀ 𝑧 ∈ ran ( 𝑛𝑍𝐵 ) 𝑦𝑧 ↔ ∀ 𝑚𝑍 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) ) )
24 21 23 syl ( ( 𝜑𝑥𝐴 ) → ( ∀ 𝑧 ∈ ran ( 𝑛𝑍𝐵 ) 𝑦𝑧 ↔ ∀ 𝑚𝑍 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) ) )
25 nfcv 𝑛 𝑦
26 nfcv 𝑛
27 nffvmpt1 𝑛 ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 )
28 25 26 27 nfbr 𝑛 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 )
29 nfv 𝑚 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 )
30 fveq2 ( 𝑚 = 𝑛 → ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) )
31 30 breq2d ( 𝑚 = 𝑛 → ( 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) ↔ 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) ) )
32 28 29 31 cbvralw ( ∀ 𝑚𝑍 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) ↔ ∀ 𝑛𝑍 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) )
33 simpr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑛𝑍 ) → 𝑛𝑍 )
34 14 fvmpt2 ( ( 𝑛𝑍𝐵 ∈ ℝ ) → ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = 𝐵 )
35 33 7 34 syl2anc ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑛𝑍 ) → ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = 𝐵 )
36 35 breq2d ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑛𝑍 ) → ( 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) ↔ 𝑦𝐵 ) )
37 36 ralbidva ( ( 𝜑𝑥𝐴 ) → ( ∀ 𝑛𝑍 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) ↔ ∀ 𝑛𝑍 𝑦𝐵 ) )
38 32 37 syl5bb ( ( 𝜑𝑥𝐴 ) → ( ∀ 𝑚𝑍 𝑦 ≤ ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) ↔ ∀ 𝑛𝑍 𝑦𝐵 ) )
39 24 38 bitrd ( ( 𝜑𝑥𝐴 ) → ( ∀ 𝑧 ∈ ran ( 𝑛𝑍𝐵 ) 𝑦𝑧 ↔ ∀ 𝑛𝑍 𝑦𝐵 ) )
40 39 rexbidv ( ( 𝜑𝑥𝐴 ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛𝑍𝐵 ) 𝑦𝑧 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑛𝑍 𝑦𝐵 ) )
41 6 40 mpbird ( ( 𝜑𝑥𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛𝑍𝐵 ) 𝑦𝑧 )
42 infrenegsup ( ( ran ( 𝑛𝑍𝐵 ) ⊆ ℝ ∧ ran ( 𝑛𝑍𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛𝑍𝐵 ) 𝑦𝑧 ) → inf ( ran ( 𝑛𝑍𝐵 ) , ℝ , < ) = - sup ( { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } , ℝ , < ) )
43 9 20 41 42 syl3anc ( ( 𝜑𝑥𝐴 ) → inf ( ran ( 𝑛𝑍𝐵 ) , ℝ , < ) = - sup ( { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } , ℝ , < ) )
44 rabid ( 𝑟 ∈ { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } ↔ ( 𝑟 ∈ ℝ ∧ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) ) )
45 7 recnd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑛𝑍 ) → 𝐵 ∈ ℂ )
46 45 adantlr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → 𝐵 ∈ ℂ )
47 simplr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → 𝑟 ∈ ℝ )
48 47 recnd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → 𝑟 ∈ ℂ )
49 negcon2 ( ( 𝐵 ∈ ℂ ∧ 𝑟 ∈ ℂ ) → ( 𝐵 = - 𝑟𝑟 = - 𝐵 ) )
50 46 48 49 syl2anc ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → ( 𝐵 = - 𝑟𝑟 = - 𝐵 ) )
51 eqcom ( 𝑟 = - 𝐵 ↔ - 𝐵 = 𝑟 )
52 50 51 bitrdi ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → ( 𝐵 = - 𝑟 ↔ - 𝐵 = 𝑟 ) )
53 35 adantlr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = 𝐵 )
54 53 eqeq1d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = - 𝑟𝐵 = - 𝑟 ) )
55 negex - 𝐵 ∈ V
56 eqid ( 𝑛𝑍 ↦ - 𝐵 ) = ( 𝑛𝑍 ↦ - 𝐵 )
57 56 fvmpt2 ( ( 𝑛𝑍 ∧ - 𝐵 ∈ V ) → ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = - 𝐵 )
58 55 57 mpan2 ( 𝑛𝑍 → ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = - 𝐵 )
59 58 adantl ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = - 𝐵 )
60 59 eqeq1d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → ( ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = 𝑟 ↔ - 𝐵 = 𝑟 ) )
61 52 54 60 3bitr4d ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑛𝑍 ) → ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = 𝑟 ) )
62 61 ralrimiva ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ∀ 𝑛𝑍 ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = 𝑟 ) )
63 27 nfeq1 𝑛 ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟
64 nffvmpt1 𝑛 ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 )
65 64 nfeq1 𝑛 ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟
66 63 65 nfbi 𝑛 ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 )
67 nfv 𝑚 ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = 𝑟 )
68 fveqeq2 ( 𝑚 = 𝑛 → ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ↔ ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = - 𝑟 ) )
69 fveqeq2 ( 𝑚 = 𝑛 → ( ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = 𝑟 ) )
70 68 69 bibi12d ( 𝑚 = 𝑛 → ( ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 ) ↔ ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = 𝑟 ) ) )
71 66 67 70 cbvralw ( ∀ 𝑚𝑍 ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 ) ↔ ∀ 𝑛𝑍 ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑛 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑛 ) = 𝑟 ) )
72 62 71 sylibr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ∀ 𝑚𝑍 ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 ) )
73 72 r19.21bi ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑚𝑍 ) → ( ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ↔ ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 ) )
74 73 rexbidva ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ( ∃ 𝑚𝑍 ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ↔ ∃ 𝑚𝑍 ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 ) )
75 21 adantr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ( 𝑛𝑍𝐵 ) Fn 𝑍 )
76 fvelrnb ( ( 𝑛𝑍𝐵 ) Fn 𝑍 → ( - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) ↔ ∃ 𝑚𝑍 ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ) )
77 75 76 syl ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ( - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) ↔ ∃ 𝑚𝑍 ( ( 𝑛𝑍𝐵 ) ‘ 𝑚 ) = - 𝑟 ) )
78 7 renegcld ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑛𝑍 ) → - 𝐵 ∈ ℝ )
79 78 fmpttd ( ( 𝜑𝑥𝐴 ) → ( 𝑛𝑍 ↦ - 𝐵 ) : 𝑍 ⟶ ℝ )
80 79 adantr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ( 𝑛𝑍 ↦ - 𝐵 ) : 𝑍 ⟶ ℝ )
81 80 ffnd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ( 𝑛𝑍 ↦ - 𝐵 ) Fn 𝑍 )
82 fvelrnb ( ( 𝑛𝑍 ↦ - 𝐵 ) Fn 𝑍 → ( 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ↔ ∃ 𝑚𝑍 ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 ) )
83 81 82 syl ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ( 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ↔ ∃ 𝑚𝑍 ( ( 𝑛𝑍 ↦ - 𝐵 ) ‘ 𝑚 ) = 𝑟 ) )
84 74 77 83 3bitr4d ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑟 ∈ ℝ ) → ( - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) ↔ 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ) )
85 84 pm5.32da ( ( 𝜑𝑥𝐴 ) → ( ( 𝑟 ∈ ℝ ∧ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) ) ↔ ( 𝑟 ∈ ℝ ∧ 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ) ) )
86 79 frnd ( ( 𝜑𝑥𝐴 ) → ran ( 𝑛𝑍 ↦ - 𝐵 ) ⊆ ℝ )
87 86 sseld ( ( 𝜑𝑥𝐴 ) → ( 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) → 𝑟 ∈ ℝ ) )
88 87 pm4.71rd ( ( 𝜑𝑥𝐴 ) → ( 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ↔ ( 𝑟 ∈ ℝ ∧ 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ) ) )
89 85 88 bitr4d ( ( 𝜑𝑥𝐴 ) → ( ( 𝑟 ∈ ℝ ∧ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) ) ↔ 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ) )
90 44 89 syl5bb ( ( 𝜑𝑥𝐴 ) → ( 𝑟 ∈ { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } ↔ 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ) )
91 90 alrimiv ( ( 𝜑𝑥𝐴 ) → ∀ 𝑟 ( 𝑟 ∈ { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } ↔ 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ) )
92 nfrab1 𝑟 { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) }
93 nfcv 𝑟 ran ( 𝑛𝑍 ↦ - 𝐵 )
94 92 93 cleqf ( { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } = ran ( 𝑛𝑍 ↦ - 𝐵 ) ↔ ∀ 𝑟 ( 𝑟 ∈ { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } ↔ 𝑟 ∈ ran ( 𝑛𝑍 ↦ - 𝐵 ) ) )
95 91 94 sylibr ( ( 𝜑𝑥𝐴 ) → { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } = ran ( 𝑛𝑍 ↦ - 𝐵 ) )
96 95 supeq1d ( ( 𝜑𝑥𝐴 ) → sup ( { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } , ℝ , < ) = sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) )
97 96 negeqd ( ( 𝜑𝑥𝐴 ) → - sup ( { 𝑟 ∈ ℝ ∣ - 𝑟 ∈ ran ( 𝑛𝑍𝐵 ) } , ℝ , < ) = - sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) )
98 43 97 eqtrd ( ( 𝜑𝑥𝐴 ) → inf ( ran ( 𝑛𝑍𝐵 ) , ℝ , < ) = - sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) )
99 98 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ inf ( ran ( 𝑛𝑍𝐵 ) , ℝ , < ) ) = ( 𝑥𝐴 ↦ - sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) ) )
100 2 99 eqtrid ( 𝜑𝐺 = ( 𝑥𝐴 ↦ - sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) ) )
101 ltso < Or ℝ
102 101 supex sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) ∈ V
103 102 a1i ( ( 𝜑𝑥𝐴 ) → sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) ∈ V )
104 eqid ( 𝑥𝐴 ↦ sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) ) = ( 𝑥𝐴 ↦ sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) )
105 5 anassrs ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
106 105 4 mbfneg ( ( 𝜑𝑛𝑍 ) → ( 𝑥𝐴 ↦ - 𝐵 ) ∈ MblFn )
107 5 renegcld ( ( 𝜑 ∧ ( 𝑛𝑍𝑥𝐴 ) ) → - 𝐵 ∈ ℝ )
108 renegcl ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
109 108 ad2antrl ( ( ( 𝜑𝑥𝐴 ) ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑛𝑍 𝑦𝐵 ) ) → - 𝑦 ∈ ℝ )
110 simplr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑛𝑍 ) → 𝑦 ∈ ℝ )
111 7 adantlr ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑛𝑍 ) → 𝐵 ∈ ℝ )
112 110 111 lenegd ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑛𝑍 ) → ( 𝑦𝐵 ↔ - 𝐵 ≤ - 𝑦 ) )
113 112 ralbidva ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑛𝑍 𝑦𝐵 ↔ ∀ 𝑛𝑍 - 𝐵 ≤ - 𝑦 ) )
114 113 biimpd ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑛𝑍 𝑦𝐵 → ∀ 𝑛𝑍 - 𝐵 ≤ - 𝑦 ) )
115 114 impr ( ( ( 𝜑𝑥𝐴 ) ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑛𝑍 𝑦𝐵 ) ) → ∀ 𝑛𝑍 - 𝐵 ≤ - 𝑦 )
116 brralrspcev ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑛𝑍 - 𝐵 ≤ - 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛𝑍 - 𝐵𝑧 )
117 109 115 116 syl2anc ( ( ( 𝜑𝑥𝐴 ) ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑛𝑍 𝑦𝐵 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛𝑍 - 𝐵𝑧 )
118 6 117 rexlimddv ( ( 𝜑𝑥𝐴 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛𝑍 - 𝐵𝑧 )
119 1 104 3 106 107 118 mbfsup ( 𝜑 → ( 𝑥𝐴 ↦ sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) ) ∈ MblFn )
120 103 119 mbfneg ( 𝜑 → ( 𝑥𝐴 ↦ - sup ( ran ( 𝑛𝑍 ↦ - 𝐵 ) , ℝ , < ) ) ∈ MblFn )
121 100 120 eqeltrd ( 𝜑𝐺 ∈ MblFn )