Metamath Proof Explorer

Theorem volsupnfl

Description: volsup is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018)

Ref Expression
Hypothesis volsupnfl.0 ⊢ ( ( 𝑓 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ⊆ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) → ( vol ‘ ∪ ran 𝑓 ) = sup ( ( vol “ ran 𝑓 ) , ℝ* , < ) )
Assertion volsupnfl ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∪ 𝐴 ≠ ℝ )

Proof

Step Hyp Ref Expression
1 volsupnfl.0 ⊢ ( ( 𝑓 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ⊆ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) → ( vol ‘ ∪ ran 𝑓 ) = sup ( ( vol “ ran 𝑓 ) , ℝ* , < ) )
2 unieq ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∪ ∅ )
3 uni0 ⊢ ∪ ∅ = ∅
4 2 3 eqtrdi ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∅ )
5 4 fveq2d ⊢ ( 𝐴 = ∅ → ( vol ‘ ∪ 𝐴 ) = ( vol ‘ ∅ ) )
6 0mbl ⊢ ∅ ∈ dom vol
7 mblvol ⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
8 6 7 ax-mp ⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
9 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
10 8 9 eqtri ⊢ ( vol ‘ ∅ ) = 0
11 5 10 eqtr2di ⊢ ( 𝐴 = ∅ → 0 = ( vol ‘ ∪ 𝐴 ) )
12 11 a1d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
13 reldom ⊢ Rel ≼
14 13 brrelex1i ⊢ ( 𝐴 ≼ ℕ → 𝐴 ∈ V )
15 0sdomg ⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
16 14 15 syl ⊢ ( 𝐴 ≼ ℕ → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
17 16 biimparc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) → ∅ ≺ 𝐴 )
18 fodomr ⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ ) → ∃ 𝑔 𝑔 : ℕ –onto→ 𝐴 )
19 17 18 sylancom ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) → ∃ 𝑔 𝑔 : ℕ –onto→ 𝐴 )
20 unissb ⊢ ( ∪ 𝐴 ⊆ ℝ ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ )
21 20 anbi1i ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) )
22 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) )
23 21 22 bitr4i ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) )
24 ovolctb2 ⊢ ( ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) → ( vol* ‘ 𝑥 ) = 0 )
25 nulmbl ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) → 𝑥 ∈ dom vol )
26 mblvol ⊢ ( 𝑥 ∈ dom vol → ( vol ‘ 𝑥 ) = ( vol* ‘ 𝑥 ) )
27 eqtr ⊢ ( ( ( vol ‘ 𝑥 ) = ( vol* ‘ 𝑥 ) ∧ ( vol* ‘ 𝑥 ) = 0 ) → ( vol ‘ 𝑥 ) = 0 )
28 27 expcom ⊢ ( ( vol* ‘ 𝑥 ) = 0 → ( ( vol ‘ 𝑥 ) = ( vol* ‘ 𝑥 ) → ( vol ‘ 𝑥 ) = 0 ) )
29 26 28 syl5 ⊢ ( ( vol* ‘ 𝑥 ) = 0 → ( 𝑥 ∈ dom vol → ( vol ‘ 𝑥 ) = 0 ) )
30 29 adantl ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) → ( 𝑥 ∈ dom vol → ( vol ‘ 𝑥 ) = 0 ) )
31 25 30 jcai ⊢ ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) = 0 ) → ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) )
32 24 31 syldan ⊢ ( ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) → ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) )
33 32 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) )
34 23 33 sylbi ⊢ ( ( ∪ 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) )
35 34 ancoms ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) )
36 fzfi ⊢ ( 1 ... 𝑚 ) ∈ Fin
37 fzssuz ⊢ ( 1 ... 𝑚 ) ⊆ ( ℤ≥ ‘ 1 )
38 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
39 37 38 sseqtrri ⊢ ( 1 ... 𝑚 ) ⊆ ℕ
40 fof ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → 𝑔 : ℕ ⟶ 𝐴 )
41 40 ffvelrnda ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ 𝑙 ∈ ℕ ) → ( 𝑔 ‘ 𝑙 ) ∈ 𝐴 )
42 eleq1 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑙 ) → ( 𝑥 ∈ dom vol ↔ ( 𝑔 ‘ 𝑙 ) ∈ dom vol ) )
43 fveqeq2 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑙 ) → ( ( vol ‘ 𝑥 ) = 0 ↔ ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 ) )
44 42 43 anbi12d ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑙 ) → ( ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑔 ‘ 𝑙 ) ∈ dom vol ∧ ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 ) ) )
45 44 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ∧ ( 𝑔 ‘ 𝑙 ) ∈ 𝐴 ) → ( ( 𝑔 ‘ 𝑙 ) ∈ dom vol ∧ ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 ) )
46 45 simpld ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ∧ ( 𝑔 ‘ 𝑙 ) ∈ 𝐴 ) → ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
47 46 ancoms ⊢ ( ( ( 𝑔 ‘ 𝑙 ) ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
48 41 47 sylan ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ 𝑙 ∈ ℕ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
49 48 an32s ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑙 ∈ ℕ ) → ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
50 49 ralrimiva ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∀ 𝑙 ∈ ℕ ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
51 ssralv ⊢ ( ( 1 ... 𝑚 ) ⊆ ℕ → ( ∀ 𝑙 ∈ ℕ ( 𝑔 ‘ 𝑙 ) ∈ dom vol → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ dom vol ) )
52 39 50 51 mpsyl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
53 finiunmbl ⊢ ( ( ( 1 ... 𝑚 ) ∈ Fin ∧ ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ dom vol ) → ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
54 36 52 53 sylancr ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
55 54 adantr ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ dom vol )
56 55 fmpttd ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) : ℕ ⟶ dom vol )
57 fzssp1 ⊢ ( 1 ... 𝑛 ) ⊆ ( 1 ... ( 𝑛 + 1 ) )
58 iunss1 ⊢ ( ( 1 ... 𝑛 ) ⊆ ( 1 ... ( 𝑛 + 1 ) ) → ∪ 𝑙 ∈ ( 1 ... 𝑛 ) ( 𝑔 ‘ 𝑙 ) ⊆ ∪ 𝑙 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑔 ‘ 𝑙 ) )
59 57 58 ax-mp ⊢ ∪ 𝑙 ∈ ( 1 ... 𝑛 ) ( 𝑔 ‘ 𝑙 ) ⊆ ∪ 𝑙 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑔 ‘ 𝑙 )
60 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 1 ... 𝑚 ) = ( 1 ... 𝑛 ) )
61 60 iuneq1d ⊢ ( 𝑚 = 𝑛 → ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) = ∪ 𝑙 ∈ ( 1 ... 𝑛 ) ( 𝑔 ‘ 𝑙 ) )
62 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) )
63 ovex ⊢ ( 1 ... 𝑛 ) ∈ V
64 fvex ⊢ ( 𝑔 ‘ 𝑙 ) ∈ V
65 63 64 iunex ⊢ ∪ 𝑙 ∈ ( 1 ... 𝑛 ) ( 𝑔 ‘ 𝑙 ) ∈ V
66 61 62 65 fvmpt ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) = ∪ 𝑙 ∈ ( 1 ... 𝑛 ) ( 𝑔 ‘ 𝑙 ) )
67 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
68 oveq2 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 1 ... 𝑚 ) = ( 1 ... ( 𝑛 + 1 ) ) )
69 68 iuneq1d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) = ∪ 𝑙 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑔 ‘ 𝑙 ) )
70 ovex ⊢ ( 1 ... ( 𝑛 + 1 ) ) ∈ V
71 70 64 iunex ⊢ ∪ 𝑙 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑔 ‘ 𝑙 ) ∈ V
72 69 62 71 fvmpt ⊢ ( ( 𝑛 + 1 ) ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) = ∪ 𝑙 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑔 ‘ 𝑙 ) )
73 67 72 syl ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) = ∪ 𝑙 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑔 ‘ 𝑙 ) )
74 66 73 sseq12d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) ↔ ∪ 𝑙 ∈ ( 1 ... 𝑛 ) ( 𝑔 ‘ 𝑙 ) ⊆ ∪ 𝑙 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑔 ‘ 𝑙 ) ) )
75 59 74 mpbiri ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) )
76 75 rgen ⊢ ∀ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) )
77 nnex ⊢ ℕ ∈ V
78 77 mptex ⊢ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ V
79 feq1 ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( 𝑓 : ℕ ⟶ dom vol ↔ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) : ℕ ⟶ dom vol ) )
80 fveq1 ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( 𝑓 ‘ 𝑛 ) = ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) )
81 fveq1 ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( 𝑓 ‘ ( 𝑛 + 1 ) ) = ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) )
82 80 81 sseq12d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( ( 𝑓 ‘ 𝑛 ) ⊆ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ↔ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) ) )
83 82 ralbidv ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ⊆ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) ) )
84 79 83 anbi12d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( ( 𝑓 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ⊆ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) ) ) )
85 rneq ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ran 𝑓 = ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
86 85 unieqd ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ∪ ran 𝑓 = ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
87 86 fveq2d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( vol ‘ ∪ ran 𝑓 ) = ( vol ‘ ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) )
88 85 imaeq2d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( vol “ ran 𝑓 ) = ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) )
89 88 supeq1d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → sup ( ( vol “ ran 𝑓 ) , ℝ* , < ) = sup ( ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) , ℝ* , < ) )
90 87 89 eqeq12d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( ( vol ‘ ∪ ran 𝑓 ) = sup ( ( vol “ ran 𝑓 ) , ℝ* , < ) ↔ ( vol ‘ ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = sup ( ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) , ℝ* , < ) ) )
91 84 90 imbi12d ⊢ ( 𝑓 = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) → ( ( ( 𝑓 : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ⊆ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) → ( vol ‘ ∪ ran 𝑓 ) = sup ( ( vol “ ran 𝑓 ) , ℝ* , < ) ) ↔ ( ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) ) → ( vol ‘ ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = sup ( ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) , ℝ* , < ) ) ) )
92 78 91 1 vtocl ⊢ ( ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) : ℕ ⟶ dom vol ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ 𝑛 ) ⊆ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ‘ ( 𝑛 + 1 ) ) ) → ( vol ‘ ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = sup ( ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) , ℝ* , < ) )
93 56 76 92 sylancl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( vol ‘ ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = sup ( ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) , ℝ* , < ) )
94 df-iun ⊢ ∪ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) = { 𝑛 ∣ ∃ 𝑥 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) }
95 eluzfz2 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) → 𝑥 ∈ ( 1 ... 𝑥 ) )
96 95 38 eleq2s ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ( 1 ... 𝑥 ) )
97 fveq2 ⊢ ( 𝑙 = 𝑥 → ( 𝑔 ‘ 𝑙 ) = ( 𝑔 ‘ 𝑥 ) )
98 97 eleq2d ⊢ ( 𝑙 = 𝑥 → ( 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) ↔ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) ) )
99 98 rspcev ⊢ ( ( 𝑥 ∈ ( 1 ... 𝑥 ) ∧ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) ) → ∃ 𝑙 ∈ ( 1 ... 𝑥 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
100 96 99 sylan ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) ) → ∃ 𝑙 ∈ ( 1 ... 𝑥 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
101 oveq2 ⊢ ( 𝑚 = 𝑥 → ( 1 ... 𝑚 ) = ( 1 ... 𝑥 ) )
102 101 rexeqdv ⊢ ( 𝑚 = 𝑥 → ( ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) ↔ ∃ 𝑙 ∈ ( 1 ... 𝑥 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) ) )
103 102 rspcev ⊢ ( ( 𝑥 ∈ ℕ ∧ ∃ 𝑙 ∈ ( 1 ... 𝑥 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) ) → ∃ 𝑚 ∈ ℕ ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
104 100 103 syldan ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) ) → ∃ 𝑚 ∈ ℕ ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
105 104 rexlimiva ⊢ ( ∃ 𝑥 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) → ∃ 𝑚 ∈ ℕ ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
106 ssrexv ⊢ ( ( 1 ... 𝑚 ) ⊆ ℕ → ( ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) → ∃ 𝑙 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) ) )
107 39 106 ax-mp ⊢ ( ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) → ∃ 𝑙 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
108 98 cbvrexvw ⊢ ( ∃ 𝑙 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) ↔ ∃ 𝑥 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) )
109 107 108 sylib ⊢ ( ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) → ∃ 𝑥 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) )
110 109 rexlimivw ⊢ ( ∃ 𝑚 ∈ ℕ ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) → ∃ 𝑥 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) )
111 105 110 impbii ⊢ ( ∃ 𝑥 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
112 eliun ⊢ ( 𝑛 ∈ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ↔ ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
113 112 rexbii ⊢ ( ∃ 𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑙 ∈ ( 1 ... 𝑚 ) 𝑛 ∈ ( 𝑔 ‘ 𝑙 ) )
114 111 113 bitr4i ⊢ ( ∃ 𝑥 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) ↔ ∃ 𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) )
115 114 abbii ⊢ { 𝑛 ∣ ∃ 𝑥 ∈ ℕ 𝑛 ∈ ( 𝑔 ‘ 𝑥 ) } = { 𝑛 ∣ ∃ 𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) }
116 94 115 eqtri ⊢ ∪ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) = { 𝑛 ∣ ∃ 𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) }
117 df-iun ⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) = { 𝑛 ∣ ∃ 𝑚 ∈ ℕ 𝑛 ∈ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) }
118 ovex ⊢ ( 1 ... 𝑚 ) ∈ V
119 118 64 iunex ⊢ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ V
120 119 dfiun3 ⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) = ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) )
121 116 117 120 3eqtr2i ⊢ ∪ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) = ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) )
122 fofn ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → 𝑔 Fn ℕ )
123 fniunfv ⊢ ( 𝑔 Fn ℕ → ∪ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) = ∪ ran 𝑔 )
124 122 123 syl ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∪ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) = ∪ ran 𝑔 )
125 forn ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ran 𝑔 = 𝐴 )
126 125 unieqd ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∪ ran 𝑔 = ∪ 𝐴 )
127 124 126 eqtrd ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∪ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) = ∪ 𝐴 )
128 121 127 eqtr3id ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = ∪ 𝐴 )
129 128 fveq2d ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( vol ‘ ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol ‘ ∪ 𝐴 ) )
130 129 adantr ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( vol ‘ ∪ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol ‘ ∪ 𝐴 ) )
131 rnco2 ⊢ ran ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
132 eqidd ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
133 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
134 133 a1i ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → vol : dom vol ⟶ ( 0 [,] +∞ ) )
135 134 feqmptd ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → vol = ( 𝑛 ∈ dom vol ↦ ( vol ‘ 𝑛 ) ) )
136 fveq2 ⊢ ( 𝑛 = ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) → ( vol ‘ 𝑛 ) = ( vol ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
137 55 132 135 136 fmptco ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( vol ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) )
138 mblvol ⊢ ( ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ dom vol → ( vol ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
139 55 138 syl ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
140 mblss ⊢ ( 𝑥 ∈ dom vol → 𝑥 ⊆ ℝ )
141 140 adantr ⊢ ( ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) → 𝑥 ⊆ ℝ )
142 26 eqeq1d ⊢ ( 𝑥 ∈ dom vol → ( ( vol ‘ 𝑥 ) = 0 ↔ ( vol* ‘ 𝑥 ) = 0 ) )
143 0re ⊢ 0 ∈ ℝ
144 eleq1a ⊢ ( 0 ∈ ℝ → ( ( vol* ‘ 𝑥 ) = 0 → ( vol* ‘ 𝑥 ) ∈ ℝ ) )
145 143 144 ax-mp ⊢ ( ( vol* ‘ 𝑥 ) = 0 → ( vol* ‘ 𝑥 ) ∈ ℝ )
146 142 145 syl6bi ⊢ ( 𝑥 ∈ dom vol → ( ( vol ‘ 𝑥 ) = 0 → ( vol* ‘ 𝑥 ) ∈ ℝ ) )
147 146 imp ⊢ ( ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) → ( vol* ‘ 𝑥 ) ∈ ℝ )
148 141 147 jca ⊢ ( ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) → ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) )
149 148 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) )
150 149 adantl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) )
151 ssid ⊢ ℕ ⊆ ℕ
152 sseq1 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑙 ) → ( 𝑥 ⊆ ℝ ↔ ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ) )
153 fveq2 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑙 ) → ( vol* ‘ 𝑥 ) = ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) )
154 153 eleq1d ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑙 ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ ↔ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) )
155 152 154 anbi12d ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑙 ) → ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ↔ ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) ) )
156 155 ralima ⊢ ( ( 𝑔 Fn ℕ ∧ ℕ ⊆ ℕ ) → ( ∀ 𝑥 ∈ ( 𝑔 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ↔ ∀ 𝑙 ∈ ℕ ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) ) )
157 122 151 156 sylancl ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ ( 𝑔 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ↔ ∀ 𝑙 ∈ ℕ ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) ) )
158 foima ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( 𝑔 “ ℕ ) = 𝐴 )
159 158 raleqdv ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ ( 𝑔 “ ℕ ) ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) )
160 157 159 bitr3d ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑙 ∈ ℕ ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) )
161 160 adantr ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( ∀ 𝑙 ∈ ℕ ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) )
162 150 161 mpbird ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∀ 𝑙 ∈ ℕ ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) )
163 ssralv ⊢ ( ( 1 ... 𝑚 ) ⊆ ℕ → ( ∀ 𝑙 ∈ ℕ ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) ) )
164 39 162 163 mpsyl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) )
165 164 adantr ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) )
166 ovolfiniun ⊢ ( ( ( 1 ... 𝑚 ) ∈ Fin ∧ ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ≤ Σ 𝑙 ∈ ( 1 ... 𝑚 ) ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) )
167 36 165 166 sylancr ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ≤ Σ 𝑙 ∈ ( 1 ... 𝑚 ) ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) )
168 mblvol ⊢ ( ( 𝑔 ‘ 𝑙 ) ∈ dom vol → ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) )
169 49 168 syl ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑙 ∈ ℕ ) → ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) )
170 45 simprd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ∧ ( 𝑔 ‘ 𝑙 ) ∈ 𝐴 ) → ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
171 41 170 sylan2 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ∧ ( 𝑔 : ℕ –onto→ 𝐴 ∧ 𝑙 ∈ ℕ ) ) → ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
172 171 ancoms ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ 𝑙 ∈ ℕ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
173 172 an32s ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑙 ∈ ℕ ) → ( vol ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
174 169 173 eqtr3d ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑙 ∈ ℕ ) → ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
175 174 ralrimiva ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∀ 𝑙 ∈ ℕ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
176 ssralv ⊢ ( ( 1 ... 𝑚 ) ⊆ ℕ → ( ∀ 𝑙 ∈ ℕ ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 ) )
177 39 175 176 mpsyl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
178 177 adantr ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
179 178 sumeq2d ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → Σ 𝑙 ∈ ( 1 ... 𝑚 ) ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) = Σ 𝑙 ∈ ( 1 ... 𝑚 ) 0 )
180 36 olci ⊢ ( ( 1 ... 𝑚 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... 𝑚 ) ∈ Fin )
181 sumz ⊢ ( ( ( 1 ... 𝑚 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... 𝑚 ) ∈ Fin ) → Σ 𝑙 ∈ ( 1 ... 𝑚 ) 0 = 0 )
182 180 181 ax-mp ⊢ Σ 𝑙 ∈ ( 1 ... 𝑚 ) 0 = 0
183 179 182 eqtrdi ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → Σ 𝑙 ∈ ( 1 ... 𝑚 ) ( vol* ‘ ( 𝑔 ‘ 𝑙 ) ) = 0 )
184 167 183 breqtrd ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ≤ 0 )
185 mblss ⊢ ( ( 𝑔 ‘ 𝑙 ) ∈ dom vol → ( 𝑔 ‘ 𝑙 ) ⊆ ℝ )
186 185 ralimi ⊢ ( ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ∈ dom vol → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ⊆ ℝ )
187 52 186 syl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ⊆ ℝ )
188 iunss ⊢ ( ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ⊆ ℝ ↔ ∀ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ⊆ ℝ )
189 187 188 sylibr ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ⊆ ℝ )
190 189 adantr ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ⊆ ℝ )
191 ovolge0 ⊢ ( ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ⊆ ℝ → 0 ≤ ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
192 190 191 syl ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → 0 ≤ ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) )
193 ovolcl ⊢ ( ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ⊆ ℝ → ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ* )
194 189 193 syl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ* )
195 194 adantr ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ* )
196 0xr ⊢ 0 ∈ ℝ*
197 xrletri3 ⊢ ( ( ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = 0 ↔ ( ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ≤ 0 ∧ 0 ≤ ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ) )
198 195 196 197 sylancl ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ( ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = 0 ↔ ( ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ≤ 0 ∧ 0 ≤ ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) ) )
199 184 192 198 mpbir2and ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = 0 )
200 139 199 eqtrd ⊢ ( ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) = 0 )
201 200 mpteq2dva ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( 𝑚 ∈ ℕ ↦ ( vol ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( 𝑚 ∈ ℕ ↦ 0 ) )
202 fconstmpt ⊢ ( ℕ × { 0 } ) = ( 𝑚 ∈ ℕ ↦ 0 )
203 201 202 eqtr4di ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( 𝑚 ∈ ℕ ↦ ( vol ‘ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( ℕ × { 0 } ) )
204 137 203 eqtrd ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( ℕ × { 0 } ) )
205 frn ⊢ ( ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) : ℕ ⟶ dom vol → ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ dom vol )
206 ffn ⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → vol Fn dom vol )
207 133 206 ax-mp ⊢ vol Fn dom vol
208 119 62 fnmpti ⊢ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) Fn ℕ
209 fnco ⊢ ( ( vol Fn dom vol ∧ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) Fn ℕ ∧ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ dom vol ) → ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) Fn ℕ )
210 207 208 209 mp3an12 ⊢ ( ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ⊆ dom vol → ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) Fn ℕ )
211 56 205 210 3syl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) Fn ℕ )
212 1nn ⊢ 1 ∈ ℕ
213 212 ne0ii ⊢ ℕ ≠ ∅
214 fconst5 ⊢ ( ( ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) Fn ℕ ∧ ℕ ≠ ∅ ) → ( ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( ℕ × { 0 } ) ↔ ran ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = { 0 } ) )
215 211 213 214 sylancl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = ( ℕ × { 0 } ) ↔ ran ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = { 0 } ) )
216 204 215 mpbid ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ran ( vol ∘ ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = { 0 } )
217 131 216 eqtr3id ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) = { 0 } )
218 217 supeq1d ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → sup ( ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < ) )
219 xrltso ⊢ < Or ℝ*
220 supsn ⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
221 219 196 220 mp2an ⊢ sup ( { 0 } , ℝ* , < ) = 0
222 218 221 eqtrdi ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → sup ( ( vol “ ran ( 𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ ( 1 ... 𝑚 ) ( 𝑔 ‘ 𝑙 ) ) ) , ℝ* , < ) = 0 )
223 93 130 222 3eqtr3rd ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) ) → 0 = ( vol ‘ ∪ 𝐴 ) )
224 223 ex ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom vol ∧ ( vol ‘ 𝑥 ) = 0 ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
225 35 224 syl5 ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
226 225 exlimiv ⊢ ( ∃ 𝑔 𝑔 : ℕ –onto→ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
227 19 226 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ ) → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
228 227 expimpd ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol ‘ ∪ 𝐴 ) ) )
229 12 228 pm2.61ine ⊢ ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → 0 = ( vol ‘ ∪ 𝐴 ) )
230 renepnf ⊢ ( 0 ∈ ℝ → 0 ≠ +∞ )
231 143 230 mp1i ⊢ ( ∪ 𝐴 = ℝ → 0 ≠ +∞ )
232 fveq2 ⊢ ( ∪ 𝐴 = ℝ → ( vol ‘ ∪ 𝐴 ) = ( vol ‘ ℝ ) )
233 rembl ⊢ ℝ ∈ dom vol
234 mblvol ⊢ ( ℝ ∈ dom vol → ( vol ‘ ℝ ) = ( vol* ‘ ℝ ) )
235 233 234 ax-mp ⊢ ( vol ‘ ℝ ) = ( vol* ‘ ℝ )
236 ovolre ⊢ ( vol* ‘ ℝ ) = +∞
237 235 236 eqtri ⊢ ( vol ‘ ℝ ) = +∞
238 232 237 eqtrdi ⊢ ( ∪ 𝐴 = ℝ → ( vol ‘ ∪ 𝐴 ) = +∞ )
239 231 238 neeqtrrd ⊢ ( ∪ 𝐴 = ℝ → 0 ≠ ( vol ‘ ∪ 𝐴 ) )
240 239 necon2i ⊢ ( 0 = ( vol ‘ ∪ 𝐴 ) → ∪ 𝐴 ≠ ℝ )
241 229 240 syl ⊢ ( ( 𝐴 ≼ ℕ ∧ ( ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴 ⊆ ℝ ) ) → ∪ 𝐴 ≠ ℝ )
242 241 expr ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ( ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ ) )
243 eqimss ⊢ ( ∪ 𝐴 = ℝ → ∪ 𝐴 ⊆ ℝ )
244 243 necon3bi ⊢ ( ¬ ∪ 𝐴 ⊆ ℝ → ∪ 𝐴 ≠ ℝ )
245 242 244 pm2.61d1 ⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∪ 𝐴 ≠ ℝ )