Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smfinflem Structured version   Visualization version   GIF version

Theorem smfinflem 46837
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.)
Hypotheses
Ref Expression
smfinflem.m (𝜑𝑀 ∈ ℤ)
smfinflem.z 𝑍 = (ℤ𝑀)
smfinflem.s (𝜑𝑆 ∈ SAlg)
smfinflem.f (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
smfinflem.d 𝐷 = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)}
smfinflem.g 𝐺 = (𝑥𝐷 ↦ inf(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
Assertion
Ref Expression
smfinflem (𝜑𝐺 ∈ (SMblFn‘𝑆))
Distinct variable groups:   𝐷,𝑛,𝑥,𝑦   𝑛,𝐹,𝑥,𝑦   𝑆,𝑛   𝑛,𝑍,𝑥,𝑦   𝜑,𝑛,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦)   𝐺(𝑥,𝑦,𝑛)   𝑀(𝑥,𝑦,𝑛)

Proof of Theorem smfinflem
Dummy variables 𝑚 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smfinflem.g . . . 4 𝐺 = (𝑥𝐷 ↦ inf(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ))
21a1i 11 . . 3 (𝜑𝐺 = (𝑥𝐷 ↦ inf(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < )))
3 nfv 1913 . . . . 5 𝑛(𝜑𝑥𝐷)
4 smfinflem.m . . . . . . 7 (𝜑𝑀 ∈ ℤ)
5 smfinflem.z . . . . . . 7 𝑍 = (ℤ𝑀)
64, 5uzn0d 45441 . . . . . 6 (𝜑𝑍 ≠ ∅)
76adantr 480 . . . . 5 ((𝜑𝑥𝐷) → 𝑍 ≠ ∅)
8 smfinflem.s . . . . . . . . 9 (𝜑𝑆 ∈ SAlg)
98adantr 480 . . . . . . . 8 ((𝜑𝑛𝑍) → 𝑆 ∈ SAlg)
10 smfinflem.f . . . . . . . . 9 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
1110ffvelcdmda 7103 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ (SMblFn‘𝑆))
12 eqid 2736 . . . . . . . 8 dom (𝐹𝑛) = dom (𝐹𝑛)
139, 11, 12smff 46752 . . . . . . 7 ((𝜑𝑛𝑍) → (𝐹𝑛):dom (𝐹𝑛)⟶ℝ)
1413adantlr 715 . . . . . 6 (((𝜑𝑥𝐷) ∧ 𝑛𝑍) → (𝐹𝑛):dom (𝐹𝑛)⟶ℝ)
15 ssrab2 4079 . . . . . . . . . 10 {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)} ⊆ 𝑛𝑍 dom (𝐹𝑛)
16 smfinflem.d . . . . . . . . . . . 12 𝐷 = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)}
1716eleq2i 2832 . . . . . . . . . . 11 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)})
1817biimpi 216 . . . . . . . . . 10 (𝑥𝐷𝑥 ∈ {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)})
1915, 18sselid 3980 . . . . . . . . 9 (𝑥𝐷𝑥 𝑛𝑍 dom (𝐹𝑛))
2019adantr 480 . . . . . . . 8 ((𝑥𝐷𝑛𝑍) → 𝑥 𝑛𝑍 dom (𝐹𝑛))
21 simpr 484 . . . . . . . 8 ((𝑥𝐷𝑛𝑍) → 𝑛𝑍)
22 eliinid 45121 . . . . . . . 8 ((𝑥 𝑛𝑍 dom (𝐹𝑛) ∧ 𝑛𝑍) → 𝑥 ∈ dom (𝐹𝑛))
2320, 21, 22syl2anc 584 . . . . . . 7 ((𝑥𝐷𝑛𝑍) → 𝑥 ∈ dom (𝐹𝑛))
2423adantll 714 . . . . . 6 (((𝜑𝑥𝐷) ∧ 𝑛𝑍) → 𝑥 ∈ dom (𝐹𝑛))
2514, 24ffvelcdmd 7104 . . . . 5 (((𝜑𝑥𝐷) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
26 rabidim2 45112 . . . . . . 7 (𝑥 ∈ {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)} → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥))
2718, 26syl 17 . . . . . 6 (𝑥𝐷 → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥))
2827adantl 481 . . . . 5 ((𝜑𝑥𝐷) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥))
293, 7, 25, 28infnsuprnmpt 45262 . . . 4 ((𝜑𝑥𝐷) → inf(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < ) = -sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < ))
3029mpteq2dva 5241 . . 3 (𝜑 → (𝑥𝐷 ↦ inf(ran (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑥)), ℝ, < )) = (𝑥𝐷 ↦ -sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )))
312, 30eqtrd 2776 . 2 (𝜑𝐺 = (𝑥𝐷 ↦ -sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )))
32 nfv 1913 . . 3 𝑥𝜑
33 fvex 6918 . . . . . . . 8 (𝐹𝑛) ∈ V
3433dmex 7932 . . . . . . 7 dom (𝐹𝑛) ∈ V
3534rgenw 3064 . . . . . 6 𝑛𝑍 dom (𝐹𝑛) ∈ V
3635a1i 11 . . . . 5 (𝜑 → ∀𝑛𝑍 dom (𝐹𝑛) ∈ V)
376, 36iinexd 45143 . . . 4 (𝜑 𝑛𝑍 dom (𝐹𝑛) ∈ V)
3816, 37rabexd 5339 . . 3 (𝜑𝐷 ∈ V)
3925renegcld 11691 . . . 4 (((𝜑𝑥𝐷) ∧ 𝑛𝑍) → -((𝐹𝑛)‘𝑥) ∈ ℝ)
40 fveq2 6905 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝐹𝑚)‘𝑤) = ((𝐹𝑚)‘𝑥))
4140breq2d 5154 . . . . . . . . . . 11 (𝑤 = 𝑥 → (𝑧 ≤ ((𝐹𝑚)‘𝑤) ↔ 𝑧 ≤ ((𝐹𝑚)‘𝑥)))
4241ralbidv 3177 . . . . . . . . . 10 (𝑤 = 𝑥 → (∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤) ↔ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)))
4342rexbidv 3178 . . . . . . . . 9 (𝑤 = 𝑥 → (∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤) ↔ ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)))
44 nfcv 2904 . . . . . . . . . . 11 𝑤 𝑛𝑍 dom (𝐹𝑛)
45 nfcv 2904 . . . . . . . . . . . 12 𝑥𝑍
46 nfcv 2904 . . . . . . . . . . . . 13 𝑥(𝐹𝑚)
4746nfdm 5961 . . . . . . . . . . . 12 𝑥dom (𝐹𝑚)
4845, 47nfiin 5023 . . . . . . . . . . 11 𝑥 𝑚𝑍 dom (𝐹𝑚)
49 nfv 1913 . . . . . . . . . . 11 𝑤𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)
50 nfv 1913 . . . . . . . . . . 11 𝑥𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤)
51 nfcv 2904 . . . . . . . . . . . . 13 𝑚dom (𝐹𝑛)
52 nfcv 2904 . . . . . . . . . . . . . 14 𝑛(𝐹𝑚)
5352nfdm 5961 . . . . . . . . . . . . 13 𝑛dom (𝐹𝑚)
54 fveq2 6905 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
5554dmeqd 5915 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → dom (𝐹𝑛) = dom (𝐹𝑚))
5651, 53, 55cbviin 5036 . . . . . . . . . . . 12 𝑛𝑍 dom (𝐹𝑛) = 𝑚𝑍 dom (𝐹𝑚)
5756a1i 11 . . . . . . . . . . 11 (𝑥 = 𝑤 𝑛𝑍 dom (𝐹𝑛) = 𝑚𝑍 dom (𝐹𝑚))
58 fveq2 6905 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → ((𝐹𝑛)‘𝑥) = ((𝐹𝑛)‘𝑤))
5958breq2d 5154 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ 𝑦 ≤ ((𝐹𝑛)‘𝑤)))
6059ralbidv 3177 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑤)))
61 nfv 1913 . . . . . . . . . . . . . . . 16 𝑚 𝑦 ≤ ((𝐹𝑛)‘𝑤)
62 nfcv 2904 . . . . . . . . . . . . . . . . 17 𝑛𝑦
63 nfcv 2904 . . . . . . . . . . . . . . . . 17 𝑛
64 nfcv 2904 . . . . . . . . . . . . . . . . . 18 𝑛𝑤
6552, 64nffv 6915 . . . . . . . . . . . . . . . . 17 𝑛((𝐹𝑚)‘𝑤)
6662, 63, 65nfbr 5189 . . . . . . . . . . . . . . . 16 𝑛 𝑦 ≤ ((𝐹𝑚)‘𝑤)
6754fveq1d 6907 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → ((𝐹𝑛)‘𝑤) = ((𝐹𝑚)‘𝑤))
6867breq2d 5154 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → (𝑦 ≤ ((𝐹𝑛)‘𝑤) ↔ 𝑦 ≤ ((𝐹𝑚)‘𝑤)))
6961, 66, 68cbvralw 3305 . . . . . . . . . . . . . . 15 (∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑤) ↔ ∀𝑚𝑍 𝑦 ≤ ((𝐹𝑚)‘𝑤))
7069a1i 11 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑤) ↔ ∀𝑚𝑍 𝑦 ≤ ((𝐹𝑚)‘𝑤)))
7160, 70bitrd 279 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ ∀𝑚𝑍 𝑦 ≤ ((𝐹𝑚)‘𝑤)))
7271rexbidv 3178 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ ∃𝑦 ∈ ℝ ∀𝑚𝑍 𝑦 ≤ ((𝐹𝑚)‘𝑤)))
73 breq1 5145 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑦 ≤ ((𝐹𝑚)‘𝑤) ↔ 𝑧 ≤ ((𝐹𝑚)‘𝑤)))
7473ralbidv 3177 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (∀𝑚𝑍 𝑦 ≤ ((𝐹𝑚)‘𝑤) ↔ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤)))
7574cbvrexvw 3237 . . . . . . . . . . . . 13 (∃𝑦 ∈ ℝ ∀𝑚𝑍 𝑦 ≤ ((𝐹𝑚)‘𝑤) ↔ ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤))
7675a1i 11 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑚𝑍 𝑦 ≤ ((𝐹𝑚)‘𝑤) ↔ ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤)))
7772, 76bitrd 279 . . . . . . . . . . 11 (𝑥 = 𝑤 → (∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤)))
7844, 48, 49, 50, 57, 77cbvrabcsfw 3939 . . . . . . . . . 10 {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)} = {𝑤 𝑚𝑍 dom (𝐹𝑚) ∣ ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤)}
7916, 78eqtri 2764 . . . . . . . . 9 𝐷 = {𝑤 𝑚𝑍 dom (𝐹𝑚) ∣ ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑤)}
8043, 79elrab2 3694 . . . . . . . 8 (𝑥𝐷 ↔ (𝑥 𝑚𝑍 dom (𝐹𝑚) ∧ ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)))
8180biimpi 216 . . . . . . 7 (𝑥𝐷 → (𝑥 𝑚𝑍 dom (𝐹𝑚) ∧ ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)))
8281simprd 495 . . . . . 6 (𝑥𝐷 → ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥))
8382adantl 481 . . . . 5 ((𝜑𝑥𝐷) → ∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥))
84 renegcl 11573 . . . . . . . 8 (𝑧 ∈ ℝ → -𝑧 ∈ ℝ)
8584ad2antlr 727 . . . . . . 7 ((((𝜑𝑥𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) → -𝑧 ∈ ℝ)
86 fveq2 6905 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
8786fveq1d 6907 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑛)‘𝑥))
8887breq2d 5154 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (𝑧 ≤ ((𝐹𝑚)‘𝑥) ↔ 𝑧 ≤ ((𝐹𝑛)‘𝑥)))
8988rspcva 3619 . . . . . . . . . . 11 ((𝑛𝑍 ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) → 𝑧 ≤ ((𝐹𝑛)‘𝑥))
9089ancoms 458 . . . . . . . . . 10 ((∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥) ∧ 𝑛𝑍) → 𝑧 ≤ ((𝐹𝑛)‘𝑥))
9190adantll 714 . . . . . . . . 9 (((((𝜑𝑥𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) ∧ 𝑛𝑍) → 𝑧 ≤ ((𝐹𝑛)‘𝑥))
92 simpllr 775 . . . . . . . . . 10 (((((𝜑𝑥𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) ∧ 𝑛𝑍) → 𝑧 ∈ ℝ)
9325ad4ant14 752 . . . . . . . . . 10 (((((𝜑𝑥𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
9492, 93lenegd 11843 . . . . . . . . 9 (((((𝜑𝑥𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) ∧ 𝑛𝑍) → (𝑧 ≤ ((𝐹𝑛)‘𝑥) ↔ -((𝐹𝑛)‘𝑥) ≤ -𝑧))
9591, 94mpbid 232 . . . . . . . 8 (((((𝜑𝑥𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) ∧ 𝑛𝑍) → -((𝐹𝑛)‘𝑥) ≤ -𝑧)
9695ralrimiva 3145 . . . . . . 7 ((((𝜑𝑥𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) → ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ -𝑧)
97 brralrspcev 5202 . . . . . . 7 ((-𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ -𝑧) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑦)
9885, 96, 97syl2anc 584 . . . . . 6 ((((𝜑𝑥𝐷) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥)) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑦)
9998rexlimdva2 3156 . . . . 5 ((𝜑𝑥𝐷) → (∃𝑧 ∈ ℝ ∀𝑚𝑍 𝑧 ≤ ((𝐹𝑚)‘𝑥) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑦))
10083, 99mpd 15 . . . 4 ((𝜑𝑥𝐷) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑦)
1013, 7, 39, 100suprclrnmpt 45263 . . 3 ((𝜑𝑥𝐷) → sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < ) ∈ ℝ)
10216a1i 11 . . . . . . 7 (𝜑𝐷 = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)})
103 nfv 1913 . . . . . . . . . 10 𝑦(𝜑𝑥 𝑛𝑍 dom (𝐹𝑛))
104 nfv 1913 . . . . . . . . . 10 𝑦𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧
105 renegcl 11573 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
1061053ad2ant2 1134 . . . . . . . . . . . 12 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)) → -𝑦 ∈ ℝ)
107 nfv 1913 . . . . . . . . . . . . . . 15 𝑛𝜑
108 nfcv 2904 . . . . . . . . . . . . . . . 16 𝑛𝑥
109 nfii1 5028 . . . . . . . . . . . . . . . 16 𝑛 𝑛𝑍 dom (𝐹𝑛)
110108, 109nfel 2919 . . . . . . . . . . . . . . 15 𝑛 𝑥 𝑛𝑍 dom (𝐹𝑛)
111107, 110nfan 1898 . . . . . . . . . . . . . 14 𝑛(𝜑𝑥 𝑛𝑍 dom (𝐹𝑛))
11262nfel1 2921 . . . . . . . . . . . . . 14 𝑛 𝑦 ∈ ℝ
113 nfra1 3283 . . . . . . . . . . . . . 14 𝑛𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)
114111, 112, 113nf3an 1900 . . . . . . . . . . . . 13 𝑛((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥))
115 simpl2 1192 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)) ∧ 𝑛𝑍) → 𝑦 ∈ ℝ)
116 simpll 766 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑛𝑍) → 𝜑)
117 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑛𝑍) → 𝑛𝑍)
11822adantll 714 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑛𝑍) → 𝑥 ∈ dom (𝐹𝑛))
119133adant3 1132 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍𝑥 ∈ dom (𝐹𝑛)) → (𝐹𝑛):dom (𝐹𝑛)⟶ℝ)
120 simp3 1138 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍𝑥 ∈ dom (𝐹𝑛)) → 𝑥 ∈ dom (𝐹𝑛))
121119, 120ffvelcdmd 7104 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍𝑥 ∈ dom (𝐹𝑛)) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
122116, 117, 118, 121syl3anc 1372 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
1231223ad2antl1 1185 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
124 rspa 3247 . . . . . . . . . . . . . . . 16 ((∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) ∧ 𝑛𝑍) → 𝑦 ≤ ((𝐹𝑛)‘𝑥))
1251243ad2antl3 1187 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)) ∧ 𝑛𝑍) → 𝑦 ≤ ((𝐹𝑛)‘𝑥))
126 leneg 11767 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℝ ∧ ((𝐹𝑛)‘𝑥) ∈ ℝ) → (𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ -((𝐹𝑛)‘𝑥) ≤ -𝑦))
127126biimp3a 1470 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ ∧ ((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑦 ≤ ((𝐹𝑛)‘𝑥)) → -((𝐹𝑛)‘𝑥) ≤ -𝑦)
128115, 123, 125, 127syl3anc 1372 . . . . . . . . . . . . . 14 ((((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)) ∧ 𝑛𝑍) → -((𝐹𝑛)‘𝑥) ≤ -𝑦)
129128ex 412 . . . . . . . . . . . . 13 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)) → (𝑛𝑍 → -((𝐹𝑛)‘𝑥) ≤ -𝑦))
130114, 129ralrimi 3256 . . . . . . . . . . . 12 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)) → ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ -𝑦)
131 brralrspcev 5202 . . . . . . . . . . . 12 ((-𝑦 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ -𝑦) → ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧)
132106, 130, 131syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑦 ∈ ℝ ∧ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)) → ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧)
1331323exp 1119 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) → (𝑦 ∈ ℝ → (∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) → ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧)))
134103, 104, 133rexlimd 3265 . . . . . . . . 9 ((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) → (∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) → ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧))
135843ad2ant2 1134 . . . . . . . . . . . 12 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧) → -𝑧 ∈ ℝ)
136 nfv 1913 . . . . . . . . . . . . . 14 𝑛 𝑧 ∈ ℝ
137 nfra1 3283 . . . . . . . . . . . . . 14 𝑛𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧
138111, 136, 137nf3an 1900 . . . . . . . . . . . . 13 𝑛((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧)
1391223ad2antl1 1185 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
140 simpl2 1192 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧) ∧ 𝑛𝑍) → 𝑧 ∈ ℝ)
141 rspa 3247 . . . . . . . . . . . . . . . 16 ((∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧𝑛𝑍) → -((𝐹𝑛)‘𝑥) ≤ 𝑧)
1421413ad2antl3 1187 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧) ∧ 𝑛𝑍) → -((𝐹𝑛)‘𝑥) ≤ 𝑧)
143 simp3 1138 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹𝑛)‘𝑥) ≤ 𝑧) → -((𝐹𝑛)‘𝑥) ≤ 𝑧)
144 renegcl 11573 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑛)‘𝑥) ∈ ℝ → -((𝐹𝑛)‘𝑥) ∈ ℝ)
145144adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ) → -((𝐹𝑛)‘𝑥) ∈ ℝ)
146 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ)
147 leneg 11767 . . . . . . . . . . . . . . . . . . 19 ((-((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-((𝐹𝑛)‘𝑥) ≤ 𝑧 ↔ -𝑧 ≤ --((𝐹𝑛)‘𝑥)))
148145, 146, 147syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-((𝐹𝑛)‘𝑥) ≤ 𝑧 ↔ -𝑧 ≤ --((𝐹𝑛)‘𝑥)))
1491483adant3 1132 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹𝑛)‘𝑥) ≤ 𝑧) → (-((𝐹𝑛)‘𝑥) ≤ 𝑧 ↔ -𝑧 ≤ --((𝐹𝑛)‘𝑥)))
150143, 149mpbid 232 . . . . . . . . . . . . . . . 16 ((((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹𝑛)‘𝑥) ≤ 𝑧) → -𝑧 ≤ --((𝐹𝑛)‘𝑥))
151 recn 11246 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑛)‘𝑥) ∈ ℝ → ((𝐹𝑛)‘𝑥) ∈ ℂ)
152151negnegd 11612 . . . . . . . . . . . . . . . . 17 (((𝐹𝑛)‘𝑥) ∈ ℝ → --((𝐹𝑛)‘𝑥) = ((𝐹𝑛)‘𝑥))
1531523ad2ant1 1133 . . . . . . . . . . . . . . . 16 ((((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹𝑛)‘𝑥) ≤ 𝑧) → --((𝐹𝑛)‘𝑥) = ((𝐹𝑛)‘𝑥))
154150, 153breqtrd 5168 . . . . . . . . . . . . . . 15 ((((𝐹𝑛)‘𝑥) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ -((𝐹𝑛)‘𝑥) ≤ 𝑧) → -𝑧 ≤ ((𝐹𝑛)‘𝑥))
155139, 140, 142, 154syl3anc 1372 . . . . . . . . . . . . . 14 ((((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧) ∧ 𝑛𝑍) → -𝑧 ≤ ((𝐹𝑛)‘𝑥))
156155ex 412 . . . . . . . . . . . . 13 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧) → (𝑛𝑍 → -𝑧 ≤ ((𝐹𝑛)‘𝑥)))
157138, 156ralrimi 3256 . . . . . . . . . . . 12 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧) → ∀𝑛𝑍 -𝑧 ≤ ((𝐹𝑛)‘𝑥))
158 breq1 5145 . . . . . . . . . . . . . 14 (𝑦 = -𝑧 → (𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ -𝑧 ≤ ((𝐹𝑛)‘𝑥)))
159158ralbidv 3177 . . . . . . . . . . . . 13 (𝑦 = -𝑧 → (∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ ∀𝑛𝑍 -𝑧 ≤ ((𝐹𝑛)‘𝑥)))
160159rspcev 3621 . . . . . . . . . . . 12 ((-𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -𝑧 ≤ ((𝐹𝑛)‘𝑥)) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥))
161135, 157, 160syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) ∧ 𝑧 ∈ ℝ ∧ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥))
1621613exp 1119 . . . . . . . . . 10 ((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) → (𝑧 ∈ ℝ → (∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧 → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥))))
163162rexlimdv 3152 . . . . . . . . 9 ((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) → (∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧 → ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)))
164134, 163impbid 212 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 dom (𝐹𝑛)) → (∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥) ↔ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧))
16532, 164rabbida 3462 . . . . . . 7 (𝜑 → {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛𝑍 𝑦 ≤ ((𝐹𝑛)‘𝑥)} = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧})
166102, 165eqtrd 2776 . . . . . 6 (𝜑𝐷 = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧})
16732, 166alrimi 2212 . . . . 5 (𝜑 → ∀𝑥 𝐷 = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧})
168 eqid 2736 . . . . . . 7 sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )
169168rgenw 3064 . . . . . 6 𝑥𝐷 sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )
170169a1i 11 . . . . 5 (𝜑 → ∀𝑥𝐷 sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < ))
171 mpteq12f 5229 . . . . 5 ((∀𝑥 𝐷 = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧} ∧ ∀𝑥𝐷 sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < ) = sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )) → (𝑥𝐷 ↦ sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )) = (𝑥 ∈ {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )))
172167, 170, 171syl2anc 584 . . . 4 (𝜑 → (𝑥𝐷 ↦ sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )) = (𝑥 ∈ {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )))
173 nfv 1913 . . . . 5 𝑧𝜑
174121renegcld 11691 . . . . 5 ((𝜑𝑛𝑍𝑥 ∈ dom (𝐹𝑛)) → -((𝐹𝑛)‘𝑥) ∈ ℝ)
175 nfv 1913 . . . . . 6 𝑥(𝜑𝑛𝑍)
17634a1i 11 . . . . . 6 ((𝜑𝑛𝑍) → dom (𝐹𝑛) ∈ V)
1771213expa 1118 . . . . . 6 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ dom (𝐹𝑛)) → ((𝐹𝑛)‘𝑥) ∈ ℝ)
17813feqmptd 6976 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐹𝑛) = (𝑥 ∈ dom (𝐹𝑛) ↦ ((𝐹𝑛)‘𝑥)))
179178eqcomd 2742 . . . . . . 7 ((𝜑𝑛𝑍) → (𝑥 ∈ dom (𝐹𝑛) ↦ ((𝐹𝑛)‘𝑥)) = (𝐹𝑛))
180179, 11eqeltrd 2840 . . . . . 6 ((𝜑𝑛𝑍) → (𝑥 ∈ dom (𝐹𝑛) ↦ ((𝐹𝑛)‘𝑥)) ∈ (SMblFn‘𝑆))
181175, 9, 176, 177, 180smfneg 46823 . . . . 5 ((𝜑𝑛𝑍) → (𝑥 ∈ dom (𝐹𝑛) ↦ -((𝐹𝑛)‘𝑥)) ∈ (SMblFn‘𝑆))
182 eqid 2736 . . . . 5 {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧} = {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧}
183 eqid 2736 . . . . 5 (𝑥 ∈ {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )) = (𝑥 ∈ {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < ))
184107, 32, 173, 4, 5, 8, 174, 181, 182, 183smfsupmpt 46835 . . . 4 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 dom (𝐹𝑛) ∣ ∃𝑧 ∈ ℝ ∀𝑛𝑍 -((𝐹𝑛)‘𝑥) ≤ 𝑧} ↦ sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )) ∈ (SMblFn‘𝑆))
185172, 184eqeltrd 2840 . . 3 (𝜑 → (𝑥𝐷 ↦ sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )) ∈ (SMblFn‘𝑆))
18632, 8, 38, 101, 185smfneg 46823 . 2 (𝜑 → (𝑥𝐷 ↦ -sup(ran (𝑛𝑍 ↦ -((𝐹𝑛)‘𝑥)), ℝ, < )) ∈ (SMblFn‘𝑆))
18731, 186eqeltrd 2840 1 (𝜑𝐺 ∈ (SMblFn‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086  wal 1537   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069  {crab 3435  Vcvv 3479  c0 4332   ciin 4991   class class class wbr 5142  cmpt 5224  dom cdm 5684  ran crn 5685  wf 6556  cfv 6560  supcsup 9481  infcinf 9482  cr 11155   < clt 11296  cle 11297  -cneg 11494  cz 12615  cuz 12879  SAlgcsalg 46328  SMblFncsmblfn 46715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682  ax-cc 10476  ax-ac2 10504  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-oadd 8511  df-omul 8512  df-er 8746  df-map 8869  df-pm 8870  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-sup 9483  df-inf 9484  df-oi 9551  df-card 9980  df-acn 9983  df-ac 10157  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-n0 12529  df-z 12616  df-uz 12880  df-q 12992  df-rp 13036  df-ioo 13392  df-ioc 13393  df-ico 13394  df-icc 13395  df-fz 13549  df-fzo 13696  df-fl 13833  df-seq 14044  df-exp 14104  df-hash 14371  df-word 14554  df-concat 14610  df-s1 14635  df-s2 14888  df-s3 14889  df-s4 14890  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-rest 17468  df-topgen 17489  df-top 22901  df-bases 22954  df-salg 46329  df-salgen 46333  df-smblfn 46716
This theorem is referenced by:  smfinf  46838
  Copyright terms: Public domain W3C validator