Metamath Proof Explorer

Theorem ovoliunnfl

Description: ovoliun is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017)

Ref Expression
Hypothesis ovoliunnfl.0 ⊢ ( ( 𝑓 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) ) ≤ sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
Assertion ovoliunnfl ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∪ 𝐴 ≠ ℝ )

Proof

Step Hyp Ref Expression
1 ovoliunnfl.0 ⊢ ( ( 𝑓 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) ) ≤ sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
2 unieq ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∪ ∅ )
3 uni0 ⊢ ∪ ∅ = ∅
4 2 3 eqtrdi ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∅ )
5 4 fveq2d ⊢ ( 𝐴 = ∅ → ( vol* ‘ ∪ 𝐴 ) = ( vol* ‘ ∅ ) )
6 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
7 5 6 eqtr2di ⊢ ( 𝐴 = ∅ → 0 = ( vol* ‘ ∪ 𝐴 ) )
8 7 a1d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol* ‘ ∪ 𝐴 ) ) )
9 ovolge0 ⊢ ( ∪ 𝐴 ⊆ ℝ → 0 ≤ ( vol* ‘ ∪ 𝐴 ) )
10 9 ad2antll ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 ≤ ( vol* ‘ ∪ 𝐴 ) )
11 reldom ⊢ Rel ≼
12 11 brrelex1i ⊢ ( 𝐴 ≼ ℕ → 𝐴 ∈ V )
13 0sdomg ⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
14 12 13 syl ⊢ ( 𝐴 ≼ ℕ → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
15 14 biimparc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) → ∅ ≺ 𝐴 )
16 fodomr ⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 )
17 15 16 sylancom ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 )
18 unissb ⊢ ( ∪ 𝐴 ⊆ ℝ ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ )
19 18 anbi1i ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) )
20 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) )
21 19 20 bitr4i ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) )
22 brdom2 ⊢ ( 𝑥 ≼ ℕ ↔ ( 𝑥 ≺ ℕ ∨ 𝑥 ≈ ℕ ) )
23 nnenom ⊢ ℕ ≈ ω
24 sdomen2 ⊢ ( ℕ ≈ ω → ( 𝑥 ≺ ℕ ↔ 𝑥 ≺ ω ) )
25 23 24 ax-mp ⊢ ( 𝑥 ≺ ℕ ↔ 𝑥 ≺ ω )
26 isfinite ⊢ ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω )
27 25 26 bitr4i ⊢ ( 𝑥 ≺ ℕ ↔ 𝑥 ∈ Fin )
28 27 orbi1i ⊢ ( ( 𝑥 ≺ ℕ ∨ 𝑥 ≈ ℕ ) ↔ ( 𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ ) )
29 22 28 bitri ⊢ ( 𝑥 ≼ ℕ ↔ ( 𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ ) )
30 ovolfi ⊢ ( ( 𝑥 ∈ Fin ∧ 𝑥 ⊆ ℝ ) → ( vol* ‘ 𝑥 ) = 0 )
31 30 expcom ⊢ ( 𝑥 ⊆ ℝ → ( 𝑥 ∈ Fin → ( vol* ‘ 𝑥 ) = 0 ) )
32 ovolctb ⊢ ( ( 𝑥 ⊆ ℝ ∧ 𝑥 ≈ ℕ ) → ( vol* ‘ 𝑥 ) = 0 )
33 32 ex ⊢ ( 𝑥 ⊆ ℝ → ( 𝑥 ≈ ℕ → ( vol* ‘ 𝑥 ) = 0 ) )
34 31 33 jaod ⊢ ( 𝑥 ⊆ ℝ → ( ( 𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ ) → ( vol* ‘ 𝑥 ) = 0 ) )
35 29 34 syl5bi ⊢ ( 𝑥 ⊆ ℝ → ( 𝑥 ≼ ℕ → ( vol* ‘ 𝑥 ) = 0 ) )
36 35 imdistani ⊢ ( ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) → ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) )
37 36 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) )
38 21 37 sylbi ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) )
39 38 ancoms ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) )
40 foima ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( 𝑓 “ ℕ ) = 𝐴 )
41 40 raleqdv ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ ( 𝑓 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ) )
42 fofn ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → 𝑓 Fn ℕ )
43 ssid ⊢ ℕ ⊆ ℕ
44 sseq1 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑙 ) → ( 𝑥 ⊆ ℝ ↔ ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ) )
45 fveqeq2 ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑙 ) → ( ( vol* ‘ 𝑥 ) = 0 ↔ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) )
46 44 45 anbi12d ⊢ ( 𝑥 = ( 𝑓 ‘ 𝑙 ) → ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ) )
47 46 ralima ⊢ ( ( 𝑓 Fn ℕ ∧ ℕ ⊆ ℕ ) → ( ∀ 𝑥 ∈ ( 𝑓 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ) )
48 42 43 47 sylancl ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ ( 𝑓 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ) )
49 41 48 bitr3d ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ) )
50 fveq2 ⊢ ( 𝑙 = 𝑛 → ( 𝑓 ‘ 𝑙 ) = ( 𝑓 ‘ 𝑛 ) )
51 50 sseq1d ⊢ ( 𝑙 = 𝑛 → ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ↔ ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ) )
52 2fveq3 ⊢ ( 𝑙 = 𝑛 → ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) )
53 52 eqeq1d ⊢ ( 𝑙 = 𝑛 → ( ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ↔ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 ) )
54 51 53 anbi12d ⊢ ( 𝑙 = 𝑛 → ( ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ↔ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 ) ) )
55 54 cbvralvw ⊢ ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 ) )
56 0re ⊢ 0 ∈ ℝ
57 eleq1a ⊢ ( 0 ∈ ℝ → ( ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 → ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) )
58 56 57 ax-mp ⊢ ( ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 → ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ )
59 58 anim2i ⊢ ( ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 ) → ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) )
60 59 ralimi ⊢ ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) = 0 ) → ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) )
61 55 60 sylbi ⊢ ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) → ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) )
62 42 61 1 syl2an ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) ) ≤ sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
63 fofun ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → Fun 𝑓 )
64 funiunfv ⊢ ( Fun 𝑓 → ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) = ∪ ( 𝑓 “ ℕ ) )
65 63 64 syl ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) = ∪ ( 𝑓 “ ℕ ) )
66 40 unieqd ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ∪ ( 𝑓 “ ℕ ) = ∪ 𝐴 )
67 65 66 eqtrd ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) = ∪ 𝐴 )
68 67 fveq2d ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) ) = ( vol* ‘ ∪ 𝐴 ) )
69 68 adantr ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) ) = ( vol* ‘ ∪ 𝐴 ) )
70 fveq2 ⊢ ( 𝑙 = 𝑚 → ( 𝑓 ‘ 𝑙 ) = ( 𝑓 ‘ 𝑚 ) )
71 70 sseq1d ⊢ ( 𝑙 = 𝑚 → ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ↔ ( 𝑓 ‘ 𝑚 ) ⊆ ℝ ) )
72 2fveq3 ⊢ ( 𝑙 = 𝑚 → ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) )
73 72 eqeq1d ⊢ ( 𝑙 = 𝑚 → ( ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ↔ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) = 0 ) )
74 71 73 anbi12d ⊢ ( 𝑙 = 𝑚 → ( ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ↔ ( ( 𝑓 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) = 0 ) ) )
75 74 rspccva ⊢ ( ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) = 0 ) )
76 75 simprd ⊢ ( ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) = 0 )
77 76 mpteq2dva ⊢ ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) → ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ 0 ) )
78 77 seqeq3d ⊢ ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) )
79 78 rneqd ⊢ ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) → ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) = ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) )
80 79 supeq1d ⊢ ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) → sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) , ℝ* , < ) )
81 0cn ⊢ 0 ∈ ℂ
82 ser1const ⊢ ( ( 0 ∈ ℂ ∧ 𝑙 ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑙 ) = ( 𝑙 · 0 ) )
83 81 82 mpan ⊢ ( 𝑙 ∈ ℕ → ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑙 ) = ( 𝑙 · 0 ) )
84 nncn ⊢ ( 𝑙 ∈ ℕ → 𝑙 ∈ ℂ )
85 84 mul01d ⊢ ( 𝑙 ∈ ℕ → ( 𝑙 · 0 ) = 0 )
86 83 85 eqtrd ⊢ ( 𝑙 ∈ ℕ → ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑙 ) = 0 )
87 86 mpteq2ia ⊢ ( 𝑙 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑙 ) ) = ( 𝑙 ∈ ℕ ↦ 0 )
88 fconstmpt ⊢ ( ℕ × { 0 } ) = ( 𝑚 ∈ ℕ ↦ 0 )
89 seqeq3 ⊢ ( ( ℕ × { 0 } ) = ( 𝑚 ∈ ℕ ↦ 0 ) → seq 1 ( + , ( ℕ × { 0 } ) ) = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) )
90 88 89 ax-mp ⊢ seq 1 ( + , ( ℕ × { 0 } ) ) = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) )
91 1z ⊢ 1 ∈ ℤ
92 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( ℕ × { 0 } ) ) Fn ( ℤ≥ ‘ 1 ) )
93 91 92 ax-mp ⊢ seq 1 ( + , ( ℕ × { 0 } ) ) Fn ( ℤ≥ ‘ 1 )
94 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
95 94 fneq2i ⊢ ( seq 1 ( + , ( ℕ × { 0 } ) ) Fn ℕ ↔ seq 1 ( + , ( ℕ × { 0 } ) ) Fn ( ℤ≥ ‘ 1 ) )
96 dffn5 ⊢ ( seq 1 ( + , ( ℕ × { 0 } ) ) Fn ℕ ↔ seq 1 ( + , ( ℕ × { 0 } ) ) = ( 𝑙 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑙 ) ) )
97 95 96 bitr3i ⊢ ( seq 1 ( + , ( ℕ × { 0 } ) ) Fn ( ℤ≥ ‘ 1 ) ↔ seq 1 ( + , ( ℕ × { 0 } ) ) = ( 𝑙 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑙 ) ) )
98 93 97 mpbi ⊢ seq 1 ( + , ( ℕ × { 0 } ) ) = ( 𝑙 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑙 ) )
99 90 98 eqtr3i ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) = ( 𝑙 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑙 ) )
100 fconstmpt ⊢ ( ℕ × { 0 } ) = ( 𝑙 ∈ ℕ ↦ 0 )
101 87 99 100 3eqtr4i ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) = ( ℕ × { 0 } )
102 101 rneqi ⊢ ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) = ran ( ℕ × { 0 } )
103 1nn ⊢ 1 ∈ ℕ
104 ne0i ⊢ ( 1 ∈ ℕ → ℕ ≠ ∅ )
105 rnxp ⊢ ( ℕ ≠ ∅ → ran ( ℕ × { 0 } ) = { 0 } )
106 103 104 105 mp2b ⊢ ran ( ℕ × { 0 } ) = { 0 }
107 102 106 eqtri ⊢ ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) = { 0 }
108 107 supeq1i ⊢ sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < )
109 xrltso ⊢ < Or ℝ*
110 0xr ⊢ 0 ∈ ℝ*
111 supsn ⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
112 109 110 111 mp2an ⊢ sup ( { 0 } , ℝ* , < ) = 0
113 108 112 eqtri ⊢ sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 0 ) ) , ℝ* , < ) = 0
114 80 113 eqtrdi ⊢ ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) → sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) , ℝ* , < ) = 0 )
115 114 adantl ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ) → sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) , ℝ* , < ) = 0 )
116 62 69 115 3brtr3d ⊢ ( ( 𝑓 : ℕ –onto→ 𝐴 ∧ ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) ) → ( vol* ‘ ∪ 𝐴 ) ≤ 0 )
117 116 ex ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( ∀ 𝑙 ∈ ℕ ( ( 𝑓 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑙 ) ) = 0 ) → ( vol* ‘ ∪ 𝐴 ) ≤ 0 ) )
118 49 117 sylbid ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) → ( vol* ‘ ∪ 𝐴 ) ≤ 0 ) )
119 118 exlimiv ⊢ ( ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) → ( vol* ‘ ∪ 𝐴 ) ≤ 0 ) )
120 119 imp ⊢ ( ( ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ) → ( vol* ‘ ∪ 𝐴 ) ≤ 0 )
121 17 39 120 syl2an ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → ( vol* ‘ ∪ 𝐴 ) ≤ 0 )
122 ovolcl ⊢ ( ∪ 𝐴 ⊆ ℝ → ( vol* ‘ ∪ 𝐴 ) ∈ ℝ* )
123 xrletri3 ⊢ ( ( 0 ∈ ℝ* ∧ ( vol* ‘ ∪ 𝐴 ) ∈ ℝ* ) → ( 0 = ( vol* ‘ ∪ 𝐴 ) ↔ ( 0 ≤ ( vol* ‘ ∪ 𝐴 ) ∧ ( vol* ‘ ∪ 𝐴 ) ≤ 0 ) ) )
124 110 122 123 sylancr ⊢ ( ∪ 𝐴 ⊆ ℝ → ( 0 = ( vol* ‘ ∪ 𝐴 ) ↔ ( 0 ≤ ( vol* ‘ ∪ 𝐴 ) ∧ ( vol* ‘ ∪ 𝐴 ) ≤ 0 ) ) )
125 124 ad2antll ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → ( 0 = ( vol* ‘ ∪ 𝐴 ) ↔ ( 0 ≤ ( vol* ‘ ∪ 𝐴 ) ∧ ( vol* ‘ ∪ 𝐴 ) ≤ 0 ) ) )
126 10 121 125 mpbir2and ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol* ‘ ∪ 𝐴 ) )
127 126 expl ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol* ‘ ∪ 𝐴 ) ) )
128 8 127 pm2.61ine ⊢ ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol* ‘ ∪ 𝐴 ) )
129 renepnf ⊢ ( 0 ∈ ℝ → 0 ≠ +∞ )
130 56 129 mp1i ⊢ ( ∪ 𝐴 = ℝ → 0 ≠ +∞ )
131 fveq2 ⊢ ( ∪ 𝐴 = ℝ → ( vol* ‘ ∪ 𝐴 ) = ( vol* ‘ ℝ ) )
132 ovolre ⊢ ( vol* ‘ ℝ ) = +∞
133 131 132 eqtrdi ⊢ ( ∪ 𝐴 = ℝ → ( vol* ‘ ∪ 𝐴 ) = +∞ )
134 130 133 neeqtrrd ⊢ ( ∪ 𝐴 = ℝ → 0 ≠ ( vol* ‘ ∪ 𝐴 ) )
135 134 necon2i ⊢ ( 0 = ( vol* ‘ ∪ 𝐴 ) → ∪ 𝐴 ≠ ℝ )
136 128 135 syl ⊢ ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → ∪ 𝐴 ≠ ℝ )
137 136 expr ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ( ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ ) )
138 eqimss ⊢ ( ∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ )
139 138 necon3bi ⊢ ( ¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ )
140 137 139 pm2.61d1 ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∪ 𝐴 ≠ ℝ )