Metamath Proof Explorer

Theorem voliunnfl

Description: voliun is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017)

Ref Expression
Hypotheses voliunnfl.1 ⊢ 𝑆 = seq 1 ( + , 𝐺 )
voliunnfl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) )
voliunnfl.3 ⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = sup ( ran 𝑆 , ℝ* , < ) )
Assertion voliunnfl ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∪ 𝐴 ≠ ℝ )

Proof

Step Hyp Ref Expression
1 voliunnfl.1 ⊢ 𝑆 = seq 1 ( + , 𝐺 )
2 voliunnfl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) )
3 voliunnfl.3 ⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = sup ( ran 𝑆 , ℝ* , < ) )
4 unieq ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∪ ∅ )
5 uni0 ⊢ ∪ ∅ = ∅
6 4 5 eqtrdi ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∅ )
7 6 fveq2d ⊢ ( 𝐴 = ∅ → ( vol ‘ ∪ 𝐴 ) = ( vol ‘ ∅ ) )
8 0mbl ⊢ ∅ ∈ dom vol
9 mblvol ⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
10 8 9 ax-mp ⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
11 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
12 10 11 eqtri ⊢ ( vol ‘ ∅ ) = 0
13 7 12 eqtr2di ⊢ ( 𝐴 = ∅ → 0 = ( vol ‘ ∪ 𝐴 ) )
14 13 a1d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
15 reldom ⊢ Rel ≼
16 15 brrelex1i ⊢ ( 𝐴 ≼ ℕ → 𝐴 ∈ V )
17 0sdomg ⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
18 16 17 syl ⊢ ( 𝐴 ≼ ℕ → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
19 18 biimparc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) → ∅ ≺ 𝐴 )
20 fodomr ⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ ) → ∃ 𝑔 𝑔 : ℕ –onto→ 𝐴 )
21 19 20 sylancom ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) → ∃ 𝑔 𝑔 : ℕ –onto→ 𝐴 )
22 unissb ⊢ ( ∪ 𝐴 ⊆ ℝ ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ )
23 22 anbi1i ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) )
24 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) )
25 23 24 bitr4i ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) )
26 ovolctb2 ⊢ ( ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) → ( vol* ‘ 𝑥 ) = 0 )
27 26 ex ⊢ ( 𝑥 ⊆ ℝ → ( 𝑥 ≼ ℕ → ( vol* ‘ 𝑥 ) = 0 ) )
28 27 imdistani ⊢ ( ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) → ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) )
29 28 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) )
30 25 29 sylbi ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) )
31 30 ancoms ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) )
32 foima ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( 𝑔 “ ℕ ) = 𝐴 )
33 32 raleqdv ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ ( 𝑔 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ) )
34 fofn ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → 𝑔 Fn ℕ )
35 ssid ⊢ ℕ ⊆ ℕ
36 sseq1 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑚 ) → ( 𝑥 ⊆ ℝ ↔ ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ) )
37 fveqeq2 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑚 ) → ( ( vol* ‘ 𝑥 ) = 0 ↔ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) )
38 36 37 anbi12d ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑚 ) → ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ) )
39 38 ralima ⊢ ( ( 𝑔 Fn ℕ ∧ ℕ ⊆ ℕ ) → ( ∀ 𝑥 ∈ ( 𝑔 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ) )
40 34 35 39 sylancl ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ ( 𝑔 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ) )
41 33 40 bitr3d ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ) )
42 difss ⊢ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ( 𝑔 ‘ 𝑚 )
43 ovolssnul ⊢ ( ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ( 𝑔 ‘ 𝑚 ) ∧ ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 )
44 42 43 mp3an1 ⊢ ( ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 )
45 ssdifss ⊢ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ → ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ℝ )
46 nulmbl ⊢ ( ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) → ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol )
47 mblvol ⊢ ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol → ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) )
48 47 eqeq1d ⊢ ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol → ( ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ↔ ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) )
49 48 biimpar ⊢ ( ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) → ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 )
50 0re ⊢ 0 ∈ ℝ
51 49 50 eqeltrdi ⊢ ( ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) → ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ )
52 51 expcom ⊢ ( ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 → ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol → ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
53 52 ancld ⊢ ( ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 → ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol → ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) ) )
54 53 adantl ⊢ ( ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) → ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol → ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) ) )
55 46 54 mpd ⊢ ( ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) → ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
56 45 55 sylan ⊢ ( ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) → ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
57 44 56 syldan ⊢ ( ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
58 57 ralimi ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → ∀ 𝑚 ∈ ℕ ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
59 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑔 ‘ 𝑚 ) = ( 𝑔 ‘ 𝑛 ) )
60 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 1 ..^ 𝑚 ) = ( 1 ..^ 𝑛 ) )
61 60 iuneq1d ⊢ ( 𝑚 = 𝑛 → ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) = ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) )
62 59 61 difeq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) )
63 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
64 fvex ⊢ ( 𝑔 ‘ 𝑛 ) ∈ V
65 difexg ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ V → ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ V )
66 64 65 ax-mp ⊢ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ V
67 62 63 66 fvmpt ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) = ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) )
68 67 eleq1d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ↔ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ) )
69 67 fveq2d ⊢ ( 𝑛 ∈ ℕ → ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) = ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) )
70 69 eleq1d ⊢ ( 𝑛 ∈ ℕ → ( ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ↔ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
71 68 70 anbi12d ⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ↔ ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) ) )
72 71 ralbiia ⊢ ( ∀ 𝑛 ∈ ℕ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ↔ ∀ 𝑛 ∈ ℕ ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
73 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑚 ) )
74 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑚 ) )
75 74 iuneq1d ⊢ ( 𝑛 = 𝑚 → ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) = ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) )
76 73 75 difeq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) = ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
77 76 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ↔ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ) )
78 76 fveq2d ⊢ ( 𝑛 = 𝑚 → ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) )
79 78 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ↔ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
80 77 79 anbi12d ⊢ ( 𝑛 = 𝑚 → ( ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) ↔ ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) ) )
81 80 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) ↔ ∀ 𝑚 ∈ ℕ ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
82 72 81 bitri ⊢ ( ∀ 𝑛 ∈ ℕ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ↔ ∀ 𝑚 ∈ ℕ ( ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ ℝ ) )
83 58 82 sylibr ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → ∀ 𝑛 ∈ ℕ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) )
84 fveq2 ⊢ ( 𝑛 = 𝑙 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑙 ) )
85 84 iundisj2 ⊢ Disj 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) )
86 disjeq2 ⊢ ( ∀ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) = ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) → ( Disj 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ↔ Disj 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) )
87 86 67 mprg ⊢ ( Disj 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ↔ Disj 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) )
88 85 87 mpbir ⊢ Disj 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 )
89 nnex ⊢ ℕ ∈ V
90 89 mptex ⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∈ V
91 fveq1 ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( 𝑓 ‘ 𝑛 ) = ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) )
92 91 eleq1d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( ( 𝑓 ‘ 𝑛 ) ∈ dom vol ↔ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ) )
93 91 fveq2d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) = ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) )
94 93 eleq1d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ↔ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) )
95 92 94 anbi12d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( ( ( 𝑓 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ↔ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ) )
96 95 ralbidv ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ↔ ∀ 𝑛 ∈ ℕ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ) )
97 91 adantr ⊢ ( ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) = ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) )
98 97 disjeq2dv ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ↔ Disj 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) )
99 96 98 anbi12d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) ↔ ( ∀ 𝑛 ∈ ℕ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) )
100 91 iuneq2d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) )
101 100 fveq2d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) )
102 seqeq3 ⊢ ( 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) → seq 1 ( + , 𝐺 ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
103 2 102 ax-mp ⊢ seq 1 ( + , 𝐺 ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
104 1 103 eqtri ⊢ 𝑆 = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
105 104 rneqi ⊢ ran 𝑆 = ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
106 105 supeq1i ⊢ sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) , ℝ* , < )
107 93 mpteq2dv ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) )
108 107 seqeq3d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) )
109 108 rneqd ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) )
110 109 supeq1d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) , ℝ* , < ) )
111 106 110 eqtrid ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) , ℝ* , < ) )
112 101 111 eqeq12d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = sup ( ran 𝑆 , ℝ* , < ) ↔ ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) , ℝ* , < ) ) )
113 99 112 imbi12d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) → ( ( ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) = sup ( ran 𝑆 , ℝ* , < ) ) ↔ ( ( ∀ 𝑛 ∈ ℕ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) , ℝ* , < ) ) ) )
114 90 113 3 vtocl ⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) , ℝ* , < ) )
115 67 iuneq2i ⊢ ∪ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) )
116 115 fveq2i ⊢ ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) = ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) )
117 69 mpteq2ia ⊢ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) )
118 seqeq3 ⊢ ( ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) )
119 117 118 ax-mp ⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) )
120 119 rneqi ⊢ ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) = ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) )
121 120 supeq1i ⊢ sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) , ℝ* , < )
122 114 116 121 3eqtr3g ⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ∈ dom vol ∧ ( vol ‘ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) ∈ ℝ ) ∧ Disj 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑚 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ‘ 𝑛 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) , ℝ* , < ) )
123 83 88 122 sylancl ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) , ℝ* , < ) )
124 123 adantl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) , ℝ* , < ) )
125 84 iundisj ⊢ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) )
126 fofun ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → Fun 𝑔 )
127 funiunfv ⊢ ( Fun 𝑔 → ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝑔 “ ℕ ) )
128 126 127 syl ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) = ∪ ( 𝑔 “ ℕ ) )
129 125 128 eqtr3id ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) = ∪ ( 𝑔 “ ℕ ) )
130 32 unieqd ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∪ ( 𝑔 “ ℕ ) = ∪ 𝐴 )
131 129 130 eqtrd ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) = ∪ 𝐴 )
132 131 fveq2d ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol ‘ ∪ 𝐴 ) )
133 132 adantr ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ) → ( vol ‘ ∪ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol ‘ ∪ 𝐴 ) )
134 59 sseq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ↔ ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ) )
135 59 fveqeq2d ⊢ ( 𝑚 = 𝑛 → ( ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ↔ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) )
136 134 135 anbi12d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ↔ ( ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) ) )
137 136 rspccva ⊢ ( ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) )
138 ssdifss ⊢ ( ( 𝑔 ‘ 𝑛 ) ⊆ ℝ → ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ℝ )
139 138 adantr ⊢ ( ( ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) → ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ℝ )
140 difss ⊢ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ( 𝑔 ‘ 𝑛 )
141 ovolssnul ⊢ ( ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) → ( vol* ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 )
142 140 141 mp3an1 ⊢ ( ( ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) → ( vol* ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 )
143 139 142 jca ⊢ ( ( ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) → ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) )
144 nulmbl ⊢ ( ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 ) → ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol )
145 mblvol ⊢ ( ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ∈ dom vol → ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol* ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) )
146 143 144 145 3syl ⊢ ( ( ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) → ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol* ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) )
147 146 142 eqtrd ⊢ ( ( ( 𝑔 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑛 ) ) = 0 ) → ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 )
148 137 147 syl ⊢ ( ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) = 0 )
149 148 mpteq2dva ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ 0 ) )
150 149 seqeq3d ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) )
151 150 rneqd ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) = ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) )
152 151 supeq1d ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) , ℝ* , < ) )
153 0cn ⊢ 0 ∈ ℂ
154 ser1const ⊢ ( ( 0 ∈ ℂ ∧ 𝑚 ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑚 ) = ( 𝑚 · 0 ) )
155 153 154 mpan ⊢ ( 𝑚 ∈ ℕ → ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑚 ) = ( 𝑚 · 0 ) )
156 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
157 156 mul01d ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 · 0 ) = 0 )
158 155 157 eqtrd ⊢ ( 𝑚 ∈ ℕ → ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑚 ) = 0 )
159 158 mpteq2ia ⊢ ( 𝑚 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑚 ) ) = ( 𝑚 ∈ ℕ ↦ 0 )
160 fconstmpt ⊢ ( ℕ × { 0 } ) = ( 𝑛 ∈ ℕ ↦ 0 )
161 seqeq3 ⊢ ( ( ℕ × { 0 } ) = ( 𝑛 ∈ ℕ ↦ 0 ) → seq 1 ( + , ( ℕ × { 0 } ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) )
162 160 161 ax-mp ⊢ seq 1 ( + , ( ℕ × { 0 } ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) )
163 1z ⊢ 1 ∈ ℤ
164 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( ℕ × { 0 } ) ) Fn ( ℤ≥ ‘ 1 ) )
165 163 164 ax-mp ⊢ seq 1 ( + , ( ℕ × { 0 } ) ) Fn ( ℤ≥ ‘ 1 )
166 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
167 166 fneq2i ⊢ ( seq 1 ( + , ( ℕ × { 0 } ) ) Fn ℕ ↔ seq 1 ( + , ( ℕ × { 0 } ) ) Fn ( ℤ≥ ‘ 1 ) )
168 dffn5 ⊢ ( seq 1 ( + , ( ℕ × { 0 } ) ) Fn ℕ ↔ seq 1 ( + , ( ℕ × { 0 } ) ) = ( 𝑚 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑚 ) ) )
169 167 168 bitr3i ⊢ ( seq 1 ( + , ( ℕ × { 0 } ) ) Fn ( ℤ≥ ‘ 1 ) ↔ seq 1 ( + , ( ℕ × { 0 } ) ) = ( 𝑚 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑚 ) ) )
170 165 169 mpbi ⊢ seq 1 ( + , ( ℕ × { 0 } ) ) = ( 𝑚 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑚 ) )
171 162 170 eqtr3i ⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) = ( 𝑚 ∈ ℕ ↦ ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ 𝑚 ) )
172 fconstmpt ⊢ ( ℕ × { 0 } ) = ( 𝑚 ∈ ℕ ↦ 0 )
173 159 171 172 3eqtr4i ⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) = ( ℕ × { 0 } )
174 173 rneqi ⊢ ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) = ran ( ℕ × { 0 } )
175 1nn ⊢ 1 ∈ ℕ
176 ne0i ⊢ ( 1 ∈ ℕ → ℕ ≠ ∅ )
177 rnxp ⊢ ( ℕ ≠ ∅ → ran ( ℕ × { 0 } ) = { 0 } )
178 175 176 177 mp2b ⊢ ran ( ℕ × { 0 } ) = { 0 }
179 174 178 eqtri ⊢ ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) = { 0 }
180 179 supeq1i ⊢ sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < )
181 xrltso ⊢ < Or ℝ*
182 0xr ⊢ 0 ∈ ℝ*
183 supsn ⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
184 181 182 183 mp2an ⊢ sup ( { 0 } , ℝ* , < ) = 0
185 180 184 eqtri ⊢ sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ 0 ) ) , ℝ* , < ) = 0
186 152 185 eqtrdi ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) , ℝ* , < ) = 0 )
187 186 adantl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ) → sup ( ran seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝑔 ‘ 𝑛 ) ∖ ∪ 𝑙 ∈ ( 1 ..^ 𝑛 ) ( 𝑔 ‘ 𝑙 ) ) ) ) ) , ℝ* , < ) = 0 )
188 124 133 187 3eqtr3rd ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) ) → 0 = ( vol ‘ ∪ 𝐴 ) )
189 188 ex ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑚 ∈ ℕ ( ( 𝑔 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑚 ) ) = 0 ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
190 41 189 sylbid ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
191 31 190 syl5 ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
192 191 exlimiv ⊢ ( ∃ 𝑔 𝑔 : ℕ –onto→ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
193 21 192 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
194 193 expimpd ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
195 14 194 pm2.61ine ⊢ ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol ‘ ∪ 𝐴 ) )
196 renepnf ⊢ ( 0 ∈ ℝ → 0 ≠ +∞ )
197 50 196 mp1i ⊢ ( ∪ 𝐴 = ℝ → 0 ≠ +∞ )
198 fveq2 ⊢ ( ∪ 𝐴 = ℝ → ( vol ‘ ∪ 𝐴 ) = ( vol ‘ ℝ ) )
199 rembl ⊢ ℝ ∈ dom vol
200 mblvol ⊢ ( ℝ ∈ dom vol → ( vol ‘ ℝ ) = ( vol* ‘ ℝ ) )
201 199 200 ax-mp ⊢ ( vol ‘ ℝ ) = ( vol* ‘ ℝ )
202 ovolre ⊢ ( vol* ‘ ℝ ) = +∞
203 201 202 eqtri ⊢ ( vol ‘ ℝ ) = +∞
204 198 203 eqtrdi ⊢ ( ∪ 𝐴 = ℝ → ( vol ‘ ∪ 𝐴 ) = +∞ )
205 197 204 neeqtrrd ⊢ ( ∪ 𝐴 = ℝ → 0 ≠ ( vol ‘ ∪ 𝐴 ) )
206 205 necon2i ⊢ ( 0 = ( vol ‘ ∪ 𝐴 ) → ∪ 𝐴 ≠ ℝ )
207 195 206 syl ⊢ ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → ∪ 𝐴 ≠ ℝ )
208 207 expr ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ( ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ ) )
209 eqimss ⊢ ( ∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ )
210 209 necon3bi ⊢ ( ¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ )
211 208 210 pm2.61d1 ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∪ 𝐴 ≠ ℝ )