Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  volsupnfl Structured version   Visualization version   GIF version

Theorem volsupnfl 35095
 Description: volsup 24163 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.)
Hypothesis
Ref Expression
volsupnfl.0 ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ))
Assertion
Ref Expression
volsupnfl ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
Distinct variable group:   𝑓,𝑛,𝑥,𝐴

Proof of Theorem volsupnfl
Dummy variables 𝑔 𝑚 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 4814 . . . . . . . . 9 (𝐴 = ∅ → 𝐴 = ∅)
2 uni0 4831 . . . . . . . . 9 ∅ = ∅
31, 2eqtrdi 2852 . . . . . . . 8 (𝐴 = ∅ → 𝐴 = ∅)
43fveq2d 6653 . . . . . . 7 (𝐴 = ∅ → (vol‘ 𝐴) = (vol‘∅))
5 0mbl 24146 . . . . . . . . 9 ∅ ∈ dom vol
6 mblvol 24137 . . . . . . . . 9 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
75, 6ax-mp 5 . . . . . . . 8 (vol‘∅) = (vol*‘∅)
8 ovol0 24100 . . . . . . . 8 (vol*‘∅) = 0
97, 8eqtri 2824 . . . . . . 7 (vol‘∅) = 0
104, 9eqtr2di 2853 . . . . . 6 (𝐴 = ∅ → 0 = (vol‘ 𝐴))
1110a1d 25 . . . . 5 (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
12 reldom 8502 . . . . . . . . . . 11 Rel ≼
1312brrelex1i 5576 . . . . . . . . . 10 (𝐴 ≼ ℕ → 𝐴 ∈ V)
14 0sdomg 8634 . . . . . . . . . 10 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1513, 14syl 17 . . . . . . . . 9 (𝐴 ≼ ℕ → (∅ ≺ 𝐴𝐴 ≠ ∅))
1615biimparc 483 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17 fodomr 8656 . . . . . . . 8 ((∅ ≺ 𝐴𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
1816, 17sylancom 591 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
19 unissb 4835 . . . . . . . . . . . . 13 ( 𝐴 ⊆ ℝ ↔ ∀𝑥𝐴 𝑥 ⊆ ℝ)
2019anbi1i 626 . . . . . . . . . . . 12 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
21 r19.26 3140 . . . . . . . . . . . 12 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
2220, 21bitr4i 281 . . . . . . . . . . 11 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23 ovolctb2 24099 . . . . . . . . . . . . 13 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24 nulmbl 24142 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 𝑥 ∈ dom vol)
25 mblvol 24137 . . . . . . . . . . . . . . . 16 (𝑥 ∈ dom vol → (vol‘𝑥) = (vol*‘𝑥))
26 eqtr 2821 . . . . . . . . . . . . . . . . 17 (((vol‘𝑥) = (vol*‘𝑥) ∧ (vol*‘𝑥) = 0) → (vol‘𝑥) = 0)
2726expcom 417 . . . . . . . . . . . . . . . 16 ((vol*‘𝑥) = 0 → ((vol‘𝑥) = (vol*‘𝑥) → (vol‘𝑥) = 0))
2825, 27syl5 34 . . . . . . . . . . . . . . 15 ((vol*‘𝑥) = 0 → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
2928adantl 485 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
3024, 29jcai 520 . . . . . . . . . . . . 13 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3123, 30syldan 594 . . . . . . . . . . . 12 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3231ralimi 3131 . . . . . . . . . . 11 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3322, 32sylbi 220 . . . . . . . . . 10 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3433ancoms 462 . . . . . . . . 9 ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
35 fzfi 13339 . . . . . . . . . . . . . . 15 (1...𝑚) ∈ Fin
36 fzssuz 12947 . . . . . . . . . . . . . . . . 17 (1...𝑚) ⊆ (ℤ‘1)
37 nnuz 12273 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
3836, 37sseqtrri 3955 . . . . . . . . . . . . . . . 16 (1...𝑚) ⊆ ℕ
39 fof 6569 . . . . . . . . . . . . . . . . . . . 20 (𝑔:ℕ–onto𝐴𝑔:ℕ⟶𝐴)
4039ffvelrnda 6832 . . . . . . . . . . . . . . . . . . 19 ((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) → (𝑔𝑙) ∈ 𝐴)
41 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑔𝑙) → (𝑥 ∈ dom vol ↔ (𝑔𝑙) ∈ dom vol))
42 fveqeq2 6658 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑔𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔𝑙)) = 0))
4341, 42anbi12d 633 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑔𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔𝑙) ∈ dom vol ∧ (vol‘(𝑔𝑙)) = 0)))
4443rspccva 3573 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → ((𝑔𝑙) ∈ dom vol ∧ (vol‘(𝑔𝑙)) = 0))
4544simpld 498 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → (𝑔𝑙) ∈ dom vol)
4645ancoms 462 . . . . . . . . . . . . . . . . . . 19 (((𝑔𝑙) ∈ 𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔𝑙) ∈ dom vol)
4740, 46sylan 583 . . . . . . . . . . . . . . . . . 18 (((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔𝑙) ∈ dom vol)
4847an32s 651 . . . . . . . . . . . . . . . . 17 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔𝑙) ∈ dom vol)
4948ralrimiva 3152 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔𝑙) ∈ dom vol)
50 ssralv 3984 . . . . . . . . . . . . . . . 16 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (𝑔𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol))
5138, 49, 50mpsyl 68 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
52 finiunmbl 24151 . . . . . . . . . . . . . . 15 (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5335, 51, 52sylancr 590 . . . . . . . . . . . . . 14 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5453adantr 484 . . . . . . . . . . . . 13 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5554fmpttd 6860 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol)
56 fzssp1 12949 . . . . . . . . . . . . . . 15 (1...𝑛) ⊆ (1...(𝑛 + 1))
57 iunss1 4898 . . . . . . . . . . . . . . 15 ((1...𝑛) ⊆ (1...(𝑛 + 1)) → 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
5856, 57ax-mp 5 . . . . . . . . . . . . . 14 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙)
59 oveq2 7147 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
6059iuneq1d 4911 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) = 𝑙 ∈ (1...𝑛)(𝑔𝑙))
61 eqid 2801 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
62 ovex 7172 . . . . . . . . . . . . . . . . 17 (1...𝑛) ∈ V
63 fvex 6662 . . . . . . . . . . . . . . . . 17 (𝑔𝑙) ∈ V
6462, 63iunex 7655 . . . . . . . . . . . . . . . 16 𝑙 ∈ (1...𝑛)(𝑔𝑙) ∈ V
6560, 61, 64fvmpt 6749 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) = 𝑙 ∈ (1...𝑛)(𝑔𝑙))
66 peano2nn 11641 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
67 oveq2 7147 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1)))
6867iuneq1d 4911 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 + 1) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
69 ovex 7172 . . . . . . . . . . . . . . . . . 18 (1...(𝑛 + 1)) ∈ V
7069, 63iunex 7655 . . . . . . . . . . . . . . . . 17 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙) ∈ V
7168, 61, 70fvmpt 6749 . . . . . . . . . . . . . . . 16 ((𝑛 + 1) ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
7266, 71syl 17 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
7365, 72sseq12d 3951 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) ↔ 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙)))
7458, 73mpbiri 261 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))
7574rgen 3119 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))
76 nnex 11635 . . . . . . . . . . . . . 14 ℕ ∈ V
7776mptex 6967 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ V
78 feq1 6472 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol))
79 fveq1 6648 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓𝑛) = ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛))
80 fveq1 6648 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))
8179, 80sseq12d 3951 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))))
8281ralbidv 3165 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))))
8378, 82anbi12d 633 . . . . . . . . . . . . . 14 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))))
84 rneq 5774 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
8584unieqd 4817 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
8685fveq2d 6653 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (vol‘ ran 𝑓) = (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
8784imaeq2d 5900 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
8887supeq1d 8898 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → sup((vol “ ran 𝑓), ℝ*, < ) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
8986, 88eqeq12d 2817 . . . . . . . . . . . . . 14 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ) ↔ (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < )))
9083, 89imbi12d 348 . . . . . . . . . . . . 13 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < )) ↔ (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))))
91 volsupnfl.0 . . . . . . . . . . . . 13 ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ))
9277, 90, 91vtocl 3510 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
9355, 75, 92sylancl 589 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
94 df-iun 4886 . . . . . . . . . . . . . . . 16 𝑥 ∈ ℕ (𝑔𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥)}
95 eluzfz2 12914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (ℤ‘1) → 𝑥 ∈ (1...𝑥))
9695, 37eleq2s 2911 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥))
97 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = 𝑥 → (𝑔𝑙) = (𝑔𝑥))
9897eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑥 → (𝑛 ∈ (𝑔𝑙) ↔ 𝑛 ∈ (𝑔𝑥)))
9998rspcev 3574 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙))
10096, 99sylan 583 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙))
101 oveq2 7147 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
102101rexeqdv 3368 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙)))
103102rspcev 3574 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
104100, 103syldan 594 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
105104rexlimiva 3243 . . . . . . . . . . . . . . . . . . 19 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
106 ssrexv 3985 . . . . . . . . . . . . . . . . . . . . . 22 ((1...𝑚) ⊆ ℕ → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙)))
10738, 106ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙))
10898cbvrexvw 3400 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
109107, 108sylib 221 . . . . . . . . . . . . . . . . . . . 20 (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
110109rexlimivw 3244 . . . . . . . . . . . . . . . . . . 19 (∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
111105, 110impbii 212 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
112 eliun 4888 . . . . . . . . . . . . . . . . . . 19 (𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
113112rexbii 3213 . . . . . . . . . . . . . . . . . 18 (∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
114111, 113bitr4i 281 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙))
115114abbii 2866 . . . . . . . . . . . . . . . 16 {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
11694, 115eqtri 2824 . . . . . . . . . . . . . . 15 𝑥 ∈ ℕ (𝑔𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
117 df-iun 4886 . . . . . . . . . . . . . . 15 𝑚 ∈ ℕ 𝑙 ∈ (1...𝑚)(𝑔𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
118 ovex 7172 . . . . . . . . . . . . . . . . 17 (1...𝑚) ∈ V
119118, 63iunex 7655 . . . . . . . . . . . . . . . 16 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ V
120119dfiun3 5806 . . . . . . . . . . . . . . 15 𝑚 ∈ ℕ 𝑙 ∈ (1...𝑚)(𝑔𝑙) = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
121116, 117, 1203eqtr2i 2830 . . . . . . . . . . . . . 14 𝑥 ∈ ℕ (𝑔𝑥) = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
122 fofn 6571 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴𝑔 Fn ℕ)
123 fniunfv 6988 . . . . . . . . . . . . . . . 16 (𝑔 Fn ℕ → 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
124122, 123syl 17 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
125 forn 6572 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴 → ran 𝑔 = 𝐴)
126125unieqd 4817 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 ran 𝑔 = 𝐴)
127124, 126eqtrd 2836 . . . . . . . . . . . . . 14 (𝑔:ℕ–onto𝐴 𝑥 ∈ ℕ (𝑔𝑥) = 𝐴)
128121, 127syl5eqr 2850 . . . . . . . . . . . . 13 (𝑔:ℕ–onto𝐴 ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 𝐴)
129128fveq2d 6653 . . . . . . . . . . . 12 (𝑔:ℕ–onto𝐴 → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol‘ 𝐴))
130129adantr 484 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol‘ 𝐴))
131 rnco2 6077 . . . . . . . . . . . . . 14 ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
132 eqidd 2802 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
133 volf 24136 . . . . . . . . . . . . . . . . . . 19 vol:dom vol⟶(0[,]+∞)
134133a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom vol⟶(0[,]+∞))
135134feqmptd 6712 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦ (vol‘𝑛)))
136 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑙 ∈ (1...𝑚)(𝑔𝑙) → (vol‘𝑛) = (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
13754, 132, 135, 136fmptco 6872 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
138 mblvol 24137 . . . . . . . . . . . . . . . . . . . 20 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
13954, 138syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
140 mblss 24138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
141140adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 𝑥 ⊆ ℝ)
14225eqeq1d 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 ↔ (vol*‘𝑥) = 0))
143 0re 10636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 0 ∈ ℝ
144 eleq1a 2888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 ∈ ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
145143, 144ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)
146142, 145syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
147146imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (vol*‘𝑥) ∈ ℝ)
148141, 147jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
149148ralimi 3131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
150149adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
151 ssid 3940 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℕ ⊆ ℕ
152 sseq1 3943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑔𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔𝑙) ⊆ ℝ))
153 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝑔𝑙) → (vol*‘𝑥) = (vol*‘(𝑔𝑙)))
154153eleq1d 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑔𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔𝑙)) ∈ ℝ))
155152, 154anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝑔𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
156155ralima 6982 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
157122, 151, 156sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
158 foima 6574 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔:ℕ–onto𝐴 → (𝑔 “ ℕ) = 𝐴)
159158raleqdv 3367 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
160157, 159bitr3d 284 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:ℕ–onto𝐴 → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
161160adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
162150, 161mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
163 ssralv 3984 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
16438, 162, 163mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
165164adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
166 ovolfiniun 24108 . . . . . . . . . . . . . . . . . . . . . 22 (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)))
16735, 165, 166sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)))
168 mblvol 24137 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑙) ∈ dom vol → (vol‘(𝑔𝑙)) = (vol*‘(𝑔𝑙)))
16948, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔𝑙)) = (vol*‘(𝑔𝑙)))
17044simprd 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → (vol‘(𝑔𝑙)) = 0)
17140, 170sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto𝐴𝑙 ∈ ℕ)) → (vol‘(𝑔𝑙)) = 0)
172171ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔𝑙)) = 0)
173172an32s 651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔𝑙)) = 0)
174169, 173eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔𝑙)) = 0)
175174ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (vol*‘(𝑔𝑙)) = 0)
176 ssralv 3984 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (vol*‘(𝑔𝑙)) = 0 → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0))
17738, 175, 176mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
178177adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
179178sumeq2d 15054 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = Σ𝑙 ∈ (1...𝑚)0)
18035olci 863 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑚) ⊆ (ℤ‘1) ∨ (1...𝑚) ∈ Fin)
181 sumz 15074 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑚) ⊆ (ℤ‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0)
182180, 181ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑙 ∈ (1...𝑚)0 = 0
183179, 182eqtrdi 2852 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
184167, 183breqtrd 5059 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0)
185 mblss 24138 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑙) ∈ dom vol → (𝑔𝑙) ⊆ ℝ)
186185ralimi 3131 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
18751, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
188 iunss 4935 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
189187, 188sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
190189adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
191 ovolge0 24088 . . . . . . . . . . . . . . . . . . . . 21 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ → 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
193 ovolcl 24085 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
194189, 193syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
195194adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
196 0xr 10681 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℝ*
197 xrletri3 12539 . . . . . . . . . . . . . . . . . . . . 21 (((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0 ↔ ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))))
198195, 196, 197sylancl 589 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0 ↔ ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))))
199184, 192, 198mpbir2and 712 . . . . . . . . . . . . . . . . . . 19 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0)
200139, 199eqtrd 2836 . . . . . . . . . . . . . . . . . 18 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0)
201200mpteq2dva 5128 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ 0))
202 fconstmpt 5582 . . . . . . . . . . . . . . . . 17 (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
203201, 202eqtr4di 2854 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}))
204137, 203eqtrd 2836 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}))
205 frn 6497 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol)
206 ffn 6491 . . . . . . . . . . . . . . . . . . 19 (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
207133, 206ax-mp 5 . . . . . . . . . . . . . . . . . 18 vol Fn dom vol
208119, 61fnmpti 6467 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) Fn ℕ
209 fnco 6441 . . . . . . . . . . . . . . . . . 18 ((vol Fn dom vol ∧ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
210207, 208, 209mp3an12 1448 . . . . . . . . . . . . . . . . 17 (ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
21155, 205, 2103syl 18 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
212 1nn 11640 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
213212ne0ii 4256 . . . . . . . . . . . . . . . 16 ℕ ≠ ∅
214 fconst5 6949 . . . . . . . . . . . . . . . 16 (((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ ∧ ℕ ≠ ∅) → ((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0}))
215211, 213, 214sylancl 589 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0}))
216204, 215mpbid 235 . . . . . . . . . . . . . 14 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0})
217131, 216syl5eqr 2850 . . . . . . . . . . . . 13 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0})
218217supeq1d 8898 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ) = sup({0}, ℝ*, < ))
219 xrltso 12526 . . . . . . . . . . . . 13 < Or ℝ*
220 supsn 8924 . . . . . . . . . . . . 13 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
221219, 196, 220mp2an 691 . . . . . . . . . . . 12 sup({0}, ℝ*, < ) = 0
222218, 221eqtrdi 2852 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ) = 0)
22393, 130, 2223eqtr3rd 2845 . . . . . . . . . 10 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 0 = (vol‘ 𝐴))
224223ex 416 . . . . . . . . 9 (𝑔:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 = (vol‘ 𝐴)))
22534, 224syl5 34 . . . . . . . 8 (𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
226225exlimiv 1931 . . . . . . 7 (∃𝑔 𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
22718, 226syl 17 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
228227expimpd 457 . . . . 5 (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
22911, 228pm2.61ine 3073 . . . 4 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴))
230 renepnf 10682 . . . . . . 7 (0 ∈ ℝ → 0 ≠ +∞)
231143, 230mp1i 13 . . . . . 6 ( 𝐴 = ℝ → 0 ≠ +∞)
232 fveq2 6649 . . . . . . 7 ( 𝐴 = ℝ → (vol‘ 𝐴) = (vol‘ℝ))
233 rembl 24147 . . . . . . . . 9 ℝ ∈ dom vol
234 mblvol 24137 . . . . . . . . 9 (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
235233, 234ax-mp 5 . . . . . . . 8 (vol‘ℝ) = (vol*‘ℝ)
236 ovolre 24132 . . . . . . . 8 (vol*‘ℝ) = +∞
237235, 236eqtri 2824 . . . . . . 7 (vol‘ℝ) = +∞
238232, 237eqtrdi 2852 . . . . . 6 ( 𝐴 = ℝ → (vol‘ 𝐴) = +∞)
239231, 238neeqtrrd 3064 . . . . 5 ( 𝐴 = ℝ → 0 ≠ (vol‘ 𝐴))
240239necon2i 3024 . . . 4 (0 = (vol‘ 𝐴) → 𝐴 ≠ ℝ)
241229, 240syl 17 . . 3 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 𝐴 ≠ ℝ)
242241expr 460 . 2 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ( 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ))
243 eqimss 3974 . . 3 ( 𝐴 = ℝ → 𝐴 ⊆ ℝ)
244243necon3bi 3016 . 2 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ)
245242, 244pm2.61d1 183 1 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2112  {cab 2779   ≠ wne 2990  ∀wral 3109  ∃wrex 3110  Vcvv 3444   ⊆ wss 3884  ∅c0 4246  {csn 4528  ∪ cuni 4803  ∪ ciun 4884   class class class wbr 5033   ↦ cmpt 5113   Or wor 5441   × cxp 5521  dom cdm 5523  ran crn 5524   “ cima 5526   ∘ ccom 5527   Fn wfn 6323  ⟶wf 6324  –onto→wfo 6326  ‘cfv 6328  (class class class)co 7139   ≼ cdom 8494   ≺ csdm 8495  Fincfn 8496  supcsup 8892  ℝcr 10529  0cc0 10530  1c1 10531   + caddc 10533  +∞cpnf 10665  ℝ*cxr 10667   < clt 10668   ≤ cle 10669  ℕcn 11629  ℤ≥cuz 12235  [,]cicc 12733  ...cfz 12889  Σcsu 15037  vol*covol 24069  volcvol 24070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-sum 15038  df-rest 16691  df-topgen 16712  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-mopn 20090  df-top 21502  df-topon 21519  df-bases 21554  df-cmp 21995  df-ovol 24071  df-vol 24072 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator