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 33761
Description: volsup 23531 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 4631 . . . . . . . . 9 (𝐴 = ∅ → 𝐴 = ∅)
2 uni0 4652 . . . . . . . . 9 ∅ = ∅
31, 2syl6eq 2852 . . . . . . . 8 (𝐴 = ∅ → 𝐴 = ∅)
43fveq2d 6406 . . . . . . 7 (𝐴 = ∅ → (vol‘ 𝐴) = (vol‘∅))
5 0mbl 23514 . . . . . . . . 9 ∅ ∈ dom vol
6 mblvol 23505 . . . . . . . . 9 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
75, 6ax-mp 5 . . . . . . . 8 (vol‘∅) = (vol*‘∅)
8 ovol0 23468 . . . . . . . 8 (vol*‘∅) = 0
97, 8eqtri 2824 . . . . . . 7 (vol‘∅) = 0
104, 9syl6req 2853 . . . . . 6 (𝐴 = ∅ → 0 = (vol‘ 𝐴))
1110a1d 25 . . . . 5 (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
12 reldom 8192 . . . . . . . . . . 11 Rel ≼
1312brrelexi 5352 . . . . . . . . . 10 (𝐴 ≼ ℕ → 𝐴 ∈ V)
14 0sdomg 8322 . . . . . . . . . 10 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1513, 14syl 17 . . . . . . . . 9 (𝐴 ≼ ℕ → (∅ ≺ 𝐴𝐴 ≠ ∅))
1615biimparc 467 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17 fodomr 8344 . . . . . . . 8 ((∅ ≺ 𝐴𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
1816, 17sylancom 578 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
19 unissb 4656 . . . . . . . . . . . . 13 ( 𝐴 ⊆ ℝ ↔ ∀𝑥𝐴 𝑥 ⊆ ℝ)
2019anbi1i 612 . . . . . . . . . . . 12 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
21 r19.26 3248 . . . . . . . . . . . 12 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
2220, 21bitr4i 269 . . . . . . . . . . 11 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23 ovolctb2 23467 . . . . . . . . . . . . 13 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
24 nulmbl 23510 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 𝑥 ∈ dom vol)
25 mblvol 23505 . . . . . . . . . . . . . . . 16 (𝑥 ∈ dom vol → (vol‘𝑥) = (vol*‘𝑥))
26 eqtr 2821 . . . . . . . . . . . . . . . . 17 (((vol‘𝑥) = (vol*‘𝑥) ∧ (vol*‘𝑥) = 0) → (vol‘𝑥) = 0)
2726expcom 400 . . . . . . . . . . . . . . . 16 ((vol*‘𝑥) = 0 → ((vol‘𝑥) = (vol*‘𝑥) → (vol‘𝑥) = 0))
2825, 27syl5 34 . . . . . . . . . . . . . . 15 ((vol*‘𝑥) = 0 → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
2928adantl 469 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol → (vol‘𝑥) = 0))
3024, 29jcai 508 . . . . . . . . . . . . 13 ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3123, 30syldan 581 . . . . . . . . . . . 12 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3231ralimi 3136 . . . . . . . . . . 11 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3322, 32sylbi 208 . . . . . . . . . 10 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
3433ancoms 448 . . . . . . . . 9 ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0))
35 fzfi 12989 . . . . . . . . . . . . . . 15 (1...𝑚) ∈ Fin
36 fzssuz 12599 . . . . . . . . . . . . . . . . 17 (1...𝑚) ⊆ (ℤ‘1)
37 nnuz 11935 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
3836, 37sseqtr4i 3829 . . . . . . . . . . . . . . . 16 (1...𝑚) ⊆ ℕ
39 fof 6325 . . . . . . . . . . . . . . . . . . . 20 (𝑔:ℕ–onto𝐴𝑔:ℕ⟶𝐴)
4039ffvelrnda 6575 . . . . . . . . . . . . . . . . . . 19 ((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) → (𝑔𝑙) ∈ 𝐴)
41 eleq1 2869 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑔𝑙) → (𝑥 ∈ dom vol ↔ (𝑔𝑙) ∈ dom vol))
42 fveqeq2 6411 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑔𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔𝑙)) = 0))
4341, 42anbi12d 618 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑔𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔𝑙) ∈ dom vol ∧ (vol‘(𝑔𝑙)) = 0)))
4443rspccva 3497 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → ((𝑔𝑙) ∈ dom vol ∧ (vol‘(𝑔𝑙)) = 0))
4544simpld 484 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → (𝑔𝑙) ∈ dom vol)
4645ancoms 448 . . . . . . . . . . . . . . . . . . 19 (((𝑔𝑙) ∈ 𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔𝑙) ∈ dom vol)
4740, 46sylan 571 . . . . . . . . . . . . . . . . . 18 (((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔𝑙) ∈ dom vol)
4847an32s 634 . . . . . . . . . . . . . . . . 17 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔𝑙) ∈ dom vol)
4948ralrimiva 3150 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔𝑙) ∈ dom vol)
50 ssralv 3857 . . . . . . . . . . . . . . . 16 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (𝑔𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol))
5138, 49, 50mpsyl 68 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
52 finiunmbl 23519 . . . . . . . . . . . . . . 15 (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5335, 51, 52sylancr 577 . . . . . . . . . . . . . 14 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5453adantr 468 . . . . . . . . . . . . 13 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol)
5554fmpttd 6601 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol)
56 fzssp1 12601 . . . . . . . . . . . . . . 15 (1...𝑛) ⊆ (1...(𝑛 + 1))
57 iunss1 4717 . . . . . . . . . . . . . . 15 ((1...𝑛) ⊆ (1...(𝑛 + 1)) → 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
5856, 57ax-mp 5 . . . . . . . . . . . . . 14 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙)
59 oveq2 6876 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
6059iuneq1d 4730 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) = 𝑙 ∈ (1...𝑛)(𝑔𝑙))
61 eqid 2802 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
62 ovex 6900 . . . . . . . . . . . . . . . . 17 (1...𝑛) ∈ V
63 fvex 6415 . . . . . . . . . . . . . . . . 17 (𝑔𝑙) ∈ V
6462, 63iunex 7371 . . . . . . . . . . . . . . . 16 𝑙 ∈ (1...𝑛)(𝑔𝑙) ∈ V
6560, 61, 64fvmpt 6497 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) = 𝑙 ∈ (1...𝑛)(𝑔𝑙))
66 peano2nn 11311 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
67 oveq2 6876 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1)))
6867iuneq1d 4730 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑛 + 1) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
69 ovex 6900 . . . . . . . . . . . . . . . . . 18 (1...(𝑛 + 1)) ∈ V
7069, 63iunex 7371 . . . . . . . . . . . . . . . . 17 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙) ∈ V
7168, 61, 70fvmpt 6497 . . . . . . . . . . . . . . . 16 ((𝑛 + 1) ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
7266, 71syl 17 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) = 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙))
7365, 72sseq12d 3825 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)) ↔ 𝑙 ∈ (1...𝑛)(𝑔𝑙) ⊆ 𝑙 ∈ (1...(𝑛 + 1))(𝑔𝑙)))
7458, 73mpbiri 249 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))
7574rgen 3106 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))
76 nnex 11305 . . . . . . . . . . . . . 14 ℕ ∈ V
7776mptex 6705 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ V
78 feq1 6231 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol))
79 fveq1 6401 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓𝑛) = ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛))
80 fveq1 6401 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))
8179, 80sseq12d 3825 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))))
8281ralbidv 3170 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))))
8378, 82anbi12d 618 . . . . . . . . . . . . . 14 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1)))))
84 rneq 5546 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
8584unieqd 4633 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
8685fveq2d 6406 . . . . . . . . . . . . . . 15 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (vol‘ ran 𝑓) = (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
8784imaeq2d 5670 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
8887supeq1d 8585 . . . . . . . . . . . . . . 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 335 . . . . . . . . . . . . 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 3448 . . . . . . . . . . . 12 (((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))‘(𝑛 + 1))) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
9355, 75, 92sylancl 576 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ))
94 df-iun 4707 . . . . . . . . . . . . . . . 16 𝑥 ∈ ℕ (𝑔𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥)}
95 eluzfz2 12566 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (ℤ‘1) → 𝑥 ∈ (1...𝑥))
9695, 37eleq2s 2899 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥))
97 fveq2 6402 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 = 𝑥 → (𝑔𝑙) = (𝑔𝑥))
9897eleq2d 2867 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑥 → (𝑛 ∈ (𝑔𝑙) ↔ 𝑛 ∈ (𝑔𝑥)))
9998rspcev 3498 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙))
10096, 99sylan 571 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙))
101 oveq2 6876 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
102101rexeqdv 3330 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙)))
103102rspcev 3498 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
104100, 103syldan 581 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
105104rexlimiva 3212 . . . . . . . . . . . . . . . . . . 19 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
106 ssrexv 3858 . . . . . . . . . . . . . . . . . . . . . 22 ((1...𝑚) ⊆ ℕ → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙)))
10738, 106ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙))
10898cbvrexv 3357 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
109107, 108sylib 209 . . . . . . . . . . . . . . . . . . . 20 (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
110109rexlimivw 3213 . . . . . . . . . . . . . . . . . . 19 (∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥))
111105, 110impbii 200 . . . . . . . . . . . . . . . . . 18 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
112 eliun 4709 . . . . . . . . . . . . . . . . . . 19 (𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
113112rexbii 3225 . . . . . . . . . . . . . . . . . 18 (∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔𝑙))
114111, 113bitr4i 269 . . . . . . . . . . . . . . . . 17 (∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙))
115114abbii 2919 . . . . . . . . . . . . . . . 16 {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
11694, 115eqtri 2824 . . . . . . . . . . . . . . 15 𝑥 ∈ ℕ (𝑔𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
117 df-iun 4707 . . . . . . . . . . . . . . 15 𝑚 ∈ ℕ 𝑙 ∈ (1...𝑚)(𝑔𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 𝑙 ∈ (1...𝑚)(𝑔𝑙)}
118 ovex 6900 . . . . . . . . . . . . . . . . 17 (1...𝑚) ∈ V
119118, 63iunex 7371 . . . . . . . . . . . . . . . 16 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ V
120119dfiun3 5575 . . . . . . . . . . . . . . 15 𝑚 ∈ ℕ 𝑙 ∈ (1...𝑚)(𝑔𝑙) = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
121116, 117, 1203eqtr2i 2830 . . . . . . . . . . . . . 14 𝑥 ∈ ℕ (𝑔𝑥) = ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))
122 fofn 6327 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴𝑔 Fn ℕ)
123 fniunfv 6723 . . . . . . . . . . . . . . . 16 (𝑔 Fn ℕ → 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
124122, 123syl 17 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 𝑥 ∈ ℕ (𝑔𝑥) = ran 𝑔)
125 forn 6328 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴 → ran 𝑔 = 𝐴)
126125unieqd 4633 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 ran 𝑔 = 𝐴)
127124, 126eqtrd 2836 . . . . . . . . . . . . . 14 (𝑔:ℕ–onto𝐴 𝑥 ∈ ℕ (𝑔𝑥) = 𝐴)
128121, 127syl5eqr 2850 . . . . . . . . . . . . 13 (𝑔:ℕ–onto𝐴 ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 𝐴)
129128fveq2d 6406 . . . . . . . . . . . 12 (𝑔:ℕ–onto𝐴 → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol‘ 𝐴))
130129adantr 468 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol‘ 𝐴))
131 rnco2 5850 . . . . . . . . . . . . . 14 ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
132 eqidd 2803 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
133 volf 23504 . . . . . . . . . . . . . . . . . . 19 vol:dom vol⟶(0[,]+∞)
134133a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom vol⟶(0[,]+∞))
135134feqmptd 6464 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦ (vol‘𝑛)))
136 fveq2 6402 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑙 ∈ (1...𝑚)(𝑔𝑙) → (vol‘𝑛) = (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
13754, 132, 135, 136fmptco 6613 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))))
138 mblvol 23505 . . . . . . . . . . . . . . . . . . . 20 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
13954, 138syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
140 mblss 23506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ dom vol → 𝑥 ⊆ ℝ)
141140adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 𝑥 ⊆ ℝ)
14225eqeq1d 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 ↔ (vol*‘𝑥) = 0))
143 0re 10321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 0 ∈ ℝ
144 eleq1a 2876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 ∈ ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
145143, 144ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)
146142, 145syl6bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ dom vol → ((vol‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ))
147146imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (vol*‘𝑥) ∈ ℝ)
148141, 147jca 503 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
149148ralimi 3136 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
150149adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ))
151 ssid 3814 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℕ ⊆ ℕ
152 sseq1 3817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑔𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔𝑙) ⊆ ℝ))
153 fveq2 6402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 = (𝑔𝑙) → (vol*‘𝑥) = (vol*‘(𝑔𝑙)))
154153eleq1d 2866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 = (𝑔𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔𝑙)) ∈ ℝ))
155152, 154anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝑔𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
156155ralima 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
157122, 151, 156sylancl 576 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
158 foima 6330 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑔:ℕ–onto𝐴 → (𝑔 “ ℕ) = 𝐴)
159158raleqdv 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
160157, 159bitr3d 272 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔:ℕ–onto𝐴 → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
161160adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)))
162150, 161mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
163 ssralv 3857 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ ((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)))
16438, 162, 163mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
165164adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ))
166 ovolfiniun 23476 . . . . . . . . . . . . . . . . . . . . . 22 (((1...𝑚) ∈ Fin ∧ ∀𝑙 ∈ (1...𝑚)((𝑔𝑙) ⊆ ℝ ∧ (vol*‘(𝑔𝑙)) ∈ ℝ)) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)))
16735, 165, 166sylancr 577 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)))
168 mblvol 23505 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑙) ∈ dom vol → (vol‘(𝑔𝑙)) = (vol*‘(𝑔𝑙)))
16948, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔𝑙)) = (vol*‘(𝑔𝑙)))
17044simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔𝑙) ∈ 𝐴) → (vol‘(𝑔𝑙)) = 0)
17140, 170sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto𝐴𝑙 ∈ ℕ)) → (vol‘(𝑔𝑙)) = 0)
172171ancoms 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑔:ℕ–onto𝐴𝑙 ∈ ℕ) ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔𝑙)) = 0)
173172an32s 634 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔𝑙)) = 0)
174169, 173eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔𝑙)) = 0)
175174ralrimiva 3150 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (vol*‘(𝑔𝑙)) = 0)
176 ssralv 3857 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1...𝑚) ⊆ ℕ → (∀𝑙 ∈ ℕ (vol*‘(𝑔𝑙)) = 0 → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0))
17738, 175, 176mpsyl 68 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
178177adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
179178sumeq2d 14649 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = Σ𝑙 ∈ (1...𝑚)0)
18035olci 884 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑚) ⊆ (ℤ‘1) ∨ (1...𝑚) ∈ Fin)
181 sumz 14670 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑚) ⊆ (ℤ‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0)
182180, 181ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 Σ𝑙 ∈ (1...𝑚)0 = 0
183179, 182syl6eq 2852 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔𝑙)) = 0)
184167, 183breqtrd 4863 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0)
185 mblss 23506 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑙) ∈ dom vol → (𝑔𝑙) ⊆ ℝ)
186185ralimi 3136 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
18751, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
188 iunss 4746 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
189187, 188sylibr 225 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
190189adantr 468 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ)
191 ovolge0 23456 . . . . . . . . . . . . . . . . . . . . 21 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ → 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))
193 ovolcl 23453 . . . . . . . . . . . . . . . . . . . . . . 23 ( 𝑙 ∈ (1...𝑚)(𝑔𝑙) ⊆ ℝ → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
194189, 193syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
195194adantr 468 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ*)
196 0xr 10365 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℝ*
197 xrletri3 12197 . . . . . . . . . . . . . . . . . . . . 21 (((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0 ↔ ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))))
198195, 196, 197sylancl 576 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0 ↔ ((vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)))))
199184, 192, 198mpbir2and 695 . . . . . . . . . . . . . . . . . . 19 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0)
200139, 199eqtrd 2836 . . . . . . . . . . . . . . . . . 18 (((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) = 0)
201200mpteq2dva 4931 . . . . . . . . . . . . . . . . 17 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ 0))
202 fconstmpt 5357 . . . . . . . . . . . . . . . . 17 (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
203201, 202syl6eqr 2854 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ (vol‘ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}))
204137, 203eqtrd 2836 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}))
205 frn 6256 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol)
206 ffn 6250 . . . . . . . . . . . . . . . . . . 19 (vol:dom vol⟶(0[,]+∞) → vol Fn dom vol)
207133, 206ax-mp 5 . . . . . . . . . . . . . . . . . 18 vol Fn dom vol
208119, 61fnmpti 6227 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) Fn ℕ
209 fnco 6204 . . . . . . . . . . . . . . . . . 18 ((vol Fn dom vol ∧ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
210207, 208, 209mp3an12 1568 . . . . . . . . . . . . . . . . 17 (ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙)) ⊆ dom vol → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
21155, 205, 2103syl 18 . . . . . . . . . . . . . . . 16 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ)
212 1nn 11310 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
213212ne0ii 4119 . . . . . . . . . . . . . . . 16 ℕ ≠ ∅
214 fconst5 6690 . . . . . . . . . . . . . . . 16 (((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) Fn ℕ ∧ ℕ ≠ ∅) → ((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0}))
215211, 213, 214sylancl 576 . . . . . . . . . . . . . . 15 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ((vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = (ℕ × {0}) ↔ ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0}))
216204, 215mpbid 223 . . . . . . . . . . . . . 14 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ran (vol ∘ (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0})
217131, 216syl5eqr 2850 . . . . . . . . . . . . 13 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))) = {0})
218217supeq1d 8585 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “ ran (𝑚 ∈ ℕ ↦ 𝑙 ∈ (1...𝑚)(𝑔𝑙))), ℝ*, < ) = sup({0}, ℝ*, < ))
219 xrltso 12184 . . . . . . . . . . . . 13 < Or ℝ*
220 supsn 8611 . . . . . . . . . . . . 13 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
221219, 196, 220mp2an 675 . . . . . . . . . . . 12 sup({0}, ℝ*, < ) = 0
222218, 221syl6eq 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 399 . . . . . . . . 9 (𝑔:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 = (vol‘ 𝐴)))
22534, 224syl5 34 . . . . . . . 8 (𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
226225exlimiv 2020 . . . . . . 7 (∃𝑔 𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
22718, 226syl 17 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
228227expimpd 443 . . . . 5 (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
22911, 228pm2.61ine 3057 . . . 4 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴))
230 renepnf 10366 . . . . . . 7 (0 ∈ ℝ → 0 ≠ +∞)
231143, 230mp1i 13 . . . . . 6 ( 𝐴 = ℝ → 0 ≠ +∞)
232 fveq2 6402 . . . . . . 7 ( 𝐴 = ℝ → (vol‘ 𝐴) = (vol‘ℝ))
233 rembl 23515 . . . . . . . . 9 ℝ ∈ dom vol
234 mblvol 23505 . . . . . . . . 9 (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
235233, 234ax-mp 5 . . . . . . . 8 (vol‘ℝ) = (vol*‘ℝ)
236 ovolre 23500 . . . . . . . 8 (vol*‘ℝ) = +∞
237235, 236eqtri 2824 . . . . . . 7 (vol‘ℝ) = +∞
238232, 237syl6eq 2852 . . . . . 6 ( 𝐴 = ℝ → (vol‘ 𝐴) = +∞)
239231, 238neeqtrrd 3048 . . . . 5 ( 𝐴 = ℝ → 0 ≠ (vol‘ 𝐴))
240239necon2i 3008 . . . 4 (0 = (vol‘ 𝐴) → 𝐴 ≠ ℝ)
241229, 240syl 17 . . 3 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 𝐴 ≠ ℝ)
242241expr 446 . 2 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ( 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ))
243 eqimss 3848 . . 3 ( 𝐴 = ℝ → 𝐴 ⊆ ℝ)
244243necon3bi 3000 . 2 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ)
245242, 244pm2.61d1 172 1 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wex 1859  wcel 2155  {cab 2788  wne 2974  wral 3092  wrex 3093  Vcvv 3387  wss 3763  c0 4110  {csn 4364   cuni 4623   ciun 4705   class class class wbr 4837  cmpt 4916   Or wor 5225   × cxp 5303  dom cdm 5305  ran crn 5306  cima 5308  ccom 5309   Fn wfn 6090  wf 6091  ontowfo 6093  cfv 6095  (class class class)co 6868  cdom 8184  csdm 8185  Fincfn 8186  supcsup 8579  cr 10214  0cc0 10215  1c1 10216   + caddc 10218  +∞cpnf 10350  *cxr 10352   < clt 10353  cle 10354  cn 11299  cuz 11898  [,]cicc 12390  ...cfz 12543  Σcsu 14633  vol*covol 23437  volcvol 23438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-inf2 8779  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292  ax-pre-sup 10293
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-se 5265  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-isom 6104  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-of 7121  df-om 7290  df-1st 7392  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-1o 7790  df-2o 7791  df-oadd 7794  df-er 7973  df-map 8088  df-en 8187  df-dom 8188  df-sdom 8189  df-fin 8190  df-fi 8550  df-sup 8581  df-inf 8582  df-oi 8648  df-card 9042  df-cda 9269  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-2 11358  df-3 11359  df-n0 11554  df-z 11638  df-uz 11899  df-q 12002  df-rp 12041  df-xneg 12156  df-xadd 12157  df-xmul 12158  df-ioo 12391  df-ico 12393  df-icc 12394  df-fz 12544  df-fzo 12684  df-fl 12811  df-seq 13019  df-exp 13078  df-hash 13332  df-cj 14056  df-re 14057  df-im 14058  df-sqrt 14192  df-abs 14193  df-clim 14436  df-sum 14634  df-rest 16282  df-topgen 16303  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-top 20906  df-topon 20923  df-bases 20958  df-cmp 21398  df-ovol 23439  df-vol 23440
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator