Metamath Proof Explorer

Theorem omssubaddlem

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 ⊢ 𝑀 = ( toOMeas ‘ 𝑅 )
oms.o ⊢ ( 𝜑 → 𝑄 ∈ 𝑉 )
oms.r ⊢ ( 𝜑 → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
omssubaddlem.a ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑄 )
omssubaddlem.m ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
omssubaddlem.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
Assertion omssubaddlem ( 𝜑 → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )

Proof

Step Hyp Ref Expression
1 oms.m ⊢ 𝑀 = ( toOMeas ‘ 𝑅 )
2 oms.o ⊢ ( 𝜑 → 𝑄 ∈ 𝑉 )
3 oms.r ⊢ ( 𝜑 → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
4 omssubaddlem.a ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑄 )
5 omssubaddlem.m ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
6 omssubaddlem.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
7 6 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
8 5 7 readdcld ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ∈ ℝ )
9 8 rexrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ∈ ℝ* )
10 omsf ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) → ( toOMeas ‘ 𝑅 ) : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) )
11 2 3 10 syl2anc ⊢ ( 𝜑 → ( toOMeas ‘ 𝑅 ) : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) )
12 1 feq1i ⊢ ( 𝑀 : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) ↔ ( toOMeas ‘ 𝑅 ) : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) )
13 11 12 sylibr ⊢ ( 𝜑 → 𝑀 : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) )
14 3 fdmd ⊢ ( 𝜑 → dom 𝑅 = 𝑄 )
15 14 unieqd ⊢ ( 𝜑 → ∪ dom 𝑅 = ∪ 𝑄 )
16 4 15 sseqtrrd ⊢ ( 𝜑 → 𝐴 ⊆ ∪ dom 𝑅 )
17 2 uniexd ⊢ ( 𝜑 → ∪ 𝑄 ∈ V )
18 4 17 jca ⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ 𝑄 ∧ ∪ 𝑄 ∈ V ) )
19 ssexg ⊢ ( ( 𝐴 ⊆ ∪ 𝑄 ∧ ∪ 𝑄 ∈ V ) → 𝐴 ∈ V )
20 elpwg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom 𝑅 ) )
21 18 19 20 3syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom 𝑅 ) )
22 16 21 mpbird ⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ∪ dom 𝑅 )
23 13 22 ffvelcdmd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
24 elxrge0 ⊢ ( ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑀 ‘ 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝑀 ‘ 𝐴 ) ) )
25 24 simprbi ⊢ ( ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑀 ‘ 𝐴 ) )
26 23 25 syl ⊢ ( 𝜑 → 0 ≤ ( 𝑀 ‘ 𝐴 ) )
27 6 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝐸 )
28 5 7 26 27 addge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )
29 elxrge0 ⊢ ( ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ∈ ( 0 [,] +∞ ) ↔ ( ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ∈ ℝ* ∧ 0 ≤ ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
30 9 28 29 sylanbrc ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ∈ ( 0 [,] +∞ ) )
31 1 fveq1i ⊢ ( 𝑀 ‘ 𝐴 ) = ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 )
32 omsfval ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ⊆ ∪ 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
33 2 3 4 32 syl3anc ⊢ ( 𝜑 → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) , ( 0 [,] +∞ ) , < ) )
34 31 33 eqtr2id ⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) , ( 0 [,] +∞ ) , < ) = ( 𝑀 ‘ 𝐴 ) )
35 5 6 ltaddrpd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )
36 34 35 eqbrtrd ⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) , ( 0 [,] +∞ ) , < ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )
37 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
38 xrltso ⊢ < Or ℝ*
39 soss ⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] +∞ ) ) )
40 37 38 39 mp2 ⊢ < Or ( 0 [,] +∞ )
41 40 a1i ⊢ ( 𝜑 → < Or ( 0 [,] +∞ ) )
42 omscl ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅 ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ⊆ ( 0 [,] +∞ ) )
43 2 3 22 42 syl3anc ⊢ ( 𝜑 → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ⊆ ( 0 [,] +∞ ) )
44 xrge0infss ⊢ ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ⊆ ( 0 [,] +∞ ) → ∃ 𝑒 ∈ ( 0 [,] +∞ ) ( ∀ 𝑡 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ¬ 𝑡 < 𝑒 ∧ ∀ 𝑡 ∈ ( 0 [,] +∞ ) ( 𝑒 < 𝑡 → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) 𝑢 < 𝑡 ) ) )
45 43 44 syl ⊢ ( 𝜑 → ∃ 𝑒 ∈ ( 0 [,] +∞ ) ( ∀ 𝑡 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ¬ 𝑡 < 𝑒 ∧ ∀ 𝑡 ∈ ( 0 [,] +∞ ) ( 𝑒 < 𝑡 → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) 𝑢 < 𝑡 ) ) )
46 41 45 infglb ⊢ ( 𝜑 → ( ( ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ∈ ( 0 [,] +∞ ) ∧ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) , ( 0 [,] +∞ ) , < ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
47 30 36 46 mp2and ⊢ ( 𝜑 → ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )
48 eqid ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) )
49 esumex ⊢ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∈ V
50 48 49 elrnmpti ⊢ ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) )
51 50 anbi1i ⊢ ( ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) ↔ ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
52 r19.41v ⊢ ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) ↔ ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
53 51 52 bitr4i ⊢ ( ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
54 53 exbii ⊢ ( ∃ 𝑢 ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) ↔ ∃ 𝑢 ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
55 df-rex ⊢ ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ↔ ∃ 𝑢 ( 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
56 rexcom4 ⊢ ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ∃ 𝑢 ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) ↔ ∃ 𝑢 ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
57 54 55 56 3bitr4i ⊢ ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ∃ 𝑢 ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
58 breq1 ⊢ ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) → ( 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ↔ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) )
59 58 biimpa ⊢ ( ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) → Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )
60 59 exlimiv ⊢ ( ∃ 𝑢 ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) → Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )
61 60 reximi ⊢ ( ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ∃ 𝑢 ( 𝑢 = Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ∧ 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )
62 57 61 sylbi ⊢ ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) ) 𝑢 < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )
63 47 62 syl ⊢ ( 𝜑 → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } Σ* 𝑤 ∈ 𝑥 ( 𝑅 ‘ 𝑤 ) < ( ( 𝑀 ‘ 𝐴 ) + 𝐸 ) )