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

Theorem volsupnfl 33787
Description: volsup 23544 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 4582 . . . . . . . . 9 (𝐴 = ∅ → 𝐴 = ∅)
2 uni0 4601 . . . . . . . . 9 ∅ = ∅
31, 2syl6eq 2821 . . . . . . . 8 (𝐴 = ∅ → 𝐴 = ∅)
43fveq2d 6336 . . . . . . 7 (𝐴 = ∅ → (vol‘ 𝐴) = (vol‘∅))
5 0mbl 23527 . . . . . . . . 9 ∅ ∈ dom vol
6 mblvol 23518 . . . . . . . . 9 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
75, 6ax-mp 5 . . . . . . . 8 (vol‘∅) = (vol*‘∅)
8 ovol0 23481 . . . . . . . 8 (vol*‘∅) = 0
97, 8eqtri 2793 . . . . . . 7 (vol‘∅) = 0
104, 9syl6req 2822 . . . . . 6 (𝐴 = ∅ → 0 = (vol‘ 𝐴))
1110a1d 25 . . . . 5 (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
12 reldom 8115 . . . . . . . . . . 11 Rel ≼
1312brrelexi 5298 . . . . . . . . . 10 (𝐴 ≼ ℕ → 𝐴 ∈ V)
14 0sdomg 8245 . . . . . . . . . 10 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1513, 14syl 17 . . . . . . . . 9 (𝐴 ≼ ℕ → (∅ ≺ 𝐴𝐴 ≠ ∅))
1615biimparc 465 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17 fodomr 8267 . . . . . . . 8 ((∅ ≺ 𝐴𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
1816, 17sylancom 576 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
19 unissb 4605 . . . . . . . . . . . . 13 ( 𝐴 ⊆ ℝ ↔ ∀𝑥𝐴 𝑥 ⊆ ℝ)
2019anbi1i 610 . . . . . . . . . . . 12 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
21 r19.26 3212 . . . . . . . . . . . 12 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
2220, 21bitr4i 267 . . . . . . . . . . 11 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23 ovolctb2 23480 . . . . . . . . . . . . 13 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24 nulmbl 23523 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 𝑥 ∈ dom vol)
25 mblvol 23518 . . . . . . . . . . . . . . . 16 (𝑥 ∈ dom vol → (vol‘𝑥) = (vol*‘𝑥))
26 eqtr 2790 . . . . . . . . . . . . . . . . 17 (((vol‘𝑥) = (vol*‘𝑥) ∧ (vol*‘𝑥) = 0) → (vol‘𝑥) = 0)
2726expcom 398 . . . . . . . . . . . . . . . 16 ((vol*‘𝑥) = 0 → ((vol‘𝑥) = (vol*‘𝑥) → (vol‘𝑥) = 0))
2825, 27syl5 34 . . . . . . . . . . . . . . 15 ((vol*‘𝑥) = 0 → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
2928adantl 467 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
3024, 29jcai 506 . . . . . . . . . . . . 13 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3123, 30syldan 579 . . . . . . . . . . . 12 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3231ralimi 3101 . . . . . . . . . . 11 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3322, 32sylbi 207 . . . . . . . . . 10 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3433ancoms 455 . . . . . . . . 9 ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
35 fzfi 12979 . . . . . . . . . . . . . . 15 (1...𝑚) ∈ Fin
36 fzssuz 12589 . . . . . . . . . . . . . . . . 17 (1...𝑚) ⊆ (ℤ‘1)
37 nnuz 11925 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
3836, 37sseqtr4i 3787 . . . . . . . . . . . . . . . 16 (1...𝑚) ⊆ ℕ
39 fof 6256 . . . . . . . . . . . . . . . . . . . 20 (𝑔:ℕ–onto𝐴𝑔:ℕ⟶𝐴)
4039ffvelrnda 6502 . . . . . . . . . . . . . . . . . . 19 ((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) → (𝑔𝑙) ∈ 𝐴)
41 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑔𝑙) → (𝑥 ∈ dom vol ↔ (𝑔𝑙) ∈ dom vol))
42 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑔𝑙) → (vol‘𝑥) = (vol‘(𝑔𝑙)))
4342eqeq1d 2773 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑔𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔𝑙)) = 0))
4441, 43anbi12d 616 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑔𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔𝑙) ∈ dom vol ∧ (vol‘(𝑔𝑙)) = 0)))
4544rspccva 3459 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → ((𝑔𝑙) ∈ dom vol ∧ (vol‘(𝑔𝑙)) = 0))
4645simpld 482 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → (𝑔𝑙) ∈ dom vol)
4746ancoms 455 . . . . . . . . . . . . . . . . . . 19 (((𝑔𝑙) ∈ 𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔𝑙) ∈ dom vol)
4840, 47sylan 569 . . . . . . . . . . . . . . . . . 18 (((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔𝑙) ∈ dom vol)
4948an32s 631 . . . . . . . . . . . . . . . . 17 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔𝑙) ∈ dom vol)
5049ralrimiva 3115 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔𝑙) ∈ dom vol)
51 ssralv 3815 . . . . . . . . . . . . . . . 16 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (𝑔𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol))
5238, 50, 51mpsyl 68 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
53 finiunmbl 23532 . . . . . . . . . . . . . . 15 (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5435, 52, 53sylancr 575 . . . . . . . . . . . . . 14 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5554adantr 466 . . . . . . . . . . . . 13 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
56 eqid 2771 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
5755, 56fmptd 6527 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol)
58 fzssp1 12591 . . . . . . . . . . . . . . 15 (1...𝑛) ⊆ (1...(𝑛 + 1))
59 iunss1 4666 . . . . . . . . . . . . . . 15 ((1...𝑛) ⊆ (1...(𝑛 + 1)) → 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
6058, 59ax-mp 5 . . . . . . . . . . . . . 14 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙)
61 oveq2 6801 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
6261iuneq1d 4679 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) = 𝑙 ∈ (1...𝑛)(𝑔𝑙))
63 ovex 6823 . . . . . . . . . . . . . . . . 17 (1...𝑛) ∈ V
64 fvex 6342 . . . . . . . . . . . . . . . . 17 (𝑔𝑙) ∈ V
6563, 64iunex 7294 . . . . . . . . . . . . . . . 16 𝑙 ∈ (1...𝑛)(𝑔𝑙) ∈ V
6662, 56, 65fvmpt 6424 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) = 𝑙 ∈ (1...𝑛)(𝑔𝑙))
67 peano2nn 11234 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
68 oveq2 6801 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1)))
6968iuneq1d 4679 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 + 1) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
70 ovex 6823 . . . . . . . . . . . . . . . . . 18 (1...(𝑛 + 1)) ∈ V
7170, 64iunex 7294 . . . . . . . . . . . . . . . . 17 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙) ∈ V
7269, 56, 71fvmpt 6424 . . . . . . . . . . . . . . . 16 ((𝑛 + 1) ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
7367, 72syl 17 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
7466, 73sseq12d 3783 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) ↔ 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙)))
7560, 74mpbiri 248 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))
7675rgen 3071 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))
77 nnex 11228 . . . . . . . . . . . . . 14 ℕ ∈ V
7877mptex 6630 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ V
79 feq1 6166 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol))
80 fveq1 6331 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓𝑛) = ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛))
81 fveq1 6331 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))
8280, 81sseq12d 3783 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))))
8382ralbidv 3135 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))))
8479, 83anbi12d 616 . . . . . . . . . . . . . 14 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))))
85 rneq 5489 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
8685unieqd 4584 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
8786fveq2d 6336 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (vol‘ ran 𝑓) = (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
8885imaeq2d 5607 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
8988supeq1d 8508 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → sup((vol “ ran 𝑓), ℝ*, < ) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
9087, 89eqeq12d 2786 . . . . . . . . . . . . . 14 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ) ↔ (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < )))
9184, 90imbi12d 333 . . . . . . . . . . . . 13 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < )) ↔ (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))))
92 volsupnfl.0 . . . . . . . . . . . . 13 ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ))
9378, 91, 92vtocl 3410 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
9457, 76, 93sylancl 574 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
95 df-iun 4656 . . . . . . . . . . . . . . . 16 𝑥 ∈ ℕ (𝑔𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥)}
96 eluzfz2 12556 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (ℤ‘1) → 𝑥 ∈ (1...𝑥))
9796, 37eleq2s 2868 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥))
98 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = 𝑥 → (𝑔𝑙) = (𝑔𝑥))
9998eleq2d 2836 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑥 → (𝑛 ∈ (𝑔𝑙) ↔ 𝑛 ∈ (𝑔𝑥)))
10099rspcev 3460 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙))
10197, 100sylan 569 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙))
102 oveq2 6801 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
103102rexeqdv 3294 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙)))
104103rspcev 3460 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
105101, 104syldan 579 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
106105rexlimiva 3176 . . . . . . . . . . . . . . . . . . 19 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
107 ssrexv 3816 . . . . . . . . . . . . . . . . . . . . . 22 ((1...𝑚) ⊆ ℕ → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙)))
10838, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙))
10999cbvrexv 3321 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
110108, 109sylib 208 . . . . . . . . . . . . . . . . . . . 20 (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
111110rexlimivw 3177 . . . . . . . . . . . . . . . . . . 19 (∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
112106, 111impbii 199 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
113 eliun 4658 . . . . . . . . . . . . . . . . . . 19 (𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
114113rexbii 3189 . . . . . . . . . . . . . . . . . 18 (∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
115112, 114bitr4i 267 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙))
116115abbii 2888 . . . . . . . . . . . . . . . 16 {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
11795, 116eqtri 2793 . . . . . . . . . . . . . . 15 𝑥 ∈ ℕ (𝑔𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
118 df-iun 4656 . . . . . . . . . . . . . . 15 𝑚 ∈ ℕ 𝑙 ∈ (1...𝑚)(𝑔𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
119 ovex 6823 . . . . . . . . . . . . . . . . 17 (1...𝑚) ∈ V
120119, 64iunex 7294 . . . . . . . . . . . . . . . 16 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ V
121120dfiun3 5518 . . . . . . . . . . . . . . 15 𝑚 ∈ ℕ 𝑙 ∈ (1...𝑚)(𝑔𝑙) = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
122117, 118, 1213eqtr2i 2799 . . . . . . . . . . . . . 14 𝑥 ∈ ℕ (𝑔𝑥) = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
123 fofn 6258 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴𝑔 Fn ℕ)
124 fniunfv 6648 . . . . . . . . . . . . . . . 16 (𝑔 Fn ℕ → 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
125123, 124syl 17 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
126 forn 6259 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴 → ran 𝑔 = 𝐴)
127126unieqd 4584 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 ran 𝑔 = 𝐴)
128125, 127eqtrd 2805 . . . . . . . . . . . . . 14 (𝑔:ℕ–onto𝐴 𝑥 ∈ ℕ (𝑔𝑥) = 𝐴)
129122, 128syl5eqr 2819 . . . . . . . . . . . . 13 (𝑔:ℕ–onto𝐴 ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 𝐴)
130129fveq2d 6336 . . . . . . . . . . . 12 (𝑔:ℕ–onto𝐴 → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol‘ 𝐴))
131130adantr 466 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol‘ 𝐴))
132 rnco2 5786 . . . . . . . . . . . . . 14 ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
133 eqidd 2772 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
134 volf 23517 . . . . . . . . . . . . . . . . . . 19 vol:dom vol⟶(0[,]+∞)
135134a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom vol⟶(0[,]+∞))
136135feqmptd 6391 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦ (vol‘𝑛)))
137 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑙 ∈ (1...𝑚)(𝑔𝑙) → (vol‘𝑛) = (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
13855, 133, 136, 137fmptco 6539 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
139 mblvol 23518 . . . . . . . . . . . . . . . . . . . 20 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
14055, 139syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
141 mblss 23519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
142141adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 𝑥 ⊆ ℝ)
14325eqeq1d 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 ↔ (vol*‘𝑥) = 0))
144 0re 10242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 0 ∈ ℝ
145 eleq1a 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 ∈ ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
146144, 145ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)
147143, 146syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
148147imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (vol*‘𝑥) ∈ ℝ)
149142, 148jca 501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
150149ralimi 3101 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
151150adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
152 ssid 3773 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℕ ⊆ ℕ
153 sseq1 3775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑔𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔𝑙) ⊆ ℝ))
154 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝑔𝑙) → (vol*‘𝑥) = (vol*‘(𝑔𝑙)))
155154eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑔𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔𝑙)) ∈ ℝ))
156153, 155anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝑔𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
157156ralima 6641 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
158123, 152, 157sylancl 574 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
159 foima 6261 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔:ℕ–onto𝐴 → (𝑔 “ ℕ) = 𝐴)
160159raleqdv 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
161158, 160bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:ℕ–onto𝐴 → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
162161adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
163151, 162mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
164 ssralv 3815 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
16538, 163, 164mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
166165adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
167 ovolfiniun 23489 . . . . . . . . . . . . . . . . . . . . . 22 (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)))
16835, 166, 167sylancr 575 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)))
169 mblvol 23518 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑙) ∈ dom vol → (vol‘(𝑔𝑙)) = (vol*‘(𝑔𝑙)))
17049, 169syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔𝑙)) = (vol*‘(𝑔𝑙)))
17145simprd 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → (vol‘(𝑔𝑙)) = 0)
17240, 171sylan2 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto𝐴𝑙 ∈ ℕ)) → (vol‘(𝑔𝑙)) = 0)
173172ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔𝑙)) = 0)
174173an32s 631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔𝑙)) = 0)
175170, 174eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔𝑙)) = 0)
176175ralrimiva 3115 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (vol*‘(𝑔𝑙)) = 0)
177 ssralv 3815 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (vol*‘(𝑔𝑙)) = 0 → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0))
17838, 176, 177mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
179178adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
180179sumeq2d 14640 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = Σ𝑙 ∈ (1...𝑚)0)
18135olci 855 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑚) ⊆ (ℤ‘1) ∨ (1...𝑚) ∈ Fin)
182 sumz 14661 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑚) ⊆ (ℤ‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0)
183181, 182ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑙 ∈ (1...𝑚)0 = 0
184180, 183syl6eq 2821 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
185168, 184breqtrd 4812 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0)
186 mblss 23519 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑙) ∈ dom vol → (𝑔𝑙) ⊆ ℝ)
187186ralimi 3101 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
18852, 187syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
189 iunss 4695 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
190188, 189sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
191190adantr 466 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
192 ovolge0 23469 . . . . . . . . . . . . . . . . . . . . 21 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ → 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
193191, 192syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
194 ovolcl 23466 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
195190, 194syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
196195adantr 466 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
197 0xr 10288 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℝ*
198 xrletri3 12190 . . . . . . . . . . . . . . . . . . . . 21 (((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0 ↔ ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))))
199196, 197, 198sylancl 574 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0 ↔ ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))))
200185, 193, 199mpbir2and 692 . . . . . . . . . . . . . . . . . . 19 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0)
201140, 200eqtrd 2805 . . . . . . . . . . . . . . . . . 18 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0)
202201mpteq2dva 4878 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ 0))
203 fconstmpt 5303 . . . . . . . . . . . . . . . . 17 (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
204202, 203syl6eqr 2823 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}))
205138, 204eqtrd 2805 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}))
206 frn 6193 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol)
207 ffn 6185 . . . . . . . . . . . . . . . . . . 19 (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
208134, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18 vol Fn dom vol
209120, 56fnmpti 6162 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) Fn ℕ
210 fnco 6139 . . . . . . . . . . . . . . . . . 18 ((vol Fn dom vol ∧ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
211208, 209, 210mp3an12 1562 . . . . . . . . . . . . . . . . 17 (ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
21257, 206, 2113syl 18 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
213 1nn 11233 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
214213ne0ii 4071 . . . . . . . . . . . . . . . 16 ℕ ≠ ∅
215 fconst5 6615 . . . . . . . . . . . . . . . 16 (((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ ∧ ℕ ≠ ∅) → ((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0}))
216212, 214, 215sylancl 574 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0}))
217205, 216mpbid 222 . . . . . . . . . . . . . 14 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0})
218132, 217syl5eqr 2819 . . . . . . . . . . . . 13 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0})
219218supeq1d 8508 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ) = sup({0}, ℝ*, < ))
220 xrltso 12179 . . . . . . . . . . . . 13 < Or ℝ*
221 supsn 8534 . . . . . . . . . . . . 13 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
222220, 197, 221mp2an 672 . . . . . . . . . . . 12 sup({0}, ℝ*, < ) = 0
223219, 222syl6eq 2821 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ) = 0)
22494, 131, 2233eqtr3rd 2814 . . . . . . . . . 10 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 0 = (vol‘ 𝐴))
225224ex 397 . . . . . . . . 9 (𝑔:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 = (vol‘ 𝐴)))
22634, 225syl5 34 . . . . . . . 8 (𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
227226exlimiv 2010 . . . . . . 7 (∃𝑔 𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
22818, 227syl 17 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
229228expimpd 441 . . . . 5 (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
23011, 229pm2.61ine 3026 . . . 4 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴))
231 renepnf 10289 . . . . . . 7 (0 ∈ ℝ → 0 ≠ +∞)
232144, 231mp1i 13 . . . . . 6 ( 𝐴 = ℝ → 0 ≠ +∞)
233 fveq2 6332 . . . . . . 7 ( 𝐴 = ℝ → (vol‘ 𝐴) = (vol‘ℝ))
234 rembl 23528 . . . . . . . . 9 ℝ ∈ dom vol
235 mblvol 23518 . . . . . . . . 9 (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
236234, 235ax-mp 5 . . . . . . . 8 (vol‘ℝ) = (vol*‘ℝ)
237 ovolre 23513 . . . . . . . 8 (vol*‘ℝ) = +∞
238236, 237eqtri 2793 . . . . . . 7 (vol‘ℝ) = +∞
239233, 238syl6eq 2821 . . . . . 6 ( 𝐴 = ℝ → (vol‘ 𝐴) = +∞)
240232, 239neeqtrrd 3017 . . . . 5 ( 𝐴 = ℝ → 0 ≠ (vol‘ 𝐴))
241240necon2i 2977 . . . 4 (0 = (vol‘ 𝐴) → 𝐴 ≠ ℝ)
242230, 241syl 17 . . 3 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 𝐴 ≠ ℝ)
243242expr 444 . 2 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ( 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ))
244 eqimss 3806 . . 3 ( 𝐴 = ℝ → 𝐴 ⊆ ℝ)
245244necon3bi 2969 . 2 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ)
246243, 245pm2.61d1 172 1 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wo 836   = wceq 1631  wex 1852  wcel 2145  {cab 2757  wne 2943  wral 3061  wrex 3062  Vcvv 3351  wss 3723  c0 4063  {csn 4316   cuni 4574   ciun 4654   class class class wbr 4786  cmpt 4863   Or wor 5169   × cxp 5247  dom cdm 5249  ran crn 5250  cima 5252  ccom 5253   Fn wfn 6026  wf 6027  ontowfo 6029  cfv 6031  (class class class)co 6793  cdom 8107  csdm 8108  Fincfn 8109  supcsup 8502  cr 10137  0cc0 10138  1c1 10139   + caddc 10141  +∞cpnf 10273  *cxr 10275   < clt 10276  cle 10277  cn 11222  cuz 11888  [,]cicc 12383  ...cfz 12533  Σcsu 14624  vol*covol 23450  volcvol 23451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-sum 14625  df-rest 16291  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-top 20919  df-topon 20936  df-bases 20971  df-cmp 21411  df-ovol 23452  df-vol 23453
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator