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 syl5eq ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ - 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 )