# Metamath Proof Explorer

Description: For any small margin E , we can find a covering approaching the outer measure of a set A by that margin. (Contributed by Thierry Arnoux, 18-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses oms.m ${⊢}{M}=\mathrm{toOMeas}\left({R}\right)$
oms.o ${⊢}{\phi }\to {Q}\in {V}$
oms.r ${⊢}{\phi }\to {R}:{Q}⟶\left[0,\mathrm{+\infty }\right]$
omssubaddlem.a ${⊢}{\phi }\to {A}\subseteq \bigcup {Q}$
omssubaddlem.m ${⊢}{\phi }\to {M}\left({A}\right)\in ℝ$
omssubaddlem.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
Assertion omssubaddlem ${⊢}{\phi }\to \exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)<{M}\left({A}\right)+{E}$

### Proof

Step Hyp Ref Expression
1 oms.m ${⊢}{M}=\mathrm{toOMeas}\left({R}\right)$
2 oms.o ${⊢}{\phi }\to {Q}\in {V}$
3 oms.r ${⊢}{\phi }\to {R}:{Q}⟶\left[0,\mathrm{+\infty }\right]$
4 omssubaddlem.a ${⊢}{\phi }\to {A}\subseteq \bigcup {Q}$
5 omssubaddlem.m ${⊢}{\phi }\to {M}\left({A}\right)\in ℝ$
6 omssubaddlem.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
7 6 rpred ${⊢}{\phi }\to {E}\in ℝ$
8 5 7 readdcld ${⊢}{\phi }\to {M}\left({A}\right)+{E}\in ℝ$
9 8 rexrd ${⊢}{\phi }\to {M}\left({A}\right)+{E}\in {ℝ}^{*}$
10 omsf ${⊢}\left({Q}\in {V}\wedge {R}:{Q}⟶\left[0,\mathrm{+\infty }\right]\right)\to \mathrm{toOMeas}\left({R}\right):𝒫\bigcup \mathrm{dom}{R}⟶\left[0,\mathrm{+\infty }\right]$
11 2 3 10 syl2anc ${⊢}{\phi }\to \mathrm{toOMeas}\left({R}\right):𝒫\bigcup \mathrm{dom}{R}⟶\left[0,\mathrm{+\infty }\right]$
12 1 feq1i ${⊢}{M}:𝒫\bigcup \mathrm{dom}{R}⟶\left[0,\mathrm{+\infty }\right]↔\mathrm{toOMeas}\left({R}\right):𝒫\bigcup \mathrm{dom}{R}⟶\left[0,\mathrm{+\infty }\right]$
13 11 12 sylibr ${⊢}{\phi }\to {M}:𝒫\bigcup \mathrm{dom}{R}⟶\left[0,\mathrm{+\infty }\right]$
14 3 fdmd ${⊢}{\phi }\to \mathrm{dom}{R}={Q}$
15 14 unieqd ${⊢}{\phi }\to \bigcup \mathrm{dom}{R}=\bigcup {Q}$
16 4 15 sseqtrrd ${⊢}{\phi }\to {A}\subseteq \bigcup \mathrm{dom}{R}$
17 uniexg ${⊢}{Q}\in {V}\to \bigcup {Q}\in \mathrm{V}$
18 2 17 syl ${⊢}{\phi }\to \bigcup {Q}\in \mathrm{V}$
19 4 18 jca ${⊢}{\phi }\to \left({A}\subseteq \bigcup {Q}\wedge \bigcup {Q}\in \mathrm{V}\right)$
20 ssexg ${⊢}\left({A}\subseteq \bigcup {Q}\wedge \bigcup {Q}\in \mathrm{V}\right)\to {A}\in \mathrm{V}$
21 elpwg ${⊢}{A}\in \mathrm{V}\to \left({A}\in 𝒫\bigcup \mathrm{dom}{R}↔{A}\subseteq \bigcup \mathrm{dom}{R}\right)$
22 19 20 21 3syl ${⊢}{\phi }\to \left({A}\in 𝒫\bigcup \mathrm{dom}{R}↔{A}\subseteq \bigcup \mathrm{dom}{R}\right)$
23 16 22 mpbird ${⊢}{\phi }\to {A}\in 𝒫\bigcup \mathrm{dom}{R}$
24 13 23 ffvelrnd ${⊢}{\phi }\to {M}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]$
25 elxrge0 ${⊢}{M}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]↔\left({M}\left({A}\right)\in {ℝ}^{*}\wedge 0\le {M}\left({A}\right)\right)$
26 25 simprbi ${⊢}{M}\left({A}\right)\in \left[0,\mathrm{+\infty }\right]\to 0\le {M}\left({A}\right)$
27 24 26 syl ${⊢}{\phi }\to 0\le {M}\left({A}\right)$
28 6 rpge0d ${⊢}{\phi }\to 0\le {E}$
29 5 7 27 28 addge0d ${⊢}{\phi }\to 0\le {M}\left({A}\right)+{E}$
30 elxrge0 ${⊢}{M}\left({A}\right)+{E}\in \left[0,\mathrm{+\infty }\right]↔\left({M}\left({A}\right)+{E}\in {ℝ}^{*}\wedge 0\le {M}\left({A}\right)+{E}\right)$
31 9 29 30 sylanbrc ${⊢}{\phi }\to {M}\left({A}\right)+{E}\in \left[0,\mathrm{+\infty }\right]$
32 1 fveq1i ${⊢}{M}\left({A}\right)=\mathrm{toOMeas}\left({R}\right)\left({A}\right)$
33 omsfval ${⊢}\left({Q}\in {V}\wedge {R}:{Q}⟶\left[0,\mathrm{+\infty }\right]\wedge {A}\subseteq \bigcup {Q}\right)\to \mathrm{toOMeas}\left({R}\right)\left({A}\right)=sup\left(\mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right),\left[0,\mathrm{+\infty }\right],<\right)$
34 2 3 4 33 syl3anc ${⊢}{\phi }\to \mathrm{toOMeas}\left({R}\right)\left({A}\right)=sup\left(\mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right),\left[0,\mathrm{+\infty }\right],<\right)$
35 32 34 syl5req ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right),\left[0,\mathrm{+\infty }\right],<\right)={M}\left({A}\right)$
36 5 6 ltaddrpd ${⊢}{\phi }\to {M}\left({A}\right)<{M}\left({A}\right)+{E}$
37 35 36 eqbrtrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right),\left[0,\mathrm{+\infty }\right],<\right)<{M}\left({A}\right)+{E}$
38 iccssxr ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
39 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
40 soss ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\to \left(<\mathrm{Or}{ℝ}^{*}\to <\mathrm{Or}\left[0,\mathrm{+\infty }\right]\right)$
41 38 39 40 mp2 ${⊢}<\mathrm{Or}\left[0,\mathrm{+\infty }\right]$
42 41 a1i ${⊢}{\phi }\to <\mathrm{Or}\left[0,\mathrm{+\infty }\right]$
43 omscl ${⊢}\left({Q}\in {V}\wedge {R}:{Q}⟶\left[0,\mathrm{+\infty }\right]\wedge {A}\in 𝒫\bigcup \mathrm{dom}{R}\right)\to \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\subseteq \left[0,\mathrm{+\infty }\right]$
44 2 3 23 43 syl3anc ${⊢}{\phi }\to \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\subseteq \left[0,\mathrm{+\infty }\right]$
45 xrge0infss ${⊢}\mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\subseteq \left[0,\mathrm{+\infty }\right]\to \exists {e}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}¬{t}<{e}\wedge \forall {t}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({e}<{t}\to \exists {u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}{u}<{t}\right)\right)$
46 44 45 syl ${⊢}{\phi }\to \exists {e}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left(\forall {t}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}¬{t}<{e}\wedge \forall {t}\in \left[0,\mathrm{+\infty }\right]\phantom{\rule{.4em}{0ex}}\left({e}<{t}\to \exists {u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}{u}<{t}\right)\right)$
47 42 46 infglb ${⊢}{\phi }\to \left(\left({M}\left({A}\right)+{E}\in \left[0,\mathrm{+\infty }\right]\wedge sup\left(\mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right),\left[0,\mathrm{+\infty }\right],<\right)<{M}\left({A}\right)+{E}\right)\to \exists {u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}{u}<{M}\left({A}\right)+{E}\right)$
48 31 37 47 mp2and ${⊢}{\phi }\to \exists {u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}{u}<{M}\left({A}\right)+{E}$
49 eqid ${⊢}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)=\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)$
50 esumex ${⊢}\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\in \mathrm{V}$
51 49 50 elrnmpti ${⊢}{u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)↔\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}{u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)$
52 51 anbi1i ${⊢}\left({u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\wedge {u}<{M}\left({A}\right)+{E}\right)↔\left(\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}{u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)$
53 r19.41v ${⊢}\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)↔\left(\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}{u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)$
54 52 53 bitr4i ${⊢}\left({u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\wedge {u}<{M}\left({A}\right)+{E}\right)↔\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)$
55 54 exbii ${⊢}\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\wedge {u}<{M}\left({A}\right)+{E}\right)↔\exists {u}\phantom{\rule{.4em}{0ex}}\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)$
56 df-rex ${⊢}\exists {u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}{u}<{M}\left({A}\right)+{E}↔\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\wedge {u}<{M}\left({A}\right)+{E}\right)$
57 rexcom4 ${⊢}\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)↔\exists {u}\phantom{\rule{.4em}{0ex}}\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)$
58 55 56 57 3bitr4i ${⊢}\exists {u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}{u}<{M}\left({A}\right)+{E}↔\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)$
59 breq1 ${⊢}{u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\to \left({u}<{M}\left({A}\right)+{E}↔\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)<{M}\left({A}\right)+{E}\right)$
60 59 biimpa ${⊢}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)\to \underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)<{M}\left({A}\right)+{E}$
61 60 exlimiv ${⊢}\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)\to \underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)<{M}\left({A}\right)+{E}$
62 61 reximi ${⊢}\exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}=\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\wedge {u}<{M}\left({A}\right)+{E}\right)\to \exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)<{M}\left({A}\right)+{E}$
63 58 62 sylbi ${⊢}\exists {u}\in \mathrm{ran}\left({x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}⟼\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)\right)\phantom{\rule{.4em}{0ex}}{u}<{M}\left({A}\right)+{E}\to \exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)<{M}\left({A}\right)+{E}$
64 48 63 syl ${⊢}{\phi }\to \exists {x}\in \left\{{z}\in 𝒫\mathrm{dom}{R}|\left({A}\subseteq \bigcup {z}\wedge {z}\preccurlyeq \mathrm{\omega }\right)\right\}\phantom{\rule{.4em}{0ex}}\underset{{w}\in {x}}{{\sum }^{*}}{R}\left({w}\right)<{M}\left({A}\right)+{E}$