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 33113
Description: volsup 23243 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 4415 . . . . . . . . 9 (𝐴 = ∅ → 𝐴 = ∅)
2 uni0 4436 . . . . . . . . 9 ∅ = ∅
31, 2syl6eq 2671 . . . . . . . 8 (𝐴 = ∅ → 𝐴 = ∅)
43fveq2d 6157 . . . . . . 7 (𝐴 = ∅ → (vol‘ 𝐴) = (vol‘∅))
5 0mbl 23226 . . . . . . . . 9 ∅ ∈ dom vol
6 mblvol 23217 . . . . . . . . 9 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
75, 6ax-mp 5 . . . . . . . 8 (vol‘∅) = (vol*‘∅)
8 ovol0 23180 . . . . . . . 8 (vol*‘∅) = 0
97, 8eqtri 2643 . . . . . . 7 (vol‘∅) = 0
104, 9syl6req 2672 . . . . . 6 (𝐴 = ∅ → 0 = (vol‘ 𝐴))
1110a1d 25 . . . . 5 (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
12 reldom 7912 . . . . . . . . . . 11 Rel ≼
1312brrelexi 5123 . . . . . . . . . 10 (𝐴 ≼ ℕ → 𝐴 ∈ V)
14 0sdomg 8040 . . . . . . . . . 10 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1513, 14syl 17 . . . . . . . . 9 (𝐴 ≼ ℕ → (∅ ≺ 𝐴𝐴 ≠ ∅))
1615biimparc 504 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17 fodomr 8062 . . . . . . . 8 ((∅ ≺ 𝐴𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
1816, 17sylancom 700 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
19 unissb 4440 . . . . . . . . . . . . 13 ( 𝐴 ⊆ ℝ ↔ ∀𝑥𝐴 𝑥 ⊆ ℝ)
2019anbi1i 730 . . . . . . . . . . . 12 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
21 r19.26 3058 . . . . . . . . . . . 12 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
2220, 21bitr4i 267 . . . . . . . . . . 11 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23 ovolctb2 23179 . . . . . . . . . . . . 13 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24 nulmbl 23222 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 𝑥 ∈ dom vol)
25 mblvol 23217 . . . . . . . . . . . . . . . 16 (𝑥 ∈ dom vol → (vol‘𝑥) = (vol*‘𝑥))
26 eqtr 2640 . . . . . . . . . . . . . . . . 17 (((vol‘𝑥) = (vol*‘𝑥) ∧ (vol*‘𝑥) = 0) → (vol‘𝑥) = 0)
2726expcom 451 . . . . . . . . . . . . . . . 16 ((vol*‘𝑥) = 0 → ((vol‘𝑥) = (vol*‘𝑥) → (vol‘𝑥) = 0))
2825, 27syl5 34 . . . . . . . . . . . . . . 15 ((vol*‘𝑥) = 0 → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
2928adantl 482 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
3024, 29jcai 558 . . . . . . . . . . . . 13 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3123, 30syldan 487 . . . . . . . . . . . 12 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3231ralimi 2947 . . . . . . . . . . 11 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3322, 32sylbi 207 . . . . . . . . . 10 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3433ancoms 469 . . . . . . . . 9 ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
35 fzfi 12718 . . . . . . . . . . . . . . 15 (1...𝑚) ∈ Fin
36 fzssuz 12331 . . . . . . . . . . . . . . . . 17 (1...𝑚) ⊆ (ℤ‘1)
37 nnuz 11674 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
3836, 37sseqtr4i 3622 . . . . . . . . . . . . . . . 16 (1...𝑚) ⊆ ℕ
39 fof 6077 . . . . . . . . . . . . . . . . . . . 20 (𝑔:ℕ–onto𝐴𝑔:ℕ⟶𝐴)
4039ffvelrnda 6320 . . . . . . . . . . . . . . . . . . 19 ((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) → (𝑔𝑙) ∈ 𝐴)
41 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑔𝑙) → (𝑥 ∈ dom vol ↔ (𝑔𝑙) ∈ dom vol))
42 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑔𝑙) → (vol‘𝑥) = (vol‘(𝑔𝑙)))
4342eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑔𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔𝑙)) = 0))
4441, 43anbi12d 746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑔𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔𝑙) ∈ dom vol ∧ (vol‘(𝑔𝑙)) = 0)))
4544rspccva 3297 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → ((𝑔𝑙) ∈ dom vol ∧ (vol‘(𝑔𝑙)) = 0))
4645simpld 475 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → (𝑔𝑙) ∈ dom vol)
4746ancoms 469 . . . . . . . . . . . . . . . . . . 19 (((𝑔𝑙) ∈ 𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔𝑙) ∈ dom vol)
4840, 47sylan 488 . . . . . . . . . . . . . . . . . 18 (((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔𝑙) ∈ dom vol)
4948an32s 845 . . . . . . . . . . . . . . . . 17 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔𝑙) ∈ dom vol)
5049ralrimiva 2961 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔𝑙) ∈ dom vol)
51 ssralv 3650 . . . . . . . . . . . . . . . 16 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (𝑔𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol))
5238, 50, 51mpsyl 68 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
53 finiunmbl 23231 . . . . . . . . . . . . . . 15 (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5435, 52, 53sylancr 694 . . . . . . . . . . . . . 14 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5554adantr 481 . . . . . . . . . . . . 13 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
56 eqid 2621 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
5755, 56fmptd 6346 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol)
58 fzssp1 12333 . . . . . . . . . . . . . . 15 (1...𝑛) ⊆ (1...(𝑛 + 1))
59 iunss1 4503 . . . . . . . . . . . . . . 15 ((1...𝑛) ⊆ (1...(𝑛 + 1)) → 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
6058, 59ax-mp 5 . . . . . . . . . . . . . 14 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙)
61 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
6261iuneq1d 4516 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) = 𝑙 ∈ (1...𝑛)(𝑔𝑙))
63 ovex 6638 . . . . . . . . . . . . . . . . 17 (1...𝑛) ∈ V
64 fvex 6163 . . . . . . . . . . . . . . . . 17 (𝑔𝑙) ∈ V
6563, 64iunex 7100 . . . . . . . . . . . . . . . 16 𝑙 ∈ (1...𝑛)(𝑔𝑙) ∈ V
6662, 56, 65fvmpt 6244 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) = 𝑙 ∈ (1...𝑛)(𝑔𝑙))
67 peano2nn 10983 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
68 oveq2 6618 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1)))
6968iuneq1d 4516 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 + 1) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
70 ovex 6638 . . . . . . . . . . . . . . . . . 18 (1...(𝑛 + 1)) ∈ V
7170, 64iunex 7100 . . . . . . . . . . . . . . . . 17 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙) ∈ V
7269, 56, 71fvmpt 6244 . . . . . . . . . . . . . . . 16 ((𝑛 + 1) ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
7367, 72syl 17 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
7466, 73sseq12d 3618 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) ↔ 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙)))
7560, 74mpbiri 248 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))
7675rgen 2917 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))
77 nnex 10977 . . . . . . . . . . . . . 14 ℕ ∈ V
7877mptex 6446 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ V
79 feq1 5988 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol))
80 fveq1 6152 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓𝑛) = ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛))
81 fveq1 6152 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))
8280, 81sseq12d 3618 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))))
8382ralbidv 2981 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))))
8479, 83anbi12d 746 . . . . . . . . . . . . . 14 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))))
85 rneq 5316 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
8685unieqd 4417 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
8786fveq2d 6157 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (vol‘ ran 𝑓) = (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
8885imaeq2d 5430 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
8988supeq1d 8303 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → sup((vol “ ran 𝑓), ℝ*, < ) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
9087, 89eqeq12d 2636 . . . . . . . . . . . . . 14 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((vol‘ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ) ↔ (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < )))
9184, 90imbi12d 334 . . . . . . . . . . . . 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 3248 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
9457, 76, 93sylancl 693 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
95 df-iun 4492 . . . . . . . . . . . . . . . 16 𝑥 ∈ ℕ (𝑔𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥)}
96 eluzfz2 12298 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (ℤ‘1) → 𝑥 ∈ (1...𝑥))
9796, 37eleq2s 2716 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥))
98 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = 𝑥 → (𝑔𝑙) = (𝑔𝑥))
9998eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑥 → (𝑛 ∈ (𝑔𝑙) ↔ 𝑛 ∈ (𝑔𝑥)))
10099rspcev 3298 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙))
10197, 100sylan 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙))
102 oveq2 6618 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
103102rexeqdv 3137 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙)))
104103rspcev 3298 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
105101, 104syldan 487 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
106105rexlimiva 3022 . . . . . . . . . . . . . . . . . . 19 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
107 ssrexv 3651 . . . . . . . . . . . . . . . . . . . . . 22 ((1...𝑚) ⊆ ℕ → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙)))
10838, 107ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙))
10999cbvrexv 3163 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
110108, 109sylib 208 . . . . . . . . . . . . . . . . . . . 20 (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
111110rexlimivw 3023 . . . . . . . . . . . . . . . . . . 19 (∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
112106, 111impbii 199 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
113 eliun 4495 . . . . . . . . . . . . . . . . . . 19 (𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
114113rexbii 3035 . . . . . . . . . . . . . . . . . 18 (∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
115112, 114bitr4i 267 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙))
116115abbii 2736 . . . . . . . . . . . . . . . 16 {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
11795, 116eqtri 2643 . . . . . . . . . . . . . . 15 𝑥 ∈ ℕ (𝑔𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
118 df-iun 4492 . . . . . . . . . . . . . . 15 𝑚 ∈ ℕ 𝑙 ∈ (1...𝑚)(𝑔𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
119 ovex 6638 . . . . . . . . . . . . . . . . 17 (1...𝑚) ∈ V
120119, 64iunex 7100 . . . . . . . . . . . . . . . 16 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ V
121120dfiun3 5345 . . . . . . . . . . . . . . 15 𝑚 ∈ ℕ 𝑙 ∈ (1...𝑚)(𝑔𝑙) = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
122117, 118, 1213eqtr2i 2649 . . . . . . . . . . . . . 14 𝑥 ∈ ℕ (𝑔𝑥) = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
123 fofn 6079 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴𝑔 Fn ℕ)
124 fniunfv 6465 . . . . . . . . . . . . . . . 16 (𝑔 Fn ℕ → 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
125123, 124syl 17 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
126 forn 6080 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴 → ran 𝑔 = 𝐴)
127126unieqd 4417 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 ran 𝑔 = 𝐴)
128125, 127eqtrd 2655 . . . . . . . . . . . . . 14 (𝑔:ℕ–onto𝐴 𝑥 ∈ ℕ (𝑔𝑥) = 𝐴)
129122, 128syl5eqr 2669 . . . . . . . . . . . . 13 (𝑔:ℕ–onto𝐴 ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 𝐴)
130129fveq2d 6157 . . . . . . . . . . . 12 (𝑔:ℕ–onto𝐴 → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol‘ 𝐴))
131130adantr 481 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol‘ 𝐴))
132 rnco2 5606 . . . . . . . . . . . . . 14 ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
133 eqidd 2622 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
134 volf 23216 . . . . . . . . . . . . . . . . . . 19 vol:dom vol⟶(0[,]+∞)
135134a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom vol⟶(0[,]+∞))
136135feqmptd 6211 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦ (vol‘𝑛)))
137 fveq2 6153 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑙 ∈ (1...𝑚)(𝑔𝑙) → (vol‘𝑛) = (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
13855, 133, 136, 137fmptco 6357 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
139 mblvol 23217 . . . . . . . . . . . . . . . . . . . 20 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
14055, 139syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
141 mblss 23218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
142141adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 𝑥 ⊆ ℝ)
14325eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 ↔ (vol*‘𝑥) = 0))
144 0re 9991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 0 ∈ ℝ
145 eleq1a 2693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 ∈ ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
146144, 145ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)
147143, 146syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
148147imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (vol*‘𝑥) ∈ ℝ)
149142, 148jca 554 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
150149ralimi 2947 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
151150adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
152 ssid 3608 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℕ ⊆ ℕ
153 sseq1 3610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑔𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔𝑙) ⊆ ℝ))
154 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝑔𝑙) → (vol*‘𝑥) = (vol*‘(𝑔𝑙)))
155154eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑔𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔𝑙)) ∈ ℝ))
156153, 155anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝑔𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
157156ralima 6458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
158123, 152, 157sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
159 foima 6082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔:ℕ–onto𝐴 → (𝑔 “ ℕ) = 𝐴)
160159raleqdv 3136 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
161158, 160bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:ℕ–onto𝐴 → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
162161adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
163151, 162mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
164 ssralv 3650 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
16538, 163, 164mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
166165adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
167 ovolfiniun 23188 . . . . . . . . . . . . . . . . . . . . . 22 (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)))
16835, 166, 167sylancr 694 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)))
169 mblvol 23217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑙) ∈ dom vol → (vol‘(𝑔𝑙)) = (vol*‘(𝑔𝑙)))
17049, 169syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔𝑙)) = (vol*‘(𝑔𝑙)))
17145simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → (vol‘(𝑔𝑙)) = 0)
17240, 171sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto𝐴𝑙 ∈ ℕ)) → (vol‘(𝑔𝑙)) = 0)
173172ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔𝑙)) = 0)
174173an32s 845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔𝑙)) = 0)
175170, 174eqtr3d 2657 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔𝑙)) = 0)
176175ralrimiva 2961 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (vol*‘(𝑔𝑙)) = 0)
177 ssralv 3650 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (vol*‘(𝑔𝑙)) = 0 → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0))
17838, 176, 177mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
179178adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
180179sumeq2d 14373 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = Σ𝑙 ∈ (1...𝑚)0)
18135olci 406 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑚) ⊆ (ℤ‘1) ∨ (1...𝑚) ∈ Fin)
182 sumz 14393 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑚) ⊆ (ℤ‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0)
183181, 182ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑙 ∈ (1...𝑚)0 = 0
184180, 183syl6eq 2671 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
185168, 184breqtrd 4644 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0)
186 mblss 23218 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑙) ∈ dom vol → (𝑔𝑙) ⊆ ℝ)
187186ralimi 2947 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
18852, 187syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
189 iunss 4532 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
190188, 189sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
191190adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
192 ovolge0 23168 . . . . . . . . . . . . . . . . . . . . 21 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ → 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
193191, 192syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
194 ovolcl 23165 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
195190, 194syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
196195adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
197 0xr 10037 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℝ*
198 xrletri3 11936 . . . . . . . . . . . . . . . . . . . . 21 (((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0 ↔ ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))))
199196, 197, 198sylancl 693 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0 ↔ ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))))
200185, 193, 199mpbir2and 956 . . . . . . . . . . . . . . . . . . 19 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0)
201140, 200eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0)
202201mpteq2dva 4709 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ 0))
203 fconstmpt 5128 . . . . . . . . . . . . . . . . 17 (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
204202, 203syl6eqr 2673 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}))
205138, 204eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}))
206 frn 6015 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol)
207 ffn 6007 . . . . . . . . . . . . . . . . . . 19 (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
208134, 207ax-mp 5 . . . . . . . . . . . . . . . . . 18 vol Fn dom vol
209120, 56fnmpti 5984 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) Fn ℕ
210 fnco 5962 . . . . . . . . . . . . . . . . . 18 ((vol Fn dom vol ∧ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
211208, 209, 210mp3an12 1411 . . . . . . . . . . . . . . . . 17 (ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
21257, 206, 2113syl 18 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
213 1nn 10982 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
214213ne0ii 3904 . . . . . . . . . . . . . . . 16 ℕ ≠ ∅
215 fconst5 6431 . . . . . . . . . . . . . . . 16 (((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ ∧ ℕ ≠ ∅) → ((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0}))
216212, 214, 215sylancl 693 . . . . . . . . . . . . . . 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 2669 . . . . . . . . . . . . 13 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0})
219218supeq1d 8303 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ) = sup({0}, ℝ*, < ))
220 xrltso 11925 . . . . . . . . . . . . 13 < Or ℝ*
221 supsn 8329 . . . . . . . . . . . . 13 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
222220, 197, 221mp2an 707 . . . . . . . . . . . 12 sup({0}, ℝ*, < ) = 0
223219, 222syl6eq 2671 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ) = 0)
22494, 131, 2233eqtr3rd 2664 . . . . . . . . . 10 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 0 = (vol‘ 𝐴))
225224ex 450 . . . . . . . . 9 (𝑔:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 = (vol‘ 𝐴)))
22634, 225syl5 34 . . . . . . . 8 (𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
227226exlimiv 1855 . . . . . . 7 (∃𝑔 𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
22818, 227syl 17 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
229228expimpd 628 . . . . 5 (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
23011, 229pm2.61ine 2873 . . . 4 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴))
231 renepnf 10038 . . . . . . 7 (0 ∈ ℝ → 0 ≠ +∞)
232144, 231mp1i 13 . . . . . 6 ( 𝐴 = ℝ → 0 ≠ +∞)
233 fveq2 6153 . . . . . . 7 ( 𝐴 = ℝ → (vol‘ 𝐴) = (vol‘ℝ))
234 rembl 23227 . . . . . . . . 9 ℝ ∈ dom vol
235 mblvol 23217 . . . . . . . . 9 (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
236234, 235ax-mp 5 . . . . . . . 8 (vol‘ℝ) = (vol*‘ℝ)
237 ovolre 23212 . . . . . . . 8 (vol*‘ℝ) = +∞
238236, 237eqtri 2643 . . . . . . 7 (vol‘ℝ) = +∞
239233, 238syl6eq 2671 . . . . . 6 ( 𝐴 = ℝ → (vol‘ 𝐴) = +∞)
240232, 239neeqtrrd 2864 . . . . 5 ( 𝐴 = ℝ → 0 ≠ (vol‘ 𝐴))
241240necon2i 2824 . . . 4 (0 = (vol‘ 𝐴) → 𝐴 ≠ ℝ)
242230, 241syl 17 . . 3 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 𝐴 ≠ ℝ)
243242expr 642 . 2 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ( 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ))
244 eqimss 3641 . . 3 ( 𝐴 = ℝ → 𝐴 ⊆ ℝ)
245244necon3bi 2816 . 2 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ)
246243, 245pm2.61d1 171 1 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wex 1701  wcel 1987  {cab 2607  wne 2790  wral 2907  wrex 2908  Vcvv 3189  wss 3559  c0 3896  {csn 4153   cuni 4407   ciun 4490   class class class wbr 4618  cmpt 4678   Or wor 4999   × cxp 5077  dom cdm 5079  ran crn 5080  cima 5082  ccom 5083   Fn wfn 5847  wf 5848  ontowfo 5850  cfv 5852  (class class class)co 6610  cdom 7904  csdm 7905  Fincfn 7906  supcsup 8297  cr 9886  0cc0 9887  1c1 9888   + caddc 9890  +∞cpnf 10022  *cxr 10024   < clt 10025  cle 10026  cn 10971  cuz 11638  [,]cicc 12127  ...cfz 12275  Σcsu 14357  vol*covol 23150  volcvol 23151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-n0 11244  df-z 11329  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-clim 14160  df-sum 14358  df-rest 16011  df-topgen 16032  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-top 20627  df-topon 20644  df-bases 20670  df-cmp 21109  df-ovol 23152  df-vol 23153
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator