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 37671
Description: voliun 25589 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 4918 . . . . . . . . 9 (𝐴 = ∅ → 𝐴 = ∅)
2 uni0 4935 . . . . . . . . 9 ∅ = ∅
31, 2eqtrdi 2793 . . . . . . . 8 (𝐴 = ∅ → 𝐴 = ∅)
43fveq2d 6910 . . . . . . 7 (𝐴 = ∅ → (vol‘ 𝐴) = (vol‘∅))
5 0mbl 25574 . . . . . . . . 9 ∅ ∈ dom vol
6 mblvol 25565 . . . . . . . . 9 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
75, 6ax-mp 5 . . . . . . . 8 (vol‘∅) = (vol*‘∅)
8 ovol0 25528 . . . . . . . 8 (vol*‘∅) = 0
97, 8eqtri 2765 . . . . . . 7 (vol‘∅) = 0
104, 9eqtr2di 2794 . . . . . 6 (𝐴 = ∅ → 0 = (vol‘ 𝐴))
1110a1d 25 . . . . 5 (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
12 reldom 8991 . . . . . . . . . . 11 Rel ≼
1312brrelex1i 5741 . . . . . . . . . 10 (𝐴 ≼ ℕ → 𝐴 ∈ V)
14 0sdomg 9144 . . . . . . . . . 10 (𝐴 ∈ V → (∅ ≺ 𝐴𝐴 ≠ ∅))
1513, 14syl 17 . . . . . . . . 9 (𝐴 ≼ ℕ → (∅ ≺ 𝐴𝐴 ≠ ∅))
1615biimparc 479 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅ ≺ 𝐴)
17 fodomr 9168 . . . . . . . 8 ((∅ ≺ 𝐴𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
1816, 17sylancom 588 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto𝐴)
19 unissb 4939 . . . . . . . . . . . . 13 ( 𝐴 ⊆ ℝ ↔ ∀𝑥𝐴 𝑥 ⊆ ℝ)
2019anbi1i 624 . . . . . . . . . . . 12 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
21 r19.26 3111 . . . . . . . . . . . 12 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ))
2220, 21bitr4i 278 . . . . . . . . . . 11 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ))
23 ovolctb2 25527 . . . . . . . . . . . . . 14 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (vol*‘𝑥) = 0)
2423ex 412 . . . . . . . . . . . . 13 (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ → (vol*‘𝑥) = 0))
2524imdistani 568 . . . . . . . . . . . 12 ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
2625ralimi 3083 . . . . . . . . . . 11 (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
2722, 26sylbi 217 . . . . . . . . . 10 (( 𝐴 ⊆ ℝ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
2827ancoms 458 . . . . . . . . 9 ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))
29 foima 6825 . . . . . . . . . . . 12 (𝑔:ℕ–onto𝐴 → (𝑔 “ ℕ) = 𝐴)
3029raleqdv 3326 . . . . . . . . . . 11 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)))
31 fofn 6822 . . . . . . . . . . . 12 (𝑔:ℕ–onto𝐴𝑔 Fn ℕ)
32 ssid 4006 . . . . . . . . . . . 12 ℕ ⊆ ℕ
33 sseq1 4009 . . . . . . . . . . . . . 14 (𝑥 = (𝑔𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔𝑚) ⊆ ℝ))
34 fveqeq2 6915 . . . . . . . . . . . . . 14 (𝑥 = (𝑔𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔𝑚)) = 0))
3533, 34anbi12d 632 . . . . . . . . . . . . 13 (𝑥 = (𝑔𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)))
3635ralima 7257 . . . . . . . . . . . 12 ((𝑔 Fn ℕ ∧ ℕ ⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)))
3731, 32, 36sylancl 586 . . . . . . . . . . 11 (𝑔:ℕ–onto𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)))
3830, 37bitr3d 281 . . . . . . . . . 10 (𝑔:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)))
39 difss 4136 . . . . . . . . . . . . . . . . . 18 ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ (𝑔𝑚)
40 ovolssnul 25522 . . . . . . . . . . . . . . . . . 18 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ (𝑔𝑚) ∧ (𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0)
4139, 40mp3an1 1450 . . . . . . . . . . . . . . . . 17 (((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0)
42 ssdifss 4140 . . . . . . . . . . . . . . . . . 18 ((𝑔𝑚) ⊆ ℝ → ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ ℝ)
43 nulmbl 25570 . . . . . . . . . . . . . . . . . . 19 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol)
44 mblvol 25565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))))
4544eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → ((vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0 ↔ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0))
4645biimpar 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0)
47 0re 11263 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ
4846, 47eqeltrdi 2849 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ)
4948expcom 413 . . . . . . . . . . . . . . . . . . . . 21 ((vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0 → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
5049ancld 550 . . . . . . . . . . . . . . . . . . . 20 ((vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0 → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ)))
5150adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ)))
5243, 51mpd 15 . . . . . . . . . . . . . . . . . 18 ((((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
5342, 52sylan 580 . . . . . . . . . . . . . . . . 17 (((𝑔𝑚) ⊆ ℝ ∧ (vol*‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = 0) → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
5441, 53syldan 591 . . . . . . . . . . . . . . . 16 (((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
5554ralimi 3083 . . . . . . . . . . . . . . 15 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
56 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑔𝑚) = (𝑔𝑛))
57 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛))
5857iuneq1d 5019 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 𝑙 ∈ (1..^𝑚)(𝑔𝑙) = 𝑙 ∈ (1..^𝑛)(𝑔𝑙))
5956, 58difeq12d 4127 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) = ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))
60 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))
61 fvex 6919 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑛) ∈ V
62 difexg 5329 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔𝑛) ∈ V → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ V)
6361, 62ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ V
6459, 60, 63fvmpt 7016 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) = ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))
6564eleq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol))
6664fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
6766eleq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ))
6865, 67anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ)))
6968ralbiia 3091 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ))
70 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑚 → (𝑔𝑛) = (𝑔𝑚))
71 oveq2 7439 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚))
7271iuneq1d 5019 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑚 𝑙 ∈ (1..^𝑛)(𝑔𝑙) = 𝑙 ∈ (1..^𝑚)(𝑔𝑙))
7370, 72difeq12d 4127 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑚 → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) = ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))
7473eleq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ↔ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol))
7573fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑚 → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))))
7675eleq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → ((vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ ↔ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
7774, 76anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → ((((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ) ↔ (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ)))
7877cbvralvw 3237 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ℕ (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
7969, 78bitri 275 . . . . . . . . . . . . . . 15 (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)) ∈ dom vol ∧ (vol‘((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ ℝ))
8055, 79sylibr 234 . . . . . . . . . . . . . 14 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ))
81 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑙 → (𝑔𝑛) = (𝑔𝑙))
8281iundisj2 25584 . . . . . . . . . . . . . . 15 Disj 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))
83 disjeq2 5114 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) = ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
8483, 64mprg 3067 . . . . . . . . . . . . . . 15 (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))
8582, 84mpbir 231 . . . . . . . . . . . . . 14 Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)
86 nnex 12272 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
8786mptex 7243 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∈ V
88 fveq1 6905 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (𝑓𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))
8988eleq1d 2826 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ((𝑓𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol))
9088fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (vol‘(𝑓𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))
9190eleq1d 2826 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ((vol‘(𝑓𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ))
9289, 91anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ)))
9392ralbidv 3178 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ)))
9488adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))
9594disjeq2dv 5115 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))
9693, 95anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))))
9788iuneq2d 5022 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → 𝑛 ∈ ℕ (𝑓𝑛) = 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))
9897fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))
99 voliunnfl.1 . . . . . . . . . . . . . . . . . . . . . 22 𝑆 = seq1( + , 𝐺)
100 voliunnfl.2 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))
101 seqeq3 14047 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))))
102100, 101ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))))
10399, 102eqtri 2765 . . . . . . . . . . . . . . . . . . . . 21 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))))
104103rneqi 5948 . . . . . . . . . . . . . . . . . . . 20 ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))))
105104supeq1i 9487 . . . . . . . . . . . . . . . . . . 19 sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))), ℝ*, < )
10690mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))))
107106seqeq3d 14050 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))))
108107rneqd 5949 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))))
109108supeq1d 9486 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ))
110105, 109eqtrid 2789 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ))
11198, 110eqeq12d 2753 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → ((vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = sup(ran 𝑆, ℝ*, < ) ↔ (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < )))
11296, 111imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙))) → (((∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = sup(ran 𝑆, ℝ*, < )) ↔ ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) → (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ))))
113 voliunnfl.3 . . . . . . . . . . . . . . . 16 ((∀𝑛 ∈ ℕ ((𝑓𝑛) ∈ dom vol ∧ (vol‘(𝑓𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = sup(ran 𝑆, ℝ*, < ))
11487, 112, 113vtocl 3558 . . . . . . . . . . . . . . 15 ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) → (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ))
11564iuneq2i 5013 . . . . . . . . . . . . . . . 16 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) = 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))
116115fveq2i 6909 . . . . . . . . . . . . . . 15 (vol‘ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) = (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))
11766mpteq2ia 5245 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
118 seqeq3 14047 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))))
119117, 118ax-mp 5 . . . . . . . . . . . . . . . . 17 seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))))
120119rneqi 5948 . . . . . . . . . . . . . . . 16 ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))))
121120supeq1i 9487 . . . . . . . . . . . . . . 15 sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < )
122114, 116, 1213eqtr3g 2800 . . . . . . . . . . . . . 14 ((∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔𝑚) ∖ 𝑙 ∈ (1..^𝑚)(𝑔𝑙)))‘𝑛)) → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ))
12380, 85, 122sylancl 586 . . . . . . . . . . . . 13 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ))
124123adantl 481 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)) → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ))
12581iundisj 25583 . . . . . . . . . . . . . . . 16 𝑛 ∈ ℕ (𝑔𝑛) = 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))
126 fofun 6821 . . . . . . . . . . . . . . . . 17 (𝑔:ℕ–onto𝐴 → Fun 𝑔)
127 funiunfv 7268 . . . . . . . . . . . . . . . . 17 (Fun 𝑔 𝑛 ∈ ℕ (𝑔𝑛) = (𝑔 “ ℕ))
128126, 127syl 17 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto𝐴 𝑛 ∈ ℕ (𝑔𝑛) = (𝑔 “ ℕ))
129125, 128eqtr3id 2791 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) = (𝑔 “ ℕ))
13029unieqd 4920 . . . . . . . . . . . . . . 15 (𝑔:ℕ–onto𝐴 (𝑔 “ ℕ) = 𝐴)
131129, 130eqtrd 2777 . . . . . . . . . . . . . 14 (𝑔:ℕ–onto𝐴 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) = 𝐴)
132131fveq2d 6910 . . . . . . . . . . . . 13 (𝑔:ℕ–onto𝐴 → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol‘ 𝐴))
133132adantr 480 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)) → (vol‘ 𝑛 ∈ ℕ ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol‘ 𝐴))
13456sseq1d 4015 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → ((𝑔𝑚) ⊆ ℝ ↔ (𝑔𝑛) ⊆ ℝ))
13556fveqeq2d 6914 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → ((vol*‘(𝑔𝑚)) = 0 ↔ (vol*‘(𝑔𝑛)) = 0))
136134, 135anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) ↔ ((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0)))
137136rspccva 3621 . . . . . . . . . . . . . . . . . . 19 ((∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0))
138 ssdifss 4140 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔𝑛) ⊆ ℝ → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ ℝ)
139138adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ ℝ)
140 difss 4136 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ (𝑔𝑛)
141 ovolssnul 25522 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ (𝑔𝑛) ∧ (𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0)
142140, 141mp3an1 1450 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0)
143139, 142jca 511 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0))
144 nulmbl 25570 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0) → ((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol)
145 mblvol 25565 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)) ∈ dom vol → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
146143, 144, 1453syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = (vol*‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))
147146, 142eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 (((𝑔𝑛) ⊆ ℝ ∧ (vol*‘(𝑔𝑛)) = 0) → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0)
148137, 147syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))) = 0)
149148mpteq2dva 5242 . . . . . . . . . . . . . . . . 17 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙)))) = (𝑛 ∈ ℕ ↦ 0))
150149seqeq3d 14050 . . . . . . . . . . . . . . . 16 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
151150rneqd 5949 . . . . . . . . . . . . . . 15 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0)))
152151supeq1d 9486 . . . . . . . . . . . . . 14 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ))
153 0cn 11253 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℂ
154 ser1const 14099 . . . . . . . . . . . . . . . . . . . . . 22 ((0 ∈ ℂ ∧ 𝑚 ∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
155153, 154mpan 690 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0))
156 nncn 12274 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
157156mul01d 11460 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → (𝑚 · 0) = 0)
158155, 157eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → (seq1( + , (ℕ × {0}))‘𝑚) = 0)
159158mpteq2ia 5245 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0)
160 fconstmpt 5747 . . . . . . . . . . . . . . . . . . . . 21 (ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0)
161 seqeq3 14047 . . . . . . . . . . . . . . . . . . . . 21 ((ℕ × {0}) = (𝑛 ∈ ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)))
162160, 161ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0))
163 1z 12647 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℤ
164 seqfn 14054 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ ℤ → seq1( + , (ℕ × {0})) Fn (ℤ‘1))
165163, 164ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 seq1( + , (ℕ × {0})) Fn (ℤ‘1)
166 nnuz 12921 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
167166fneq2i 6666 . . . . . . . . . . . . . . . . . . . . . 22 (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn (ℤ‘1))
168 dffn5 6967 . . . . . . . . . . . . . . . . . . . . . 22 (seq1( + , (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
169167, 168bitr3i 277 . . . . . . . . . . . . . . . . . . . . 21 (seq1( + , (ℕ × {0})) Fn (ℤ‘1) ↔ seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)))
170165, 169mpbi 230 . . . . . . . . . . . . . . . . . . . 20 seq1( + , (ℕ × {0})) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
171162, 170eqtr3i 2767 . . . . . . . . . . . . . . . . . . 19 seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (𝑚 ∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))
172 fconstmpt 5747 . . . . . . . . . . . . . . . . . . 19 (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
173159, 171, 1723eqtr4i 2775 . . . . . . . . . . . . . . . . . 18 seq1( + , (𝑛 ∈ ℕ ↦ 0)) = (ℕ × {0})
174173rneqi 5948 . . . . . . . . . . . . . . . . 17 ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = ran (ℕ × {0})
175 1nn 12277 . . . . . . . . . . . . . . . . . 18 1 ∈ ℕ
176 ne0i 4341 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℕ → ℕ ≠ ∅)
177 rnxp 6190 . . . . . . . . . . . . . . . . . 18 (ℕ ≠ ∅ → ran (ℕ × {0}) = {0})
178175, 176, 177mp2b 10 . . . . . . . . . . . . . . . . 17 ran (ℕ × {0}) = {0}
179174, 178eqtri 2765 . . . . . . . . . . . . . . . 16 ran seq1( + , (𝑛 ∈ ℕ ↦ 0)) = {0}
180179supeq1i 9487 . . . . . . . . . . . . . . 15 sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = sup({0}, ℝ*, < )
181 xrltso 13183 . . . . . . . . . . . . . . . 16 < Or ℝ*
182 0xr 11308 . . . . . . . . . . . . . . . 16 0 ∈ ℝ*
183 supsn 9512 . . . . . . . . . . . . . . . 16 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
184181, 182, 183mp2an 692 . . . . . . . . . . . . . . 15 sup({0}, ℝ*, < ) = 0
185180, 184eqtri 2765 . . . . . . . . . . . . . 14 sup(ran seq1( + , (𝑛 ∈ ℕ ↦ 0)), ℝ*, < ) = 0
186152, 185eqtrdi 2793 . . . . . . . . . . . . 13 (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ) = 0)
187186adantl 481 . . . . . . . . . . . 12 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔𝑛) ∖ 𝑙 ∈ (1..^𝑛)(𝑔𝑙))))), ℝ*, < ) = 0)
188124, 133, 1873eqtr3rd 2786 . . . . . . . . . . 11 ((𝑔:ℕ–onto𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0)) → 0 = (vol‘ 𝐴))
189188ex 412 . . . . . . . . . 10 (𝑔:ℕ–onto𝐴 → (∀𝑚 ∈ ℕ ((𝑔𝑚) ⊆ ℝ ∧ (vol*‘(𝑔𝑚)) = 0) → 0 = (vol‘ 𝐴)))
19038, 189sylbid 240 . . . . . . . . 9 (𝑔:ℕ–onto𝐴 → (∀𝑥𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 = (vol‘ 𝐴)))
19128, 190syl5 34 . . . . . . . 8 (𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
192191exlimiv 1930 . . . . . . 7 (∃𝑔 𝑔:ℕ–onto𝐴 → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
19318, 192syl 17 . . . . . 6 ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ((∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ) → 0 = (vol‘ 𝐴)))
194193expimpd 453 . . . . 5 (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴)))
19511, 194pm2.61ine 3025 . . . 4 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 0 = (vol‘ 𝐴))
196 renepnf 11309 . . . . . . 7 (0 ∈ ℝ → 0 ≠ +∞)
19747, 196mp1i 13 . . . . . 6 ( 𝐴 = ℝ → 0 ≠ +∞)
198 fveq2 6906 . . . . . . 7 ( 𝐴 = ℝ → (vol‘ 𝐴) = (vol‘ℝ))
199 rembl 25575 . . . . . . . . 9 ℝ ∈ dom vol
200 mblvol 25565 . . . . . . . . 9 (ℝ ∈ dom vol → (vol‘ℝ) = (vol*‘ℝ))
201199, 200ax-mp 5 . . . . . . . 8 (vol‘ℝ) = (vol*‘ℝ)
202 ovolre 25560 . . . . . . . 8 (vol*‘ℝ) = +∞
203201, 202eqtri 2765 . . . . . . 7 (vol‘ℝ) = +∞
204198, 203eqtrdi 2793 . . . . . 6 ( 𝐴 = ℝ → (vol‘ 𝐴) = +∞)
205197, 204neeqtrrd 3015 . . . . 5 ( 𝐴 = ℝ → 0 ≠ (vol‘ 𝐴))
206205necon2i 2975 . . . 4 (0 = (vol‘ 𝐴) → 𝐴 ≠ ℝ)
207195, 206syl 17 . . 3 ((𝐴 ≼ ℕ ∧ (∀𝑥𝐴 𝑥 ≼ ℕ ∧ 𝐴 ⊆ ℝ)) → 𝐴 ≠ ℝ)
208207expr 456 . 2 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → ( 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ))
209 eqimss 4042 . . 3 ( 𝐴 = ℝ → 𝐴 ⊆ ℝ)
210209necon3bi 2967 . 2 𝐴 ⊆ ℝ → 𝐴 ≠ ℝ)
211208, 210pm2.61d1 180 1 ((𝐴 ≼ ℕ ∧ ∀𝑥𝐴 𝑥 ≼ ℕ) → 𝐴 ≠ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  Vcvv 3480  cdif 3948  wss 3951  c0 4333  {csn 4626   cuni 4907   ciun 4991  Disj wdisj 5110   class class class wbr 5143  cmpt 5225   Or wor 5591   × cxp 5683  dom cdm 5685  ran crn 5686  cima 5688  Fun wfun 6555   Fn wfn 6556  ontowfo 6559  cfv 6561  (class class class)co 7431  cdom 8983  csdm 8984  supcsup 9480  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  +∞cpnf 11292  *cxr 11294   < clt 11295  cn 12266  cz 12613  cuz 12878  ..^cfzo 13694  seqcseq 14042  vol*covol 25497  volcvol 25498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-rest 17467  df-topgen 17488  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-top 22900  df-topon 22917  df-bases 22953  df-cmp 23395  df-ovol 25499  df-vol 25500
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator