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

Theorem voliunnfl 33787
Description: voliun 23543 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.)
Hypotheses
Ref Expression
voliunnfl.1 𝑆 = seq1( + , 𝐺)
voliunnfl.2 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))
voliunnfl.3 ((∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = sup(ran 𝑆, ℝ*, < ))
Assertion
Ref Expression
voliunnfl ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
Distinct variable group:   𝑓,𝑛,𝑥,𝐴
Allowed substitution hints:   𝑆(𝑥,𝑓,𝑛)   𝐺(𝑥,𝑓,𝑛)

Proof of Theorem voliunnfl
Dummy variables 𝑔 𝑚 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 4583 . . . . . . . . 9 (𝐴 = ∅ → 𝐴 = ∅)
2 uni0 4602 . . . . . . . . 9 ∅ = ∅
31, 2syl6eq 2821 . . . . . . . 8 (𝐴 = ∅ → 𝐴 = ∅)
43fveq2d 6337 . . . . . . 7 (𝐴 = ∅ → (vol‘ 𝐴) = (vol‘∅))
5 0mbl 23528 . . . . . . . . 9 ∅ ∈ dom vol
6 mblvol 23519 . . . . . . . . 9 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
75, 6ax-mp 5 . . . . . . . 8 (vol‘∅) = (vol*‘∅)
8 ovol0 23482 . . . . . . . 8 (vol*‘∅) = 0
97, 8eqtri 2793 . . . . . . 7 (vol‘∅) = 0
104, 9syl6req 2822 . . . . . 6 (𝐴 = ∅ → 0 = (vol‘ 𝐴))
1110a1d 25 . . . . 5 (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
12 reldom 8116 . . . . . . . . . . 11 Rel ≼
1312brrelexi 5299 . . . . . . . . . 10 (𝐴 ≼ ℕ → 𝐴 ∈ V)
14 0sdomg 8246 . . . . . . . . . 10 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1513, 14syl 17 . . . . . . . . 9 (𝐴 ≼ ℕ → (∅ ≺ 𝐴𝐴 ≠ ∅))
1615biimparc 465 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17 fodomr 8268 . . . . . . . 8 ((∅ ≺ 𝐴𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
1816, 17sylancom 570 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
19 unissb 4606 . . . . . . . . . . . . 13 ( 𝐴 ⊆ ℝ ↔ ∀𝑥𝐴 𝑥 ⊆ ℝ)
2019anbi1i 604 . . . . . . . . . . . 12 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
21 r19.26 3212 . . . . . . . . . . . 12 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
2220, 21bitr4i 267 . . . . . . . . . . 11 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23 ovolctb2 23481 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
2423ex 397 . . . . . . . . . . . . 13 (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ → (vol*‘𝑥) = 0))
2524imdistani 552 . . . . . . . . . . . 12 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
2625ralimi 3101 . . . . . . . . . . 11 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
2722, 26sylbi 207 . . . . . . . . . 10 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
2827ancoms 455 . . . . . . . . 9 ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
29 foima 6262 . . . . . . . . . . . 12 (𝑔:ℕ–onto𝐴 → (𝑔 “ ℕ) = 𝐴)
3029raleqdv 3293 . . . . . . . . . . 11 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)))
31 fofn 6259 . . . . . . . . . . . 12 (𝑔:ℕ–onto𝐴𝑔 Fn ℕ)
32 ssid 3774 . . . . . . . . . . . 12 ℕ ⊆ ℕ
33 sseq1 3776 . . . . . . . . . . . . . 14 (𝑥 = (𝑔𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔𝑚) ⊆ ℝ))
34 fveq2 6333 . . . . . . . . . . . . . . 15 (𝑥 = (𝑔𝑚) → (vol*‘𝑥) = (vol*‘(𝑔𝑚)))
3534eqeq1d 2773 . . . . . . . . . . . . . 14 (𝑥 = (𝑔𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔𝑚)) = 0))
3633, 35anbi12d 610 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)))
3736ralima 6642 . . . . . . . . . . . 12 ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)))
3831, 32, 37sylancl 568 . . . . . . . . . . 11 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)))
3930, 38bitr3d 270 . . . . . . . . . 10 (𝑔:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)))
40 difss 3889 . . . . . . . . . . . . . . . . . 18 ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ (𝑔𝑚)
41 ovolssnul 23476 . . . . . . . . . . . . . . . . . 18 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ (𝑔𝑚) ∧ (𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0)
4240, 41mp3an1 1559 . . . . . . . . . . . . . . . . 17 (((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0)
43 ssdifss 3893 . . . . . . . . . . . . . . . . . 18 ((𝑔𝑚) ⊆ ℝ → ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ ℝ)
44 nulmbl 23524 . . . . . . . . . . . . . . . . . . 19 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol)
45 mblvol 23519 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))))
4645eqeq1d 2773 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → ((vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0 ↔ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0))
4746biimpar 463 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0)
48 0re 10243 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ
4947, 48syl6eqel 2858 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ)
5049expcom 398 . . . . . . . . . . . . . . . . . . . . 21 ((vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0 → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
5150ancld 534 . . . . . . . . . . . . . . . . . . . 20 ((vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0 → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ)))
5251adantl 467 . . . . . . . . . . . . . . . . . . 19 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ)))
5344, 52mpd 15 . . . . . . . . . . . . . . . . . 18 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
5443, 53sylan 563 . . . . . . . . . . . . . . . . 17 (((𝑔𝑚) ⊆ ℝ ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
5542, 54syldan 573 . . . . . . . . . . . . . . . 16 (((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
5655ralimi 3101 . . . . . . . . . . . . . . 15 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
57 fveq2 6333 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑔𝑚) = (𝑔𝑛))
58 oveq2 6802 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛))
5958iuneq1d 4680 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 𝑙 ∈ (1..^𝑚)(𝑔𝑙) = 𝑙 ∈ (1..^𝑛)(𝑔𝑙))
6057, 59difeq12d 3881 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) = ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))
61 eqid 2771 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))
62 fvex 6343 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑛) ∈ V
63 difexg 4943 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔𝑛) ∈ V → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ V)
6462, 63ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ V
6560, 61, 64fvmpt 6425 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) = ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))
6665eleq1d 2835 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol))
6765fveq2d 6337 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
6867eleq1d 2835 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ))
6966, 68anbi12d 610 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ)))
7069ralbiia 3128 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ))
71 fveq2 6333 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑚 → (𝑔𝑛) = (𝑔𝑚))
72 oveq2 6802 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚))
7372iuneq1d 4680 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑚 𝑙 ∈ (1..^𝑛)(𝑔𝑙) = 𝑙 ∈ (1..^𝑚)(𝑔𝑙))
7471, 73difeq12d 3881 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑚 → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) = ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))
7574eleq1d 2835 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ↔ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol))
7674fveq2d 6337 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑚 → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))))
7776eleq1d 2835 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → ((vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ ↔ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
7875, 77anbi12d 610 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → ((((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ) ↔ (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ)))
7978cbvralv 3320 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ℕ (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
8070, 79bitri 264 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
8156, 80sylibr 224 . . . . . . . . . . . . . 14 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ))
82 fveq2 6333 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑙 → (𝑔𝑛) = (𝑔𝑙))
8382iundisj2 23538 . . . . . . . . . . . . . . 15 Disj 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))
84 disjeq2 4759 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) = ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
8584, 65mprg 3075 . . . . . . . . . . . . . . 15 (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))
8683, 85mpbir 221 . . . . . . . . . . . . . 14 Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)
87 nnex 11229 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
8887mptex 6631 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ V
89 fveq1 6332 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (𝑓𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))
9089eleq1d 2835 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ((𝑓𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol))
9189fveq2d 6337 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (vol‘(𝑓𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))
9291eleq1d 2835 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ((vol‘(𝑓𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ))
9390, 92anbi12d 610 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ)))
9493ralbidv 3135 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ)))
9589adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))
9695disjeq2dv 4760 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))
9794, 96anbi12d 610 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))))
9889iuneq2d 4682 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → 𝑛 ∈ ℕ (𝑓𝑛) = 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))
9998fveq2d 6337 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))
100 voliunnfl.1 . . . . . . . . . . . . . . . . . . . . . 22 𝑆 = seq1( + , 𝐺)
101 voliunnfl.2 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))
102 seqeq3 13014 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))))
103101, 102ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))))
104100, 103eqtri 2793 . . . . . . . . . . . . . . . . . . . . 21 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))))
105104rneqi 5491 . . . . . . . . . . . . . . . . . . . 20 ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))))
106105supeq1i 8510 . . . . . . . . . . . . . . . . . . 19 sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))), ℝ*, < )
10791mpteq2dv 4880 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))))
108107seqeq3d 13017 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))))
109108rneqd 5492 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))))
110109supeq1d 8509 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ))
111106, 110syl5eq 2817 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ))
11299, 111eqeq12d 2786 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ((vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = sup(ran 𝑆, ℝ*, < ) ↔ (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < )))
11397, 112imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (((∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = sup(ran 𝑆, ℝ*, < )) ↔ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) → (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ))))
114 voliunnfl.3 . . . . . . . . . . . . . . . 16 ((∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = sup(ran 𝑆, ℝ*, < ))
11588, 113, 114vtocl 3411 . . . . . . . . . . . . . . 15 ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) → (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ))
11665iuneq2i 4674 . . . . . . . . . . . . . . . 16 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) = 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))
117116fveq2i 6336 . . . . . . . . . . . . . . 15 (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))
11867mpteq2ia 4875 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
119 seqeq3 13014 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))))
120118, 119ax-mp 5 . . . . . . . . . . . . . . . . 17 seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))))
121120rneqi 5491 . . . . . . . . . . . . . . . 16 ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))))
122121supeq1i 8510 . . . . . . . . . . . . . . 15 sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < )
123115, 117, 1223eqtr3g 2828 . . . . . . . . . . . . . 14 ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ))
12481, 86, 123sylancl 568 . . . . . . . . . . . . 13 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ))
125124adantl 467 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)) → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ))
12682iundisj 23537 . . . . . . . . . . . . . . . 16 𝑛 ∈ ℕ (𝑔𝑛) = 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))
127 fofun 6258 . . . . . . . . . . . . . . . . 17 (𝑔:ℕ–onto𝐴 → Fun 𝑔)
128 funiunfv 6650 . . . . . . . . . . . . . . . . 17 (Fun 𝑔 𝑛 ∈ ℕ (𝑔𝑛) = (𝑔 “ ℕ))
129127, 128syl 17 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴 𝑛 ∈ ℕ (𝑔𝑛) = (𝑔 “ ℕ))
130126, 129syl5eqr 2819 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) = (𝑔 “ ℕ))
13129unieqd 4585 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 (𝑔 “ ℕ) = 𝐴)
132130, 131eqtrd 2805 . . . . . . . . . . . . . 14 (𝑔:ℕ–onto𝐴 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) = 𝐴)
133132fveq2d 6337 . . . . . . . . . . . . 13 (𝑔:ℕ–onto𝐴 → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol‘ 𝐴))
134133adantr 466 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)) → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol‘ 𝐴))
13557sseq1d 3782 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → ((𝑔𝑚) ⊆ ℝ ↔ (𝑔𝑛) ⊆ ℝ))
13657fveq2d 6337 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 → (vol*‘(𝑔𝑚)) = (vol*‘(𝑔𝑛)))
137136eqeq1d 2773 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → ((vol*‘(𝑔𝑚)) = 0 ↔ (vol*‘(𝑔𝑛)) = 0))
138135, 137anbi12d 610 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) ↔ ((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0)))
139138rspccva 3460 . . . . . . . . . . . . . . . . . . 19 ((∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0))
140 ssdifss 3893 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔𝑛) ⊆ ℝ → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ ℝ)
141140adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ ℝ)
142 difss 3889 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ (𝑔𝑛)
143 ovolssnul 23476 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ (𝑔𝑛) ∧ (𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0)
144142, 143mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0)
145141, 144jca 497 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0))
146 nulmbl 23524 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0) → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol)
147 mblvol 23519 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
148145, 146, 1473syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
149148, 144eqtrd 2805 . . . . . . . . . . . . . . . . . . 19 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0)
150139, 149syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0)
151150mpteq2dva 4879 . . . . . . . . . . . . . . . . 17 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))) = (𝑛 ∈ ℕ ↦ 0))
152151seqeq3d 13017 . . . . . . . . . . . . . . . 16 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
153152rneqd 5492 . . . . . . . . . . . . . . 15 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0)))
154153supeq1d 8509 . . . . . . . . . . . . . 14 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ))
155 0cn 10235 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
156 ser1const 13065 . . . . . . . . . . . . . . . . . . . . . 22 ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
157155, 156mpan 664 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
158 nncn 11231 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
159158mul01d 10438 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → (𝑚 · 0) = 0)
160157, 159eqtrd 2805 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = 0)
161160mpteq2ia 4875 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0)
162 fconstmpt 5304 . . . . . . . . . . . . . . . . . . . . 21 (ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0)
163 seqeq3 13014 . . . . . . . . . . . . . . . . . . . . 21 ((ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
164162, 163ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0))
165 1z 11610 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℤ
166 seqfn 13021 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ ℤ → seq1( + , (ℕ × {0})) Fn (ℤ‘1))
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 seq1( + , (ℕ × {0})) Fn (ℤ‘1)
168 nnuz 11926 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
169168fneq2i 6127 . . . . . . . . . . . . . . . . . . . . . 22 (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn (ℤ‘1))
170 dffn5 6384 . . . . . . . . . . . . . . . . . . . . . 22 (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
171169, 170bitr3i 266 . . . . . . . . . . . . . . . . . . . . 21 (seq1( + , (ℕ × {0})) Fn (ℤ‘1) ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
172167, 171mpbi 220 . . . . . . . . . . . . . . . . . . . 20 seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
173164, 172eqtr3i 2795 . . . . . . . . . . . . . . . . . . 19 seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
174 fconstmpt 5304 . . . . . . . . . . . . . . . . . . 19 (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
175161, 173, 1743eqtr4i 2803 . . . . . . . . . . . . . . . . . 18 seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (ℕ × {0})
176175rneqi 5491 . . . . . . . . . . . . . . . . 17 ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = ran (ℕ × {0})
177 1nn 11234 . . . . . . . . . . . . . . . . . 18 1 ∈ ℕ
178 ne0i 4070 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℕ → ℕ ≠ ∅)
179 rnxp 5706 . . . . . . . . . . . . . . . . . 18 (ℕ ≠ ∅ → ran (ℕ × {0}) = {0})
180177, 178, 179mp2b 10 . . . . . . . . . . . . . . . . 17 ran (ℕ × {0}) = {0}
181176, 180eqtri 2793 . . . . . . . . . . . . . . . 16 ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = {0}
182181supeq1i 8510 . . . . . . . . . . . . . . 15 sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = sup({0}, ℝ*, < )
183 xrltso 12180 . . . . . . . . . . . . . . . 16 < Or ℝ*
184 0xr 10289 . . . . . . . . . . . . . . . 16 0 ∈ ℝ*
185 supsn 8535 . . . . . . . . . . . . . . . 16 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
186183, 184, 185mp2an 666 . . . . . . . . . . . . . . 15 sup({0}, ℝ*, < ) = 0
187182, 186eqtri 2793 . . . . . . . . . . . . . 14 sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = 0
188154, 187syl6eq 2821 . . . . . . . . . . . . 13 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ) = 0)
189188adantl 467 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ) = 0)
190125, 134, 1893eqtr3rd 2814 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)) → 0 = (vol‘ 𝐴))
191190ex 397 . . . . . . . . . 10 (𝑔:ℕ–onto𝐴 → (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → 0 = (vol‘ 𝐴)))
19239, 191sylbid 230 . . . . . . . . 9 (𝑔:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 = (vol‘ 𝐴)))
19328, 192syl5 34 . . . . . . . 8 (𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
194193exlimiv 2010 . . . . . . 7 (∃𝑔 𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
19518, 194syl 17 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
196195expimpd 441 . . . . 5 (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
19711, 196pm2.61ine 3026 . . . 4 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴))
198 renepnf 10290 . . . . . . 7 (0 ∈ ℝ → 0 ≠ +∞)
19948, 198mp1i 13 . . . . . 6 ( 𝐴 = ℝ → 0 ≠ +∞)
200 fveq2 6333 . . . . . . 7 ( 𝐴 = ℝ → (vol‘ 𝐴) = (vol‘ℝ))
201 rembl 23529 . . . . . . . . 9 ℝ ∈ dom vol
202 mblvol 23519 . . . . . . . . 9 (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
203201, 202ax-mp 5 . . . . . . . 8 (vol‘ℝ) = (vol*‘ℝ)
204 ovolre 23514 . . . . . . . 8 (vol*‘ℝ) = +∞
205203, 204eqtri 2793 . . . . . . 7 (vol‘ℝ) = +∞
206200, 205syl6eq 2821 . . . . . 6 ( 𝐴 = ℝ → (vol‘ 𝐴) = +∞)
207199, 206neeqtrrd 3017 . . . . 5 ( 𝐴 = ℝ → 0 ≠ (vol‘ 𝐴))
208207necon2i 2977 . . . 4 (0 = (vol‘ 𝐴) → 𝐴 ≠ ℝ)
209197, 208syl 17 . . 3 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 𝐴 ≠ ℝ)
210209expr 444 . 2 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ( 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ))
211 eqimss 3807 . . 3 ( 𝐴 = ℝ → 𝐴 ⊆ ℝ)
212211necon3bi 2969 . 2 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ)
213210, 212pm2.61d1 172 1 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  Vcvv 3351  cdif 3721  wss 3724  c0 4064  {csn 4317   cuni 4575   ciun 4655  Disj wdisj 4755   class class class wbr 4787  cmpt 4864   Or wor 5170   × cxp 5248  dom cdm 5250  ran crn 5251  cima 5253  Fun wfun 6026   Fn wfn 6027  ontowfo 6030  cfv 6032  (class class class)co 6794  cdom 8108  csdm 8109  supcsup 8503  cc 10137  cr 10138  0cc0 10139  1c1 10140   + caddc 10142   · cmul 10144  +∞cpnf 10274  *cxr 10276   < clt 10277  cn 11223  cz 11580  cuz 11889  ..^cfzo 12674  seqcseq 13009  vol*covol 23451  volcvol 23452
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 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-inf2 8703  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  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 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-disj 4756  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-of 7045  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-oadd 7718  df-er 7897  df-map 8012  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8966  df-cda 9193  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-n0 11496  df-z 11581  df-uz 11890  df-q 11993  df-rp 12037  df-xneg 12152  df-xadd 12153  df-xmul 12154  df-ioo 12385  df-ico 12387  df-icc 12388  df-fz 12535  df-fzo 12675  df-fl 12802  df-seq 13010  df-exp 13069  df-hash 13323  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-clim 14428  df-sum 14626  df-rest 16292  df-topgen 16313  df-psmet 19954  df-xmet 19955  df-met 19956  df-bl 19957  df-mopn 19958  df-top 20920  df-topon 20937  df-bases 20972  df-cmp 21412  df-ovol 23453  df-vol 23454
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator