Metamath Proof Explorer

Theorem smfinflem

Description: The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfinflem.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smfinflem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smfinflem.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smfinflem.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
smfinflem.d ⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
smfinflem.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
Assertion smfinflem ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 smfinflem.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 smfinflem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 smfinflem.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 smfinflem.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5 smfinflem.d ⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
6 smfinflem.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
7 6 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
8 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐷 )
9 1 2 uzn0d ⊢ ( 𝜑 → 𝑍 ≠ ∅ )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑍 ≠ ∅ )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
12 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) )
13 eqid ⊢ dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑛 )
14 11 12 13 smff ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
15 14 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
16 ssrab2 ⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ⊆ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
17 5 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
18 17 biimpi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
19 16 18 sselid ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
20 19 adantr ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
21 simpr ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
22 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
23 20 21 22 syl2anc ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
24 23 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
25 15 24 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
26 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
27 18 26 syl ⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
29 8 10 25 28 infnsuprnmpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = - sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
30 29 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑥 ∈ 𝐷 ↦ - sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
31 7 30 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ - sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
32 nfv ⊢ Ⅎ 𝑥 𝜑
33 fvex ⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
34 33 dmex ⊢ dom ( 𝐹 ‘ 𝑛 ) ∈ V
35 34 rgenw ⊢ ∀ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∈ V
36 35 a1i ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∈ V )
37 9 36 iinexd ⊢ ( 𝜑 → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∈ V )
38 5 37 rabexd ⊢ ( 𝜑 → 𝐷 ∈ V )
39 25 renegcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
40 fveq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
41 40 breq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
42 41 ralbidv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
43 42 rexbidv ⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
44 nfcv ⊢ Ⅎ 𝑤 ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
45 nfcv ⊢ Ⅎ 𝑥 𝑍
46 nfcv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
47 46 nfdm ⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑚 )
48 45 47 nfiin ⊢ Ⅎ 𝑥 ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 )
49 nfv ⊢ Ⅎ 𝑤 ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 )
50 nfv ⊢ Ⅎ 𝑥 ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
51 nfcv ⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑛 )
52 nfcv ⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑚 )
53 52 nfdm ⊢ Ⅎ 𝑛 dom ( 𝐹 ‘ 𝑚 )
54 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
55 54 dmeqd ⊢ ( 𝑛 = 𝑚 → dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑚 ) )
56 51 53 55 cbviin ⊢ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) = ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 )
57 56 a1i ⊢ ( 𝑥 = 𝑤 → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) = ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) )
58 fveq2 ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) )
59 58 breq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) )
60 59 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) )
61 nfv ⊢ Ⅎ 𝑚 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 )
62 nfcv ⊢ Ⅎ 𝑛 𝑦
63 nfcv ⊢ Ⅎ 𝑛 ≤
64 nfcv ⊢ Ⅎ 𝑛 𝑤
65 52 64 nffv ⊢ Ⅎ 𝑛 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
66 62 63 65 nfbr ⊢ Ⅎ 𝑛 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
67 54 fveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
68 67 breq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ↔ 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
69 61 66 68 cbvralw ⊢ ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
70 69 a1i ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
71 60 70 bitrd ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
72 71 rexbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
73 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
74 73 ralbidv ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
75 74 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
76 75 a1i ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
77 72 76 bitrd ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
78 44 48 49 50 57 77 cbvrabcsfw ⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } = { 𝑤 ∈ ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) }
79 5 78 eqtri ⊢ 𝐷 = { 𝑤 ∈ ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) }
80 43 79 elrab2 ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
81 80 biimpi ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
82 81 simprd ⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
84 renegcl ⊢ ( 𝑧 ∈ ℝ → - 𝑧 ∈ ℝ )
85 84 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) → - 𝑧 ∈ ℝ )
86 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
87 86 fveq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
88 87 breq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ↔ 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
89 88 rspcva ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) → 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
90 89 ancoms ⊢ ( ( ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
91 90 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
92 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑧 ∈ ℝ )
93 25 ad4ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
94 92 93 lenegd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑧 ) )
95 91 94 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑧 )
96 95 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) → ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑧 )
97 brralrspcev ⊢ ( ( - 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑧 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
98 85 96 97 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
99 98 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
100 83 99 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
101 8 10 39 100 suprclrnmpt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ℝ )
102 5 a1i ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
103 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
104 nfv ⊢ Ⅎ 𝑦 ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧
105 renegcl ⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
106 105 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → - 𝑦 ∈ ℝ )
107 nfv ⊢ Ⅎ 𝑛 𝜑
108 nfcv ⊢ Ⅎ 𝑛 𝑥
109 nfii1 ⊢ Ⅎ 𝑛 ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
110 108 109 nfel ⊢ Ⅎ 𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
111 107 110 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
112 62 nfel1 ⊢ Ⅎ 𝑛 𝑦 ∈ ℝ
113 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 )
114 111 112 113 nf3an ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
115 simpl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ )
116 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
117 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
118 22 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
119 14 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
120 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
121 119 120 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
122 116 117 118 121 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
123 122 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
124 rspa ⊢ ( ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
125 124 3ad2antl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
126 leneg ⊢ ( ( 𝑦 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑦 ) )
127 126 biimp3a ⊢ ( ( 𝑦 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑦 )
128 115 123 125 127 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑦 )
129 128 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → ( 𝑛 ∈ 𝑍 → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑦 ) )
130 114 129 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑦 )
131 brralrspcev ⊢ ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ - 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 )
132 106 130 131 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 )
133 132 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → ( 𝑦 ∈ ℝ → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) ) )
134 103 104 133 rexlimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) )
135 84 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → - 𝑧 ∈ ℝ )
136 nfv ⊢ Ⅎ 𝑛 𝑧 ∈ ℝ
137 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧
138 111 136 137 nf3an ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 )
139 122 3ad2antl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
140 simpl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑧 ∈ ℝ )
141 rspa ⊢ ( ( ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ∧ 𝑛 ∈ 𝑍 ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 )
142 141 3ad2antl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) ∧ 𝑛 ∈ 𝑍 ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 )
143 simp3 ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 )
144 renegcl ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
145 144 adantr ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
146 simpr ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ )
147 leneg ⊢ ( ( - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ↔ - 𝑧 ≤ - - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
148 145 146 147 syl2anc ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ↔ - 𝑧 ≤ - - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
149 148 3adant3 ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → ( - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ↔ - 𝑧 ≤ - - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
150 143 149 mpbid ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → - 𝑧 ≤ - - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
151 recn ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
152 151 negnegd ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ → - - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
153 152 3ad2ant1 ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → - - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
154 150 153 breqtrd ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → - 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
155 139 140 142 154 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
156 155 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → ( 𝑛 ∈ 𝑍 → - 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
157 138 156 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → ∀ 𝑛 ∈ 𝑍 - 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
158 breq1 ⊢ ( 𝑦 = - 𝑧 → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ - 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
159 158 ralbidv ⊢ ( 𝑦 = - 𝑧 → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑍 - 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
160 159 rspcev ⊢ ( ( - 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - 𝑧 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
161 135 157 160 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑧 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
162 161 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → ( 𝑧 ∈ ℝ → ( ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ) )
163 162 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → ( ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
164 134 163 impbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 ) )
165 32 164 rabbida ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } )
166 102 165 eqtrd ⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } )
167 32 166 alrimi ⊢ ( 𝜑 → ∀ 𝑥 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } )
168 eqid ⊢ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < )
169 168 rgenw ⊢ ∀ 𝑥 ∈ 𝐷 sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < )
170 169 a1i ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
171 mpteq12f ⊢ ( ( ∀ 𝑥 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } ∧ ∀ 𝑥 ∈ 𝐷 sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) → ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
172 167 170 171 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
173 nfv ⊢ Ⅎ 𝑧 𝜑
174 121 renegcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
175 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
176 34 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom ( 𝐹 ‘ 𝑛 ) ∈ V )
177 121 3expa ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
178 14 feqmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
179 178 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑛 ) )
180 179 12 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
181 175 11 176 177 180 smfneg ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
182 eqid ⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 }
183 eqid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
184 107 32 173 1 2 3 174 181 182 183 smfsupmpt ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ 𝑍 - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑧 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) ∈ ( SMblFn ‘ 𝑆 ) )
185 172 184 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) ∈ ( SMblFn ‘ 𝑆 ) )
186 32 3 38 101 185 smfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ - sup ( ran ( 𝑛 ∈ 𝑍 ↦ - ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) ∈ ( SMblFn ‘ 𝑆 ) )
187 31 186 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )